Relational concurrent refinement. II: Internal operations and outputs

DOI10.1007/S00165-007-0066-ZzbMath1165.68412OpenAlexW2111901968MaRDI QIDQ1019018

John Derrick, Gerhard Schellhorn, Eerke A. Boiten

Publication date: 27 May 2009

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-007-0066-z

zbMATH Keywords

Zdata refinementmechanisationdeadlockinternal operationsoutputsfailures-divergences refinementKIVsimulations, process algebraic semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Related Items (7)

Incompleteness of relational simulations in the blocking paradigm ⋮ Relational Concurrent Refinement: Automata ⋮ More Relational Concurrent Refinement: Traces and Partial Relations ⋮ Modelling Divergence in Relational Concurrent Refinement ⋮ Introducing extra operations in refinement ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ Understanding, Explaining, and Deriving Refinement

Uses Software

• LOTOS
• KIV
• Z

Cites Work

• LOTOS
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• Relational concurrent refinement
• An analysis of refinement in an abortive paradigm
• Process simulation and refinement
• Relational algebraic semantics of deterministic and nondeterministic programs
• A state-based approach to communicating processes
• Specifying and refining internal operations in \(Z\)
• A theory of communicating processes with value passing
• A hierarchy of failures-based models: theory and application
• Compositional failure-based semantic models for basic LOTOS
• CSP theorems for communicating B machines
• A singleton failures semantics for communicating sequential processes
• A Theory of Communicating Sequential Processes
• The B-Book
• Data Refinement
• CONFLICTS AND FAIR TESTING
• ZB 2005: Formal Specification and Development in Z and B
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Relational concurrent refinement. II: Internal operations and outputs