Compositional verification of asynchronous concurrent systems using CADP

DOI10.1007/S00236-015-0226-1MaRDI QIDQ2350492zbMATH OpenOpenAlexFDO

Authors Hubert Garavel, Frédéric Lang, Radu Mateescu

Publication date 24 June 2015

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00236-015-0226-1

Mathematics Subject Classification ID

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

• Automata, Languages and Programming
• Automatic verification of concurrent systems using a formula-based compositional approach
• Verification of large state/event systems using compositionality and dependency analysis
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Automatic and hierarchical verification for concurrent systems

Cites work

• scientific article; zbMATH DE number 1670789 (Why is no real title available?)
• scientific article; zbMATH DE number 4056971 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 49477 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 176726 (Why is no real title available?)
• scientific article; zbMATH DE number 177237 (Why is no real title available?)
• scientific article; zbMATH DE number 177254 (Why is no real title available?)
• scientific article; zbMATH DE number 177514 (Why is no real title available?)
• scientific article; zbMATH DE number 177521 (Why is no real title available?)
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• scientific article; zbMATH DE number 1283472 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 526071 (Why is no real title available?)
• scientific article; zbMATH DE number 1088043 (Why is no real title available?)
• scientific article; zbMATH DE number 1956590 (Why is no real title available?)
• scientific article; zbMATH DE number 2080056 (Why is no real title available?)
• scientific article; zbMATH DE number 2080068 (Why is no real title available?)
• scientific article; zbMATH DE number 1487860 (Why is no real title available?)
• scientific article; zbMATH DE number 1538042 (Why is no real title available?)
• scientific article; zbMATH DE number 4119602 (Why is no real title available?)
• scientific article; zbMATH DE number 4119650 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 1418456 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Theory of Communicating Sequential Processes
• A calculus of communicating systems
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• A partial approach to model checking
• A structural approach to operational semantics
• Algebra of communicating processes with abstraction
• An action-based framework for veryfying logical and behavioural properties of concurrent systems
• Branching time and abstraction in bisimulation semantics
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Communicating sequential processes
• Compiling communicating processes into delay-insensitive VLSI circuits
• Compositional checking of satisfaction
• Compositional minimisation of finite state systems using interface specifications
• Dynamic partial-order reduction for model checking software
• Efficient on-the-fly model-checking for regular alternation-free -calculus
• FDR3 -- a modern refinement checker for CSP
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Handbook of process algebra
• Local model checking and protocol analysis
• Modal logics and mu-calculi: An introduction
• Model checking and boolean graphs
• Model checking for action-based logics
• Model-checking for real-time systems
• On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP
• Partial model checking of modal equations: a survey
• Partial model checking using networks of labelled transition systems and Boolean equation systems
• Partial model checking using networks of labelled transition systems and Boolean equation systems
• Propositional dynamic logic of looping and converse is elementarily decidable
• Propositional dynamic logic of regular programs
• Refined Interfaces for Compositional Verification
• Results on the propositional \(\mu\)-calculus
• Selective mu-calculus and formula-based equivalence of transition systems
• Specification guidelines to avoid the state space explosion problem
• Structural operational semantics.
• Temporal logic can be more expressive
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• The origins of structural operational semantics
• The temporal semantics of concurrent programs
• Three Partition Refinement Algorithms
• Translating FSP into LOTOS and networks of automata
• Using branching time temporal logic to synthesize synchronization skeletons
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Verification, Model Checking, and Abstract Interpretation
• “Sometimes” and “not never” revisited

Cited in

(22)

• To compose, or not to compose, that is the question: an analysis of compositional state space generation
• Reflections on the future of concurrency theory in general and process calculi in particular
• Automata, Languages and Programming
• Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
• Compositional verification of priority systems using sharp bisimulation
• Compositional verification of concurrent systems by combining bisimulations
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Formal modelling and verification of GALS systems using GRL and CADP
• Equivalence checking 40 years after: a review of bisimulation tools
• Compositional verification in rewriting logic
• Sharp congruences adequate with temporal logics combining weak and strong modalities
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• Component-aware input-output conformance
• scientific article; zbMATH DE number 2090149 (Why is no real title available?)
• Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous
• A system for compositional verification of asynchronous objects
• Verification of large state/event systems using compositionality and dependency analysis
• A formalisation of consistent consequence for Boolean equation systems
• Compositional verification of concurrent systems by combining bisimulations
• An account of implementing applicative term rewriting
• Caper
• Cartesian difference categories

Describes a project that uses

Uses Software

• LNT2LOTOS
• CMC
• FDR3
• fc2tools
• CAESAR_SOLVE
• Exp.Open
• LTSmin
• CADP
• E-LOTOS

This page was built for publication: Compositional verification of asynchronous concurrent systems using CADP

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