A compositional protocol verification using relativized bisimulation

DOI10.1016/0890-5401(92)90025-BMaRDI QIDQ1193593zbMATH OpenOpenAlexFDO

Authors Kim G. Larsen, Robin Milner

Publication date 27 September 1992

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0890-5401(92)90025-b

zbMATH Keywords

communicating systemsalternating bit protocolrelative bisimulation

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Network design and communication in computer systems (68M10)

Recommendations

• scientific article; zbMATH DE number 4022620
• scientific article; zbMATH DE number 4060694
• Partial specifications and compositional verification
• scientific article; zbMATH DE number 3958712
• Focus points and convergent process operators: A proof strategy for protocol verification

Cites work

• scientific article; zbMATH DE number 3919813 (Why is no real title available?)
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• scientific article; zbMATH DE number 3956417 (Why is no real title available?)
• scientific article; zbMATH DE number 3958712 (Why is no real title available?)
• scientific article; zbMATH DE number 3958718 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 3744561 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• A calculus of communicating systems
• A context dependent equivalence between processes
• Algebra of communicating processes with abstraction
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Bisimulation and divergence
• Calculi for synchrony and asynchrony
• Communicating sequential processes
• Compositionality Through an Operational Semantics of Contexts
• Tentative steps toward a development method for interfering programs

Cited in

(8)

• scientific article; zbMATH DE number 2102719 (Why is no real title available?)
• Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
• scientific article; zbMATH DE number 4022620 (Why is no real title available?)
• Focus points and convergent process operators: A proof strategy for protocol verification
• scientific article; zbMATH DE number 4060694 (Why is no real title available?)
• Extending modal transition systems with structured labels
• \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
• Self-similarity breeds resilience

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: A compositional protocol verification using relativized bisimulation

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