Relational concurrent refinement: automata

DOI10.1016/J.ENTCS.2009.12.015MaRDI QIDQ2994488zbMATH OpenOpenAlexFDO

Authors John Derrick, Eerke Boiten

Publication date 1 August 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.12.015

zbMATH Keywords

automata-based refinementsdata refinementsimulationsZ

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) 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. III: Traces, partial relations and automata
• More relational concurrent refinement: traces and partial relations
• Relational concurrent refinement
• Unifying concurrent and relational refinement
• Verifying data refinements using a model checker

Cites work

• A process algebraic view of input/output automata
• A singleton failures semantics for communicating sequential processes
• Data Refinement
• Data refinement and singleton failures refinement are not equivalent
• Forward and backward simulations. I. Untimed Systems
• Handbook of process algebra
• scientific article; zbMATH DE number 1615985 (Why is no real title available?)
• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 4110131 (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 2086954 (Why is no real title available?)
• scientific article; zbMATH DE number 938070 (Why is no real title available?)
• scientific article; zbMATH DE number 2227867 (Why is no real title available?)
• Modelling Divergence in Relational Concurrent Refinement
• More relational concurrent refinement: traces and partial relations
• Prespecification in data refinement
• Quiescence, fairness, testing, and the notion of implementation
• Relational concurrent refinement
• Relational concurrent refinement. II: Internal operations and outputs
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Unifying concurrent and relational refinement

Cited in

(9)

• Unifying concurrent and relational refinement
• Deciding properties of integral relational automata
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• More relational concurrent refinement: traces and partial relations
• ZB 2005: Formal Specification and Development in Z and B
• Refinements for open automata
• Relational concurrent refinement
• Relational concurrent refinement. III: Traces, partial relations and automata
• Verifying data refinements using a model checker

Describes a project that uses

Uses Software

• Z

This page was built for publication: Relational concurrent refinement: automata

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