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 D.; Di Guglielmo L.; Geretti L; Villa T.. - STAMPA. - (2011), pp. 1660-1665. (Intervento presentato al convegno 7th International Wireless Communications and Mobile Computing Conference (IWCMC 2011) tenutosi a Istanbul, Turkey nel July 5-8, 2011) [10.1109/IWCMC.2011.5982784].
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.