Relational concurrent refinement. II: Internal operations and outputs

DOI10.1007/S00165-007-0066-ZMaRDI QIDQ1019018zbMATH OpenOpenAlexFDO

Authors John Derrick, Gerhard Schellhorn, Eerke 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 refinementdeadlockinternal operationsoutputsfailures-divergences refinementKIVmechanisationsimulations, process algebraic semantics

Mathematics Subject Classification ID

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

Recommendations

• Unifying concurrent and relational refinement
• Relational concurrent refinement
• Modelling Divergence in Relational Concurrent Refinement
• Relational concurrent refinement. III: Traces, partial relations and automata
• More relational concurrent refinement: traces and partial relations

Cites work

• scientific article; zbMATH DE number 1615985 (Why is no real title available?)
• scientific article; zbMATH DE number 3902016 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949592 (Why is no real title available?)
• scientific article; zbMATH DE number 1487738 (Why is no real title available?)
• scientific article; zbMATH DE number 1552508 (Why is no real title available?)
• scientific article; zbMATH DE number 2086954 (Why is no real title available?)
• A Theory of Communicating Sequential Processes
• A hierarchy of failures-based models
• A hierarchy of failures-based models: theory and application
• A singleton failures semantics for communicating sequential processes
• A state-based approach to communicating processes
• A theory of communicating processes with value passing
• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• An analysis of refinement in an abortive paradigm
• CONFLICTS AND FAIR TESTING
• CSP theorems for communicating B machines
• Compositional failure-based semantic models for basic LOTOS
• Concurrency theory. Calculi and automata for modelling untimed and timed cocurrent systems.
• Data Refinement
• LOTOS
• Process simulation and refinement
• Relational algebraic semantics of deterministic and nondeterministic programs
• Relational concurrent refinement
• Specifying and refining internal operations in \(Z\)
• The B-Book
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Unifying concurrent and relational refinement
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(10)

• Modelling Divergence in Relational Concurrent Refinement
• Relational concurrent refinement
• Understanding, Explaining, and Deriving Refinement
• Introducing extra operations in refinement
• Relational concurrent refinement. III: Traces, partial relations and automata
• Incompleteness of relational simulations in the blocking paradigm
• Relational concurrent refinement: automata
• Theoretical Aspects of Computing – ICTAC 2005
• More relational concurrent refinement: traces and partial relations
• Unifying concurrent and relational refinement

Describes a project that uses

Uses Software

• Z
• KIV
• LOTOS

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

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