This paper presents a validation and verification tool component, based on the Abstract State Machine formal method, that we are developing to support high level formal analysis of embedded system model-driven design. This component is integrated into a model-driven environment for HW/SW co-design that provides a graphical high-level representation of HW and SW components by means of UML profiles for SystemC/multi-thread C, and allows C/C++/SystemC code generation/back-annotation from/to graphical UML models.

A model-driven validation & verification environment for embedded systems / A. Gargantini, E. Riccobene, P. Scandurra - In: SIES'2008 : third International symposium on industrial embedded systems : june 11-13, 2008 : Montpellier-La Grande Motte, France / [a cura di] [s.n.]. - Los Alamitos : Institute of electrical and electronics engineers, 2008. - ISBN 9781424419944. - pp. 241-244 (( Intervento presentato al 3. convegno International Symposium on Industrial Embedded Systems (SIES) tenutosi a Montpellier nel 2008 [10.1109/SIES.2008.4577708].

A model-driven validation & verification environment for embedded systems

E. Riccobene
Secondo
;
P. Scandurra
Ultimo
2008

Abstract

This paper presents a validation and verification tool component, based on the Abstract State Machine formal method, that we are developing to support high level formal analysis of embedded system model-driven design. This component is integrated into a model-driven environment for HW/SW co-design that provides a graphical high-level representation of HW and SW components by means of UML profiles for SystemC/multi-thread C, and allows C/C++/SystemC code generation/back-annotation from/to graphical UML models.
C++ language ; Unified modeling language ; Embedded systems ; Formal verification ; Hardware-software codesign ; Multi-threading ; Program compilers.
Settore INF/01 - Informatica
2008
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/2434/50394
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 0
social impact