Relational Concurrent Refinement: Automata

DOI10.1016/j.entcs.2009.12.015zbMath1342.68226OpenAlexW1993758089MaRDI QIDQ2994488

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

simulationsZdata refinementautomata-based refinements

Mathematics Subject Classification ID

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Z

Cites Work

• Prespecification in data refinement
• A process algebraic view of input/output automata
• Relational concurrent refinement
• Data refinement and singleton failures refinement are not equivalent
• Relational concurrent refinement. II: Internal operations and outputs
• Quiescence, fairness, testing, and the notion of implementation
• Forward and backward simulations. I. Untimed Systems
• A singleton failures semantics for communicating sequential processes
• Modelling Divergence in Relational Concurrent Refinement
• Data Refinement
• More Relational Concurrent Refinement: Traces and Partial Relations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item