From the series: Model-Based Design for DO-178C Software Development with MathWorks Tools
Mike Anthony, MathWorks
In part 7 of this webinar series, we discuss the use of Polyspace for formal verification of the embedded software. Polyspace provides two capabilities within this workflow. The first is the inclusion of a MISRA AC AGC compliance checker which includes the capability to author custom coding rules. The second, and more important, is the application of formal methods to prove the absence of runtime errors in the software. Similar to the concept introduced earlier with Simulink Design Verifier for property proving, Polyspace uses formal methods to prove the absence of runtime errors.
Part 1: Introduction to Model-Based Design for High Integrity Software Development In this first webinar in the series, we introduce Model-Based Design and discuss why it can provide value over traditional software development processes in certification workflows.
Part 2: Requirements-Based Modeling and Traceability In part 2 of this webinar series, we discuss how to build a Simulink model from a requirements document, and how to create bi-directional links for traceability between the detailed design model and the textual high-level requirements.
Part 3: Conformance to Modeling Standards In part 3 of this webinar series, we discuss the importance of developing and enforcing a modeling standard.
Part 4: Verification of the Model Against High-Level Requirements In part 4 of this webinar series, we discuss verification of the model against the textual requirements.
Part 5: Proving Algorithmic Correctness In part 5 of this webinar series, we discuss the idea of using formal methods to further verify the model and assess robustness.
Part 6: Automatic Code Generation and Traceability In part 6 of this webinar series, we discuss automatic flight code generation.
Part 7: Proving Code Correctness In part 7 of this webinar series, we discuss the use of Polyspace for formal verification of the embedded software.
Part 8: Automatic Test Vector Generation and Software-In-the-Loop Testing In part 8 of this webinar series, we discuss the use of Simulink Code Inspector to automate source code reviews.
Part 9: Verification of the Object Code Against the Model In part 9 of this webinar series, we discuss requirements-based testing of the cross-compiled executable object code.
We will not sell or rent your personal contact information. See our privacy policy for details.
You are already signed in to your MathWorks Account. Please press the "Submit" button to complete the process.
Choose a web site to get translated content where available and see local events and offers. Based on your location, we recommend that you select: .
Select web siteYou can also select a web site from the following list:
Select the China site (in Chinese or English) for best site performance. Other MathWorks country sites are not optimized for visits from your location.
This website uses cookies to improve your user experience, personalize content and ads, and analyze website traffic. By continuing to use this website, you consent to our use of cookies. Please see our Privacy Policy to learn more about cookies and how to change your settings.