Verification of GALS Systems by Combining Synchronous Languages and Process Calculi

Hubert Garavel and Damien Thivolle

Proceedings of the 16th International SPIN Workshop on Model Checking of Software SPIN'2009 (Grenoble, France)

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.

20 pages

PDF

Postscript

Slides of D. Thivolle's lecture at SPIN'09:

PDF