The existence of refinement mappings
A refinement mapping from a lower-level specification \(S_ 1\) to higher- level specification \(S_ 2\) can be used to prove that \(S_ 1\) is a correct implementation of \(S_ 2\)- if such a mapping does exist. The goal of the paper is to find out assumptions about specifications to guarantee the existence of a refinement mapping. A program is represented by a state machine (which may be infinite-state) specifying safety requirements (behaviour satisfies the property if it can be generated by a program); fairness constraints are represented by an arbitrary supplementary condition. A refinement mapping from a specification \(S_ 1\) to a specification \(S_ 2\) is a mapping from state space of \(S_ 1\) to state space of \(S_ 2\) which preserves state machine behaviour and liveness. Three cases when a refinement mapping does not exist are mentioned and it is shown how to overcome these problems by adding auxiliary variables (i.e. by adding internal state components not affecting the visible behaviour) to \(S_ 1\). The main result is a completeness theorem which states that, under three hypotheses about the specifications, if \(S_ 1\) implements \(S_ 2\) then one can add auxiliary, history and prophecy variables to \(S_ 1\) to form an equivalent \(S_ 1^{hp}\) and find a refinement mapping from \(S_ 1^{hp}\) to \(S_ 2\). Some examples demonstrate why these three hypotheses are needed.
- scientific article; zbMATH DE number 3614147 (Why is no real title available?)
- scientific article; zbMATH DE number 3303654 (Why is no real title available?)
- Protocol Verification via Projections
- Proving entailment between conceptual state specifications
- Proving the Correctness of Multiprocess Programs
- Recognizing safety and liveness
- Specifying Concurrent Program Modules
- Network invariants for real-time systems
- Operating system verification---an overview
- Resolution-based approach to compatibility analysis of interacting automata
- A theory of implementation and refinement in timed Petri nets
- Operational specification with joint actions: Serializable databases
- Specifying modules to satisfy interfaces: A state transition system approach
- Critique of the Lake Arrowhead three
- Using mappings to prove timing properties
- Liveness in timed and untimed systems
- Formal verification of a programming logic for a distributed programming language
- A formal theory of simulations between infinite automata
- Set theory for verification. I: From foundations to functions
- Program refinement in fair transition systems
- Property preserving abstractions for the verification of concurrent systems
- Two implementation relations and the correctness of communicating replicated processes
- A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
- Verification, refinement and scheduling of real-time programs
- Relating trace refinement and linearizability
- Dynamic hierarchical reactive controller synthesis
- Conditions of contracts for separating responsibilities in heterogeneous systems
- Finite and infinite implementation of transition systems
- On fairness notions in distributed systems. I: A characterization of implementability
- Fair simulation
- On the complexity of verifying concurrent transition systems
- Verification of schedulability for real-time programs
- Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
- On the limits of refinement-testing for model-checking CSP
- On hierarchically developing reactive systems
- UNITY and Büchi automata
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Temporal prophecy for proving temporal properties of infinite-state systems
- Generalized arrays for Stainless frames
- Synthesizing precise and useful commutativity conditions
- Specifying reversibility with \(\mathrm{TLA}^+\)
- Decomposing data structure commutativity proofs with \(mn\)-differencing
- Abstract semantic diffing of evolving concurrent programs
- Specification and verification of concurrent programs through refinements
- Refinement calculus: A basis for translation validation, debugging and certification
- Precise specification matching for adaptive reuse in embedded systems
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- Comparative branching-time semantics for Markov chains
- Local abstraction refinement for probabilistic timed programs
- Universal extensions to simulate specifications
- Bridging the gap between fair simulation and trace inclusion
- Splitting forward simulations to cope with liveness
- Refinement verification of the lazy caching algorithm
- Programming interfaces and basic topology
- Layout randomization and nondeterminism
- Mutex needs fairness
- New results on timed specifications
- A sound and complete proof technique for linearizability of concurrent data structures
- Guarded transitions in evolving specifications
- Byzantizing Paxos by refinement
- Compositional Abstraction in Real-Time Model Checking
- Design and Verification of Fault-Tolerant Components
- Formal verification for high-assurance behavioral synthesis
- scientific article; zbMATH DE number 3943005 (Why is no real title available?)
- A distributed resource allocation algorithm for many processes
- Combining decision procedures by (model-)equality propagation
- Synthesis of Reactive(1) designs
- scientific article; zbMATH DE number 1949612 (Why is no real title available?)
- scientific article; zbMATH DE number 1759495 (Why is no real title available?)
- Dynamic networks of heterogeneous timed machines
- Starvation-free mutual exclusion with semaphores
- Requirements, specifications, and minimal refinement
- Verifying visibility-based weak consistency
- RustHorn: CHC-based verification for Rust programs
- Heterogeneous and asynchronous networks of timed systems
- Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
- Action systems in incremental and aspect-oriented modeling
- scientific article; zbMATH DE number 7407781 (Why is no real title available?)
- Combining Decision Procedures by (Model-)Equality Propagation
- Queue based mutual exclusion with linearly bounded overtaking
- Automated verification and refinement for physical-layer protocols
- Simulation Refinement for Concurrency Verification
- Completeness of ASM refinement
- Simulation refinement for concurrency verification
- Completeness of fair ASM refinement
- Layout Randomization and Nondeterminism
- Understanding, Explaining, and Deriving Refinement
- Minimal refinements of specifications in modal and temporal logics
- Minimal refinements of specifications in modal and temporal logics
- Axioms for real-time logics
- Refinement and state machine abstraction
- On the complexity of verifying concurrent transition systems
- Fair simulation
- I/O automata in Isabelle/HOL
- Incompleteness of relational simulations in the blocking paradigm
- Simulation relations and applications in formal methods
- Why3-do: the way of harmonious distributed system proofs
- Liminf progress measures
- Synthesizing history and prophecy variables for symbolic model checking
- RHLE: modular deductive verification of relational \(\forall \exists\) properties
- Model-based construction and verification of critical systems using composition and partial refinement
- Software Verification of Hyperproperties Beyond k-Safety
- Efficient loop conditions for bounded model checking hyperproperties
- A new approach for active automata learning based on apartness
- Some extensions to propositional mean-value calculus: expressiveness and decidability
- Towards applying the composition principle to verify a microkernel operating system
- Hume box calculus: Robust system development through software transformation
This page was built for publication: The existence of refinement mappings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q805251)
