HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format

Jan Stöcker 1 Frederic Lang 1 Hubert Garavel 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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).
Document type :
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download

Contributor : Jan Stöcker Connect in order to contact the contributor
Submitted on : Wednesday, June 3, 2009 - 11:29:13 AM
Last modification on : Friday, February 4, 2022 - 3:24:43 AM
Long-term archiving on: : Thursday, June 10, 2010 - 10:08:22 PM


Files produced by the author(s)


  • HAL Id : inria-00391024, version 1


Jan Stöcker, Frederic Lang, Hubert Garavel. Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. [Research Report] RR-6950, INRIA. 2009, pp.27. ⟨inria-00391024⟩



Record views


Files downloads