Formal modelling and verification of GALS systems using GRL and CADP

DOI10.1007/S00165-016-0373-3MaRDI QIDQ315303zbMATH OpenOpenAlexFDO

Authors Fatma Jebali, Frédéric Lang, Radu Mateescu

Publication date 20 September 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01290449/file/fac2egui-crc.pdf

zbMATH Keywords

asynchronous concurrencyCADPformal description techniquesGALS systemsGRLmodel-based verification

Mathematics Subject Classification ID

Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Computer Aided Verification
• Formal verification of timed synchronous dataflow graphs using Lustre
• scientific article; zbMATH DE number 2017354
• Publication:4507869
• RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking

Cites work

• A calculus of communicating systems
• Branching time and abstraction in bisimulation semantics
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Calculi for synchrony and asynchrony
• Compiling and verifying SC-SystemJ programs for safety-critical reactive systems
• Compositional verification of asynchronous concurrent systems using CADP
• Computer Aided Verification
• Concurrency in synchronous systems
• From concurrent multi-clock programs to deterministic asynchronous implementations
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1361122 (Why is no real title available?)
• scientific article; zbMATH DE number 526071 (Why is no real title available?)
• scientific article; zbMATH DE number 2017354 (Why is no real title available?)
• scientific article; zbMATH DE number 2033527 (Why is no real title available?)
• scientific article; zbMATH DE number 2087557 (Why is no real title available?)
• scientific article; zbMATH DE number 1852153 (Why is no real title available?)
• Reflections on the future of concurrency theory in general and process calculi in particular
• System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation

Cited in

(5)

• Formal verification of timed synchronous dataflow graphs using Lustre
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• scientific article; zbMATH DE number 2017356 (Why is no real title available?)
• scientific article; zbMATH DE number 2086953 (Why is no real title available?)
• Computer Aided Verification

Describes a project that uses

Uses Software

• CADP
• Polychrony
• GRL
• Esterel
• E-LOTOS
• SPIN
• LNT2LOTOS
• AADL

This page was built for publication: Formal modelling and verification of GALS systems using GRL and CADP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q315303)