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

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 engineer...

Full description

Saved in:
Bibliographic Details
Published in:Software and systems modeling 2015-02, Vol.14 (1), p.343-363
Main Authors: Baresi, Luciano, Blohm, Gundula, Kolovos, Dimitrios S., Matragkas, Nicholas, Motta, Alfredo, Paige, Richard F., Radjenovic, Alek, Rossi, Matteo
Format: Article
Language:English
Subjects:
Compilers
Computer programs
Computer Science
Consistency
Embedded computer systems
Information Systems Applications (incl.Internet)
Integrity
Interpreters
IT in Business
Phases
Programming Languages
Programming Techniques
Simulation
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Special Section Paper
Tasks
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1619-1366
1619-1374
DOI:10.1007/s10270-013-0330-z