Modelling Divergence in Relational Concurrent Refinement

DOI10.1007/978-3-642-00255-7_13zbMath1211.68265OpenAlexW1588227792MaRDI QIDQ3605466

John Derrick, Eerke A. Boiten

Publication date: 24 February 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-00255-7_13

zbMATH Keywords

divergencesimulationsdata refinementinternal operationsprocess algebraic refinement preorders

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)

Related Items (4)

Relational Concurrent Refinement: Automata ⋮ The behavioural semantics of Event-B refinement ⋮ Introducing extra operations in refinement ⋮ Relational concurrent refinement. III: Traces, partial relations and automata

Uses Software

• LOTOS
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Observation equivalence as a testing equivalence
• Incompleteness of relational simulations in the blocking paradigm
• Relational concurrent refinement
• Data refinement and singleton failures refinement are not equivalent
• Relational concurrent refinement. II: Internal operations and outputs
• Extensional equivalences for transition systems
• A state-based approach to communicating processes
• Specifying and refining internal operations in \(Z\)
• Testing equivalence as a bisimulation equivalence
• Data Refinement
• More Relational Concurrent Refinement: Traces and Partial Relations
• Communicating Sequential Processes. The First 25 Years

This page was built for publication: Modelling Divergence in Relational Concurrent Refinement