CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes

DOI10.1007/978-3-642-19835-9_33zbMath1316.68074OpenAlexW1980824962MaRDI QIDQ3000666

Frédéric Lang, Radu Mateescu, Hubert Garavel, Wendelin Serwe

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_33

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) Software, source code, etc. for problems pertaining to computer science (68-04)

Related Items (32)

An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Performance Model Checking Scenario-Aware Dataflow ⋮ Formal modelling and verification of GALS systems using GRL and CADP ⋮ On the diversity of asynchronous communication ⋮ Scaling up livelock verification for network-on-chip routing algorithms ⋮ Automated verification of automata communicating via FIFO and bag buffers ⋮ A compositional framework to the specification of service protocols controllability and substitutability ⋮ Probabilistic model checking of BPMN processes at runtime ⋮ Fault trees on a diet: automated reduction by graph rewriting ⋮ Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets ⋮ Elimination of detached regions in dependency graph verification ⋮ Simulation relations and applications in formal methods ⋮ Convex lattice equation systems ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ Cartesian difference categories ⋮ A generic framework for \(n\)-protocol compatibility checking ⋮ Sequential and distributed on-the-fly computation of weak tau-confluence ⋮ On the Minimisation of Acyclic Models ⋮ Improving active Mealy machine learning for protocol conformance testing ⋮ Model checking properties on reduced trace systems ⋮ Computing maximal weak and other bisimulations ⋮ A formal verification technique for behavioural model-to-model transformations ⋮ Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities ⋮ Probabilistic Model Checking for Energy-Utility Analysis ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ Identity-Based Cryptosystems and Quadratic Residuosity ⋮ Branching Bisimulation Games ⋮ A linear process-algebraic format with data for probabilistic automata ⋮ Evaluation of cyber security and modelling of risk propagation with Petri nets ⋮ Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• Kronos
• BISIMULATOR
• M-TREE
• E-LOTOS
• SPIN
• CADP
• Fiacre
• Exp.Open
• CAESAR_SOLVE
• XTL
• CAESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Translating FSP into LOTOS and networks of automata
• Interactive Markov chains. And the quest for quantified quality
• State space reduction for process algebra specifications
• On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP
• Model checking and boolean graphs
• Efficient on-the-fly model-checking for regular alternation-free \(\mu\)-calculus
• Rewriting of imperative programs into logical equations
• Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular
• Solving Parity Games in Big Steps
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes