Algebraic process verification.
The article shows how to verify distributed and communicating systems in an effective way from an explicit process algebraic standpoint. All calculations involved are based on the axioms and principles of process algebras. The standard process algebra is extended by adding equational data types. Various means to verify complex systems are explained including: invariants, linear process operations, the cones and foci method, the use of confluence, and the composition of similar parallel processes. Verifications of the serial line interface protocol and IEEE 1394 tree identify protocol are presented as an illustration of the method.NEWLINENEWLINEFor the entire collection see [Zbl 0971.00006].
- Automatic verification of distributed systems: the process algebra approach.
- Focus points and convergent process operators: A proof strategy for protocol verification
- scientific article; zbMATH DE number 3958712
- A computer checked algebraic verification of a distributed summation algorithm
- scientific article; zbMATH DE number 5181778
- A formal axiomatization for alphabet reasoning with parametrized processes
- Focus points and convergent process operators: A proof strategy for protocol verification
- Hybrid process algebra
- A brief history of process algebra
- On the usability of process algebra: An architectural view
- On the expressiveness of choice quantification
- Axiomatizing recursion-free, regular monitors
- Algebraic verification method for SEREs properties via Groebner bases approaches
- Verifying an infinite systolic algorithm using third-order equational methods
- Parameterised Boolean equation systems
- A computer checked algebraic verification of a distributed summation algorithm
- Generalizing DPLL and satisfiability for equalities
- Multiparty contract signing over a reliable network
- Relating hybrid chi to other formalisms
- Model-based engineering of embedded systems using the hybrid process algebra Chi
- A verification technique for reversible process algebra
- A Context-Free Process as a Pushdown Automaton
- Five Determinisation Algorithms
- A Framework for Automatically Checking Anonymity with μCRL
- Refined Interfaces for Compositional Verification
- scientific article; zbMATH DE number 4092735 (Why is no real title available?)
- scientific article; zbMATH DE number 1746446 (Why is no real title available?)
- scientific article; zbMATH DE number 868110 (Why is no real title available?)
- An algebraic reasoning approach for verifying the behavior of software evolution processes
- Dynamic consistency in process algebra: from paradigm to ACP
- From CRL to mCRL2: motivation and outline
- Discretization of timed automata in timed CRL à la regions and zones
- Dynamic consistency in process algebra: from paradigm to ACP
- scientific article; zbMATH DE number 5181778 (Why is no real title available?)
- Process-algebraic approaches for multi-agent systems: an overview
- On process equivalence = equation solving in CCS
- Cones and foci: A mechanical framework for protocol verification
- Model checking a cache coherence protocol of a Java DSM implementation
- Automatic verification of distributed systems: the process algebra approach.
This page was built for publication: Algebraic process verification.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2760254)
