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)
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).
An extended version of the paper is available as Inria research report RR-6950:
|Slides of J. Stoecker's lecture at IFM'09|