Property preserving abstractions for the verification of concurrent systems
Formal Methods in System DesignPublished 1 January 1995
Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, Saddek Bensalem, David K. Probst
Citations357
SJR quartileQ3
SJR score0.34
SNIP1.03
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
Results are given on the preservation of properties expressed in sublanguages of the branching time μ-calculus when two systemsS andS' are related via (α, γ)-simulations, using simulations parameterized by Galois connections.
Abstract
We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections (α, γ), relating the lattices of properties of two systems. We propose and study a notion of preservation of properties expressed by formulas of a logic, by a function α mapping sets of states of a systemS into sets of states of a systemS'. We give results on the preservation of properties expressed in sublanguages of the branching time μ-calculus when two systemsS andS' are related via (α, γ)-simulations. They can be used to verify a property for a system by verifying the same property on a simpler system which is an abstraction of it. We show also under which conditions abstraction of concurrent systems can be computed from the abstraction of their components. This allows a compositional application of the proposed verification method. This is a revised version of the papers [2] and [16]; the results are fully developed in [28].
Keywords
Computer Science
IEEE Transactions on ComputersGraph-Based Algorithms for Boolean Function Manipulation
8,829 Citations1986Bryant
Experimental results from applying a new data structure for representing Boolean functions and an associated set of manipulation algorithms to problems in logic design verification demonstrate the practicality of this approach.
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
ACM Transactions on Programming Languages and SystemsAutomatic verification of finite-state concurrent systems using temporal logic specifications
3,555 Citations1986E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems.
Systematic design of program analysis frameworks
1,598 Citations1979Patrick Cousot, Radhia Cousot
The systematic and correct design of program analysis frameworks with respect to a formal semantics is devoted to the main elements of the lattice theoretic approach to approximate semantic analysis of programs.
On a Decision Method in Restricted Second Order Arithmetic
1,277 Citations1990J Büchi
Formal Aspects of ComputingAn Introduction to Input/Output Automata
1,024 Citations2026Nancy Lynch, Mark R. Tuttle
This paper is intended to introduce researchers to the input output automaton model and examines several illustrative examples concerning candy vending machines and other uses of the model.
Journal of the ACM“Sometimes” and “not never” revisited
996 Citations1986E. Allen Emerson, Joseph Y. Halpern
A language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined and the expressive power of a number of sublanguages is compared.
Theoretical Computer ScienceCalculi for synchrony and asynchrony
898 Citations1983Robin Milner
It is shown that the author's Calculus of Communicating Systems (1980), which is an asynchronous model, is derivable from the calculus presented here, which models both synchronous and asynchronous computation.
Theoretical Computer ScienceThe existence of refinement mappings
734 Citations1991Martı́n Abadi, Leslie Lamport
The authors consider specifications consisting of a state machine that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements and show that under reasonable assumptions about the specifications, if S/ Sub 1/ implements S/sub 2/, then by adding auxiliary variables to S/ sub 1/ one can guarantee the existence of a refinement mapping.
Theoretical Computer ScienceThe temporal semantics of concurrent programs
701 Citations1981Amir Pnueli
It is demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.
Parallel Program Design
670 Citations1989K. Mani Chandy
My goal is to propose a set of questions that I think are important and to work on these questions with J. J. Misra, a researcher at the University of California, Berkeley.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)An algebraic definition of simulation between programs
530 Citations1971Robin Milner
A technique is given and illustrated for proving simulation and equivalence of programs; there is an analogy with Floyd''s technique for proving correctness of programs.
Lecture notes in computer scienceComparing the Galois connection and widening/narrowing approaches to abstract interpretation
421 Citations2006Patrick Cousot, Radhia Cousot
The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices.
Automatic verification of finite state concurrent system using temporal logic specifications
412 Citations1983E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.
ACM Transactions on Programming Languages and SystemsAbstract interpretation of reactive systems
379 Citations1997Dennis Dams, Rob Gerth +1 more
This article extends Abstract Interpretation to the analysis of both existential and universal reactive properties, as expressible in the modal -calculus, and shows how abstract models may be constructed by symbolic execution of programs.
Model checking and abstraction
348 Citations1992Edmund M. Clarke, Orna Grümberg +1 more
A method for using abstraction to reduce the complexity of temporal logic model checking by constructing an abstract model of a program without ever examining the corresponding unabstracted model is described.
A hierarchy of temporal properties
186 Citations1987Zohar Manna, Amir Pnueli
A classification of temporal properties into a hierarchy which refines the known safety-liveness classification of properties, and recognizes the classes of safety, guarantee, persistence, fairness, and hyper-fairness.
A hierarchy of temporal properties (invited paper, 1989)
163 Citations1990Zohar Manna, Amir Pnueli
This work proposes a classification of temporal properties into a hierarchy, and relates this classification to the well known safety[iweness classification, and shows that in some sense the two are orthogonal to one another.
Lecture notes in computer scienceAnalysis of discrete event coordination
141 Citations1990Robert P. Kurshan
A reduction is a validity-preserving transformation by which a complex assertion about a complex model may be replaced by a simpler assertion aboutA simpler model in such a way that the validity of the latter implies thevalidity of the former.
Lecture notes in computer scienceModel checking and modular verification
121 Citations1991Orna Grümberg, David E. Long
Lecture notes in computer scienceProperty preserving simulations
104 Citations1993Saddek Bensalem, Ahmed Bouajjani +2 more
Property preserving transformations for reactive systems are studied by using -simulations which are simulations parameterized by a Galois connection relating the lattices of properties of two systems.
"Sometimes" and "not never" revisited
93 Citations1983E. Allen Emerson, Joseph Y. Halpern
This paper re-examines Lamport's arguments, points out some technical difficulties with the formalism of [LA80], and concludes that, while branching time logic issuitable for reasoning about nondeterministic programs, linear timelogic is preferable for reasoningAbout concurrent programs.
Lecture notes in computer scienceSafety for branching time semantics
83 Citations1991Ahmed Bouajjani, J. C. Fernandez +3 more
It is shown that verifying safety properties on trees reduces to simulation testing and a safety preorder is proposed for this semantics based on simulation and dealing with silent actions.
Lecture notes in computer scienceProperty preserving homomorphisms of transition systems
47 Citations1984Joseph Sifakis
This work studies functions preserving properties of transition systems described by formulas of a logic by studying how these properties are preserved in the real world.
Lecture notes in computer scienceA tool for symbolic program verification and abstraction
46 Citations1993Susanne Graf, Claire Loiseaux
A verification tool takes boolean programs of guarded commands as input and allows to construct an abstract program of the same form obtained using an abstraction relation given by a boolean expression on “concrete”' and “abstract” variables.
Lecture notes in computer scienceVerification of a distributed cache memory by using abstractions
41 Citations1994Susanne Graf
This paper verifies a distributed cache memory system by using the following general verification method: verify the properties characterizing a complex system on some small finite abstraction of it, obtained as a composition of abstractions of each component of the system.
Lecture notes in computer scienceOn decomposing and refining specifications of distributed systems
26 Citations1990Bengt Jönsson
This paper presents existing techniques that reduce the verification problem to classical verification conditions, using a notation with guarded assignment statements, and examines conditions under which the techniques are complete.
RAIRO Informatique théoriqueData types as lattices : retractions, closures and projections
17 Citations1977Luis E. Sanchis
This paper presents the mathematical principles of lattice theory oriented toward the theory of computation, and attempted is a systematic treatment of this lattices theory that involves the definition of data structures.
Elsevier eBooksSpecification and Validation of a Simple Overtaking Protocol using LOTOS
9 Citations1992Patrik Ernberg, Lars‐Åke Fredlund +1 more
A specification of a simple Overtaking protocol for vehicles using the Formal Description Technique LOTOS is presented and the applicability of existing tools in the context of this example is discussed.
Lecture notes in computer scienceVarious simulations and refinements
7 Citations1990He Jifeng
The paper provides a rigorous method for the formal development of communicating processes by integrating the event-based approach with the state-based technique by investigating various kinds of process refinement and their corresponding simulation rules.