Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download
Contributor : Christine Mckinty Connect in order to contact the contributor
Submitted on : Wednesday, May 27, 2009 - 3:08:30 PM
Last modification on : Tuesday, August 2, 2022 - 4:24:27 AM
Long-term archiving on: : Monday, October 15, 2012 - 11:15:23 AM


Files produced by the author(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⟩



Record views


Files downloads