Formal verification and validation of embedded systems: The UML-based MADES approach

Luciano Baresi; Gundula Blohm; Dimitris Kolovos; Nicholas Matragkas; Alfredo Motta; Richard Freeman Paige; Alek Radjenovic; Matteo Rossi

doi:10.1007/s10270-013-0330-z

Formal verification and validation of embedded systems: The UML-based MADES approach

Luciano Baresi, Gundula Blohm, Dimitris Kolovos, Nicholas Matragkas, Alfredo Motta, Richard Freeman Paige, Alek Radjenovic, Matteo Rossi

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

Formal verification and validation activities from the early development phases can foster system consistency, correctness, and integrity, but they are often hard to carry out as most designers do not have the necessary background. To address this difficulty, a possible approach is to allow engineers to continue using familiar notations and tools, while verification and validation are performed on demand, automatically, and transparently. In this paper we describe how the problem of making formal verification and validation tasks more designer-friendly is tackled by the MADES approach. Our solution is based on a tool chain that is built atop mature, popular, and widespread technologies. The paper focuses on the verification and closed-loop simulation (validation) aspects of the approach and shows how it can be applied to significant embedded software systems.

Original language	English
Number of pages	21
Journal	Software and Systems Modeling
DOIs	https://doi.org/10.1007/s10270-013-0330-z
Publication status	Published - 12 Jun 2013

Access to Document

10.1007/s10270-013-0330-z

Cite this

@article{dfc1b639b175412ebe7b5b6bfd9f092b,

title = "Formal verification and validation of embedded systems: The UML-based MADES approach",

abstract = "Formal verification and validation activities from the early development phases can foster system consistency, correctness, and integrity, but they are often hard to carry out as most designers do not have the necessary background. To address this difficulty, a possible approach is to allow engineers to continue using familiar notations and tools, while verification and validation are performed on demand, automatically, and transparently. In this paper we describe how the problem of making formal verification and validation tasks more designer-friendly is tackled by the MADES approach. Our solution is based on a tool chain that is built atop mature, popular, and widespread technologies. The paper focuses on the verification and closed-loop simulation (validation) aspects of the approach and shows how it can be applied to significant embedded software systems.",

author = "Luciano Baresi and Gundula Blohm and Dimitris Kolovos and Nicholas Matragkas and Alfredo Motta and Paige, {Richard Freeman} and Alek Radjenovic and Matteo Rossi",

year = "2013",

month = jun,

day = "12",

doi = "10.1007/s10270-013-0330-z",

language = "English",

journal = "Software and Systems Modeling",

issn = "1619-1366",

publisher = "Springer",

}

TY - JOUR

T1 - Formal verification and validation of embedded systems

T2 - The UML-based MADES approach

AU - Baresi, Luciano

AU - Blohm, Gundula

AU - Kolovos, Dimitris

AU - Matragkas, Nicholas

AU - Motta, Alfredo

AU - Paige, Richard Freeman

AU - Radjenovic, Alek

AU - Rossi, Matteo

PY - 2013/6/12

Y1 - 2013/6/12

N2 - Formal verification and validation activities from the early development phases can foster system consistency, correctness, and integrity, but they are often hard to carry out as most designers do not have the necessary background. To address this difficulty, a possible approach is to allow engineers to continue using familiar notations and tools, while verification and validation are performed on demand, automatically, and transparently. In this paper we describe how the problem of making formal verification and validation tasks more designer-friendly is tackled by the MADES approach. Our solution is based on a tool chain that is built atop mature, popular, and widespread technologies. The paper focuses on the verification and closed-loop simulation (validation) aspects of the approach and shows how it can be applied to significant embedded software systems.

AB - Formal verification and validation activities from the early development phases can foster system consistency, correctness, and integrity, but they are often hard to carry out as most designers do not have the necessary background. To address this difficulty, a possible approach is to allow engineers to continue using familiar notations and tools, while verification and validation are performed on demand, automatically, and transparently. In this paper we describe how the problem of making formal verification and validation tasks more designer-friendly is tackled by the MADES approach. Our solution is based on a tool chain that is built atop mature, popular, and widespread technologies. The paper focuses on the verification and closed-loop simulation (validation) aspects of the approach and shows how it can be applied to significant embedded software systems.

U2 - 10.1007/s10270-013-0330-z

DO - 10.1007/s10270-013-0330-z

M3 - Article

SN - 1619-1366

JO - Software and Systems Modeling

JF - Software and Systems Modeling

ER -