CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
From MaRDI portal
Publication:3000666
DOI10.1007/978-3-642-19835-9_33zbMath1316.68074MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68-04: Software, source code, etc. for problems pertaining to computer science
Related Items
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities, An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation, Probabilistic Model Checking for Energy-Utility Analysis, Verification of \(\mathrm{EB}^3\) specifications using CADP, Formal modelling and verification of GALS systems using GRL and CADP, On the diversity of asynchronous communication, A generic framework for \(n\)-protocol compatibility checking, Sequential and distributed on-the-fly computation of weak tau-confluence, Improving active Mealy machine learning for protocol conformance testing, Computing maximal weak and other bisimulations, A formal verification technique for behavioural model-to-model transformations, A linear process-algebraic format with data for probabilistic automata, Automated verification of automata communicating via FIFO and bag buffers, Model checking properties on reduced trace systems, Ensuring liveness properties of distributed systems: open problems, Scaling up livelock verification for network-on-chip routing algorithms, Cartesian difference categories, Evaluation of cyber security and modelling of risk propagation with Petri nets, Compositional verification of asynchronous concurrent systems using CADP, Fault trees on a diet: automated reduction by graph rewriting, Identity-Based Cryptosystems and Quadratic Residuosity, Branching Bisimulation Games, Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular, A compositional framework to the specification of service protocols controllability and substitutability, Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets, Performance Model Checking Scenario-Aware Dataflow, On the Minimisation of Acyclic Models
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
