Modelling Divergence in Relational Concurrent Refinement

DOI10.1007/978-3-642-00255-7_13MaRDI QIDQ3605466zbMATH OpenOpenAlexFDO

Authors John Derrick, Eerke 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

data refinementdivergenceinternal operationsprocess algebraic refinement preorderssimulations

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)

Recommendations

• Relational concurrent refinement
• Relational concurrent refinement. II: Internal operations and outputs
• Unifying concurrent and relational refinement
• More relational concurrent refinement: traces and partial relations
• Relational concurrent refinement. III: Traces, partial relations and automata

Cites work

• A state-based approach to communicating processes
• Communicating Sequential Processes. The First 25 Years
• Data Refinement
• Data refinement and singleton failures refinement are not equivalent
• Extensional equivalences for transition systems
• Handbook of process algebra
• 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 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 1361140 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 2086954 (Why is no real title available?)
• Incompleteness of relational simulations in the blocking paradigm
• More relational concurrent refinement: traces and partial relations
• Observation equivalence as a testing equivalence
• Relational concurrent refinement
• Relational concurrent refinement. II: Internal operations and outputs
• Specifying and refining internal operations in \(Z\)
• Testing equivalence as a bisimulation equivalence
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.

Cited in

(6)

• Relational concurrent refinement. II: Internal operations and outputs
• Relational concurrent refinement: automata
• More relational concurrent refinement: traces and partial relations
• The behavioural semantics of Event-B refinement
• Introducing extra operations in refinement
• Relational concurrent refinement. III: Traces, partial relations and automata

Describes a project that uses

Uses Software

• LOTOS
• Z

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

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