Formal model and code verification in Model-Based Design

The increasing complexity of embedded software makes its verification a key challenge in designing embedded systems. This paper gives an overview of Model-Based Design used for large and complex embedded systems, with emphasis on the early verification of the design. Two tools for verification through formal analysis are described: Simulinkreg Design Verifiertrade to check the properties of a model, and PolySpacereg to prove the absence of certain run-time errors in the embedded software.