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).
Type de document :
Rapport
[Research Report] RR-6950, INRIA. 2009, pp.27
Liste complète des métadonnées

Littérature citée [43 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00391024
Contributeur : Jan Stöcker <>
Soumis le : mercredi 3 juin 2009 - 11:29:13
Dernière modification le : mercredi 11 avril 2018 - 01:51:50
Document(s) archivé(s) le : jeudi 10 juin 2010 - 22:08:22

Fichiers

RR-6950.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

416

Téléchargements de fichiers

364