Automatic verification of distributed systems: the process algebra approach.

DOI10.1007/BF00121261zbMATH Open1425.68294MaRDI QIDQ960505FDOQ960505

Authors: P. Inverardi, Corrado Priami 

Publication date: 21 December 2008

Published in: Formal Methods in System Design (Search for Journal in Brave)

Recommendations

• Algebraic process verification.
• scientific article
• Process algebra and model checking
• Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings
• Publication:4941495

zbMATH Keywords

toolsdistributed systemsprocess algebraconcurrent systemsautomatic verification

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)

Cites Work

• LOTOS
• Graph-Based Algorithms for Boolean Function Manipulation
• Characterizing finite Kripke structures in propositional temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Process algebra for synchronous communication
• Algebraic laws for nondeterminism and concurrency
• Title not available (Why is that?)
• Title not available (Why is that?)
• Calculi for synchrony and asynchrony
• Bisimulation through probabilistic testing
• Three Partition Refinement Algorithms
• Testing equivalences for processes
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Results on the propositional \(\mu\)-calculus
• “Sometimes” and “not never” revisited
• Formal verification of parallel programs
• Branching time and abstraction in bisimulation semantics
• Submodule construction as equation solving in CCS
• Algèbre de processus et synchronisation
• Title not available (Why is that?)
• Three logics for branching bisimulation
• Title not available (Why is that?)
• Testing equivalence as a bisimulation equivalence
• Title not available (Why is that?)
• Universal axioms for bisimulations
• Title not available (Why is that?)
• An action-based framework for veryfying logical and behavioural properties of concurrent systems
• Title not available (Why is that?)
• CIRCAL and the representation of communication, concurrency, and time
• Title not available (Why is that?)
• Linear time, branching time and partial order in logics and models for concurrency. School/workshop, Noordwijkerhout, The Netherlands, May 30- June 3, 1988. Proceedings
• Fast Algorithms for Solving Path Problems
• Proof systems for satisfiability in Hennessy-Milner logic with recursion
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Title not available (Why is that?)
• Generating BDDs for symbolic model checking in CCS
• A Unified Approach to Path Problems
• Automatizing parametric reasoning on distributed concurrent systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (10)

• Automatizing parametric reasoning on distributed concurrent systems
• Title not available (Why is that?)
• Equivalence checking 40 years after: a review of bisimulation tools
• CADP 2010: a toolbox for the construction and analysis of distributed processes
• On the usability of process algebra: An architectural view
• Algebraic process verification.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Protocol verification with the Aldébaran toolset

Uses Software

• LOTOS

This page was built for publication: Automatic verification of distributed systems: the process algebra approach.

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