We present a tool for the design and validation of embedded real time applications. The tool integrates two approaches: the use of the synchronous programming language, ESTEREL for design, and the application of model checking techniques for validation of real time properties. Validation is carried out on a global formal model (timed automata) taking into account the effective implementation of the application on the target hardware architecture as well as its external environment behavior
Sandro Carrara, Ali Meimandi, Ata Jedari Golparvar, Sarah Tonello