Title :
Towards validated real-time software
Author :
Bertin, Valérie ; Poize, Michel ; Pulou, Jacques ; Sifakis, Joseph
Author_Institution :
Centre Nat. d Etudes de Telecommun., Meylan, France
Abstract :
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 :
automata theory; high level languages; program verification; real-time systems; scheduling; ESTEREL; embedded real time applications; external environment behavior; global formal model; model checking techniques; real time properties; synchronous programming language; target hardware architecture; timed automata; validated real time software; Application software; Automata; Computer applications; Computer languages; Costs; Electrical capacitance tomography; Embedded computing; Equations; Software tools; Timing;
Conference_Titel :
Real-Time Systems, 2000. Euromicro RTS 2000. 12th Euromicro Conference on
Conference_Location :
Stockholm
Print_ISBN :
0-7695-0734-4
DOI :
10.1109/EMRTS.2000.854003
