Model-Based Design Verification

Model-Based Design (MBD) provides a basis for machine-assisted verification of the system under development by the definition of models, supporting initial design decisions as well as enabling early discovering of errors. Models can be analysed with different MBD Verification methods.

Method Purpose Short description of the method's purpose and main benefits

Method description A detailed description of the method

Model-Based Design (MBD) is a method to address the design of complex systems with models. It prescribes the use of models through the development process in order to represent system requirements, architecture and behaviours, providing a basis for machine-assisted analysis of system properties, and supporting design decisions through processes of refinement into implementation. The purpose is:

To reduce the complexity of design by abstraction,
To ensure the quality of the system by rigorous analysis of its properties, and
To reduce the cost of the development by detecting issues in the early phases of the development.

MBD is quite standard in software engineering and is becoming more and more relevant in system engineering, where it must integrate methods for control engineering and safety engineering [MBD1, MBD2, MBD3, MBD4, MBD5, MBD6].
Models can be analysed with different V&V methods. When the models are associated with a formal semantics, formal methods can be applied for a rigorous analysis of correctness and dependability properties. MBD V&V methods include: simulation, testing, model checking, model-based safety analysis, requirements analysis, schedulability analysis, performance analysis, design space exploration.
The models are typically described in high-level languages, usually with a graphical notation. These languages can be standardized (e.g., AADL, UML, SysML) or proprietary (e.g., Simulink).

Method Strengths A listof the strengths of the method

Reduces the complexity of design by abstraction;
Ensures the quality of the system by rigorous analysis of its properties;
Reduces the cost of the development by detecting issues in the early phases of the development.

Method Limitations The limitations of the method

A formal semantics must be assigned to the models.

Method References Bibliography references to papers about the method.

[MBD1] Bouali, Amar & Dion, Bernard. (2005). Formal Verification for Model-Based Development. 10.4271/2005-01-0781.
[MBD2] Conrad, Mirko & Mosterman, Pieter. (2013). Model-Based Design Using Simulink - Modeling, Code Generation, Verification, and Validation. 159-181. 10.1002/9781118561898.ch4.
[MBD3] Antonio Cicchetti, Federico Ciccozzi, Silvia Mazzini, Stefano Puri, Marco Panunzio, Alessandro Zovi, Tullio Vardanega: CHESS: a model-driven engineering tool environment for aiding the development of complex industrial systems. ASE 2012: 362-365
[MBD4] Mazzini, S. & Baracchi, L. & Gérald, Garcia & Cimatti, Alessandro & Tonetta, Stefano. (2013). The FOREVER Methodology: a MBSE framework for Formal Verification.
[MBD5] Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri: The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. SAFECOMP 2009: 173-186
[MBD6] Jeff C. Jensen, Danica H. Chang, Edward A. Lee: A model-based design methodology for cyber-physical systems. IWCMC 2011: 1666-1671

Method Dimensions

Evaluation Environment Type Type of environment where the method is applied. It can be more than one type of environment. (Dimension 1)

Evaluation Type Type of evaluation performed with that method. If a method is hybrid, more than one type can be selected. (Dimension 2)

Type of Component Under Evaluation Type of components that can be evaluated with that method. It can be more than one type. (Dimension 3)

Evaluation Stage The evaluation stage where the method is used. (Dimension 5)

Purpose of the Component Under Evaluation The type of purpose that can be evaluated by a method. It can be more than one type. (Dimension 6)

Type of Requirement Under Evaluation The type of requirements that a method is able to evaluate. It can be more than one type. (Dimension 7)

Evaluation Performance Indicator The type of evaluation criteria or KPI that a method is able to improve. It can be more than one type. (Dimension 8)

Relations

Related Methods A method could be related to other methods.

Tools A method can use zero or more tools.

Part Method A method (when it is a combination: Combination of method artefact that is a specialization of a V&V Method) could be composed of a set of V&V Methods.

Test Case or Verification and Validation activity Test Case or V&V activity performed in a Use Case. We will link to the method to the test cases where the method is used.

Standards A method can be linked with standards.

Context

Workflow

Contents

There are currently no items in this folder.