MOdel-based DEsign & Verification for Safety-Critical Embedded Systems

Model Based System Engineering (MBSE) for Embedded Systems: An Overview

The early design verification of safety-critical embedded systems is a key research area due to the complexity of these systems. Model Based System Engineering (MBSE) has been frequently used to perform the early design verification. Consequently, the major steps are shown in the following figure:

MBSE introduction


  • Representation of structural and behavioral requirements at higher abstraction level
    • Unified Modeling Language (UML) and its SYSML (Systems Modeling Language) / MARTE (Modeling and Analysis of Real-Time and Embedded systems) profiles are frequently used
  • Representation of system properties / constraints for early design verification
    • OMG (Object Management Group) standards like OCL (Object Constraint Language) and MARTE Clock Constraint Specification Language (CCSL)are frequently used
  • Output of modeling phase is a complete abstract model/design that includes structural, behavioral /temporal and verification requirements altogether


  • It is used to generate the target verification model/code from the source model
  • Two types of transformation approaches: Model-to-Model (M2M) and Model-to-Text (M2T)
  • After the generation of required verification model/code, verification is performed


  • Two types of verification techniques: Static Verification (Formal Verification) and Dynamic Verification (Simulation)
  • In static verification, formal approaches are used. For example, Timed Automata and B method
  • In dynamic verification, simulation is performed. For example, Modelica and VHDL