Temporal-logic property preservation under Z refinement
From MaRDI portal
Publication:1941860
DOI10.1007/s00165-011-0177-4zbMath1259.68032OpenAlexW2079360995MaRDI QIDQ1941860
Publication date: 22 March 2013
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-011-0177-4
Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Foundations for using linear temporal logic in Event-B refinement ⋮ On the preservation of properties when changing communication models
Uses Software
Cites Work
- Prespecification in data refinement
- A single complete rule for data refinement
- Relational concurrent refinement
- Results on the propositional \(\mu\)-calculus
- Extensional equivalences for transition systems
- Myths about the mutual exclusion problem
- Property preserving abstractions for the verification of concurrent systems
- Testing equivalences for processes
- Forward and backward simulations. I. Untimed Systems
- A singleton failures semantics for communicating sequential processes
- The B-Book
- Data Refinement
- Algebraic Methodology and Software Technology
- ZB 2005: Formal Specification and Development in Z and B
- Unnamed Item
- Unnamed Item
- 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: Temporal-logic property preservation under Z refinement