In the last years hybrid automata have been applied in the design and verification of embedded systems. Once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to extract a correct-by-construction HW/SW implementation of it. This work discusses a methodology and a corresponding tool chain that allow to extract a HW/SW implementation of a controller modeled by a subclass of timed automata, named elastic controllers, operating in an environment represented by a hybrid automaton. The required tools have been either developed from scratch or extended from the current state-of-the-art in order to support an automated flow from hybrid automata specifications to correct-by-construction discrete implementations described in the SystemC language.

Correct-by-construction code generation from hybrid automata specification

BRESOLIN, DAVIDE;
2011

Abstract

In the last years hybrid automata have been applied in the design and verification of embedded systems. Once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to extract a correct-by-construction HW/SW implementation of it. This work discusses a methodology and a corresponding tool chain that allow to extract a HW/SW implementation of a controller modeled by a subclass of timed automata, named elastic controllers, operating in an environment represented by a hybrid automaton. The required tools have been either developed from scratch or extended from the current state-of-the-art in order to support an automated flow from hybrid automata specifications to correct-by-construction discrete implementations described in the SystemC language.
2011
7th International Wireless Communications and Mobile Computing Conference (IWCMC 2011)
9781424495399
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/11577/3229616
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 4
social impact