Towards validated real-time software

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. Keywords : real-time computing, embedded applications, real-time constraints, compiling, synchronous languages, validation, timed automata, model-checking, external environment modelling.

• Type: Conference
• Year: 2000
• Where: ECRTS
• Authors: Valérie Bertin, Michel Poize, Jacques Pulou, Joseph Sifakis
• Keywords: ECRTS 2000, Embedded Real-time Applications, Embedded Systems, External Environment, Real-time