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.

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

BARESI, LUCIANO;MOTTA, ALFREDO;ROSSI, MATTEO GIOVANNI
2015-01-01

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.
2015
Closed-loop simulation; Embedded systems; MARTE; Model-driven development, Verification
File in questo prodotto:
File Dimensione Formato  
art%3A10.1007%2Fs10270-013-0330-z.pdf

Accesso riservato

Descrizione: Versione pubblicata
: Publisher’s version
Dimensione 3.27 MB
Formato Adobe PDF
3.27 MB Adobe PDF   Visualizza/Apri
Formal verification and validation of embedded systems_11311-758852_Baresi.pdf

accesso aperto

: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 2.85 MB
Formato Adobe PDF
2.85 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11311/758852
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 12
social impact