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
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
Contributeur : Christine Mckinty <>
Soumis le : mercredi 27 mai 2009 - 15:08:30
Dernière modification le : vendredi 25 octobre 2019 - 02:01:26
Archivage à long terme le : lundi 15 octobre 2012 - 11:15:23


Fichiers produits par l'(les) auteur(s)




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. ⟨10.1007/978-3-642-02652-2_20⟩. ⟨inria-00388819⟩



Consultations de la notice


Téléchargements de fichiers