2009 | OriginalPaper | Buchkapitel
Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
verfasst von : Hubert Garavel, Damien Thivolle
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
TftpUdp
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.