Mike Anthony, MathWorks
In part 5 of this webinar series, we discuss the idea of using formal methods to further verify the model and assess robustness. Executing test cases verifies the algorithm’s functionality for that single input case. The use of formal methods analysis allows the developer to verify the algorithm’s functionality for all possible inputs. Except for the simplest algorithms, this level of rigor and robustness is typically impossible to perform via testing alone. This example uses Simulink and Simulink Design Verifier to apply formal methods to prove the absence of design errors in the model, assess functional behavior in all possible scenarios, and automatically generate test cases for missing coverage.
Recorded: 31 March 2013
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 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.