PostScript
Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format
Jan Stoecker, Frédéric Lang, and Hubert Garavel
Proceedings of the 7th International Conference on Integrated Formal Methods IFM'09 (Dusseldorf, Germany)
Abstract:
To model real-life critical systems, one needs ``high-level'' languages to express three important concepts: complex data structures, concurrency, and real-time. So far, the verification of timed systems has been successfully applied to ``low-level'' models, such as timed extensions of automata or of Petri nets. To bridge the gap between high-level languages, which allow a concise modeling of systems, and low-level models, for which efficient algorithms and tools have been designed, intermediate models are needed. In this article, we propose the ATLANTIF intermediate model, an extension with real-time and concurrency of the NTIF (New Technology Intermediate Format) intermediate model. We define the formal semantics of ATLANTIF and present a translator from ATLANTIF to timed automata (for verification using UPPAAL), and to time Petri nets (for verification using TINA).
| 15 pages | |
PostScript |
An extended version of the paper is available as Inria research report RR-6950:
| 30 pages | |
PostScript |
| Slides of J. Stoecker's lecture at IFM'09 | |