Introducing extra operations in refinement

DOI10.1007/S00165-012-0266-ZzbMath1342.68204OpenAlexW2000939935MaRDI QIDQ736913

Eerke A. Boiten

Publication date: 5 August 2016

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

Full work available at URL: https://kar.kent.ac.uk/31991/1/stutterfacv2withbibs.pdf

zbMATH Keywords

divergenceZrefinementgranularityASMaction refinementEvent-Bweakinternal operationsperspicuitystuttering steps

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Understanding, Explaining, and Deriving Refinement

Uses Software

• LOTOS
• Z

Cites Work

• ASM refinement and generalizations of forward simulation in data refinement: a comparison
• Incompleteness of relational simulations in the blocking paradigm
• Data refinement and singleton failures refinement are not equivalent
• Relational concurrent refinement. II: Internal operations and outputs
• Specifying and refining internal operations in \(Z\)
• Atomic actions, and their refinements to isolated protocols
• A singleton failures semantics for communicating sequential processes
• Modelling Divergence in Relational Concurrent Refinement
• Data Refinement
• Eternity variables to prove simulation of specifications
• Program development by stepwise refinement
• 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: Introducing extra operations in refinement