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
Reports

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 :
Reports
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download

https://hal.inria.fr/inria-00391024
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

RR-6950.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00391024, version 1

Citation

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⟩

Share

Metrics

Record views

187

Files downloads

260