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

https://hal.inria.fr/inria-00388819
Contributor : Christine Mckinty <>
Submitted on : Wednesday, May 27, 2009 - 3:08:30 PM
Last modification on : Thursday, November 19, 2020 - 1:00:26 PM
Long-term archiving on: : Monday, October 15, 2012 - 11:15:23 AM

File

Garavel-Thivolle-09.pdf
Files produced by the author(s)

Identifiers

Collections

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

Share

Metrics

Record views

375

Files downloads

568