Verification of GALS Systems by Combining Synchronous Languages and Process Calculi

Hubert Garavel 1 Damien Thivolle 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : A Gals (Globally Asynchronous Locally Synchronous) system typically consists of a collection of sequential, deterministic components that execute concurrently and communicate using slow or unreliable channels. This paper proposes a general approach for modelling and verifying Gals systems using a combination of synchronous languages (for the sequential components) and process calculi (for communication channels and asynchronous concurrency). This approach is illustrated with an industrial case-study provided by Airbus: a Tftp/Udp communication protocol between a plane and the ground, which is modelled using the Eclipse/Topcased workbench for model-driven engineering and then analysed formally using the Cadp verification and performance evaluation toolbox.
Type de document :
Communication dans un congrès
Model Checking Software, Proceedings of the 16th International SPIN Workshop on Model Checking of Software SPIN'2009, Jun 2009, Grenoble, France. 2009, 〈10.1007/978-3-642-02652-2_20〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00388819
Contributeur : Christine Mckinty <>
Soumis le : mercredi 27 mai 2009 - 15:08:30
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : lundi 15 octobre 2012 - 11:15:23

Fichier

Garavel-Thivolle-09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UGA | LIG_MFML | LIG | LIG_MFML_CONVECS | LIG_SRCPR

Citation

Hubert Garavel, Damien Thivolle. Verification of GALS Systems by Combining Synchronous Languages and Process Calculi. Model Checking Software, Proceedings of the 16th International SPIN Workshop on Model Checking of Software SPIN'2009, Jun 2009, Grenoble, France. 2009, 〈10.1007/978-3-642-02652-2_20〉. 〈inria-00388819〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

252

Téléchargements de fichiers

230

Contact


archive-ouverte@inria.fr