Generating finite-state abstractions of reactive systems using decision procedures
Lecture notes in computer sciencePublished 1 January 1998Open access
Michael A. Colón, Tomás E. Uribe
Citations92
SJR quartileQ2
SJR score0.35
SNIP0.55
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
An algorithm that uses decision procedures to generate finite-state abstractions of possibly infinite-state systems that compositionally abstracts the transitions of the system, relative to a given, fixed set of assertions.
Abstract
We present an algorithm that uses decision procedures to generate finite-state abstractions of possibly infinite-state systems. The algorithm compositionally abstracts the transitions of the system, relative to a given, fixed set of assertions. Thus, the number of validity checks is proportional to the size of the system description, rather than the size of the abstract state-space. The generated abstractions are weakly preserving for ∀CTL temporal properties. We describe several applications of the algorithm, implemented using the decision procedures of the Stanford Temporal Prover (STeP).
Keywords
Computer Science
Abstract interpretation
6,131 Citations1977Patrick Cousot, Radhia Cousot
Lecture notes in computer scienceSymbolic model checking
2,843 Citations1996Emma L. Clarke, K. McMillan +2 more
Using symbolic model checking techniques it is possible to verify industrial-size finite state systems and models with more than 10120 states have been verified using special techniques.
Symbolic Model Checking
1,645 Citations1993Kenneth L. McMillan
The symbolic model checking technique revealed subtle errors in this protocol, resulting from complex execution sequences that would occur with very low probability in random simulation runs, and an alternative method is developed for avoiding the state explosion in the case of asynchronous control circuits.
Lecture notes in computer scienceConstruction of abstract state graphs with PVS
1,471 Citations1997Susanne Graf, Hassen Saı̈di
This paper proposes a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.
ACM Transactions on Programming Languages and SystemsModel checking and abstraction
1,217 Citations1994Edmund M. Clarke, Orna Grümberg +1 more
Using techniques similar to those involved in abstract interpretation, an abstract model of a program is constructed without ever examining the corresponding unabstracted model, and it is shown how this abstract model can be used to verify properties of the original program.
Medical Entomology and ZoologyTemporal Verification of Reactive Systems: Safety
945 Citations1995Zohar Manna, Amir Pnueli
This paper presents a meta-language for estimating Satisfiability over a Finite-State Program: Examples and some examples of how such a program might be implemented in a number of different programming languages.
Temporal and Modal Logic.
823 Citations1990E. Allen Emerson
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.
Formal Methods in System DesignProperty preserving abstractions for the verification of concurrent systems
357 Citations1995Claire Loiseaux, Susanne Graf +4 more
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.
Theoretical Computer ScienceAutomatic generation of invariants and intermediate assertions
155 Citations1997Nikolaj Bjørner, Anca Browne +1 more
Two dual approaches find solutions to verifying temporal specifications of reactive and concurrent systems: the bottom-up method performs an abstract forward propagation of the system, generating auxiliary properties; the top-down method performsAn abstract backward propagation to strengthen given properties.
Lecture notes in computer scienceExperiments in theorem proving and model checking for protocol verification
147 Citations1996Klaus Havelund, Natarajan Shankar
This work describes a series of protocol verification experiments culminating in a methodology where theorem proving is used to abstract out the sources of unboundedness in the protocol to yield a skeletal protocol that can be verified using model checking.
Lecture notes in computer scienceThe bounded retransmission protocol must be on time!
121 Citations1997Pedro R. D’Argenio, Joost-Pieter Katoen +2 more
It is investigated to what extent real-time aspects are important to guarantee the protocol's correctness and the Spin and Uppaal model checking for this purpose is used.
Lecture notes in computer scienceSTeP: Deductive-algorithmic verification of reactive and real-time systems
113 Citations1996Nikolaj Bjørner, Anca Browne +6 more
The Stanford Temporal Prover, STeP, combines deductive methods with algorithmic techniques to verify linear-time temporal logic specifications of reactive and real-time systems.
Lecture notes in computer scienceVerification of real-time systems by successive over and under approximation
65 Citations1995David L. Dill, Howard Wong-Toi
An algorithm is presented which uses simple heuristics to automatically generate finer abstractions until the approximations correctly answer the verification problem of finite-bounded systems.
Lecture notes in computer scienceModel checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving
58 Citations1995Jürgen Dingel, Thomas Filkorn
This paper contains a complete case study to prove safety and liveness of an implementation of a scheduler for the readers/writers problem which uses unbounded queues and sets.
Lecture notes in computer scienceTemporal verification of simulation and refinement
52 Citations1994Yonit Kesten, Zohar Manna +1 more
The paper presents temporal logic methods for proving simulation and refinement relations between programs and relates them to inclusion relations between computations and observations of the compared systems.
Lecture notes in computer scienceDeductive model checking
49 Citations1996Henny B. Sipma, Tomás E. Uribe +1 more
Symbolic approximations for verifying real-time systems
45 Citations1995Howard Wong-Toi
A generic iterative approximation algorithm is described that is designed to exploit the fact that not all the details of a system need to be considered in order to prove it correct, and to verify that systems with hard real-time bounds satisfy timed safety properties.
Clocked Transition Systems
38 Citations1996Zohar Manna, Amir Pnueli
This paper presents a new computational model for real-time systems, called the clocked transition system model, a development of the previous timed transition model, where some of the changes are inspired by the model of timed automata.
Lecture notes in computer scienceAutomatic abstraction techniques for propositional μ-calculus model checking
27 Citations1997Abelardo Pardo, Gary D. Hachtel
An abstraction/refinement paradigm for the full propositional μ-calculus is presented, with necessary conditions for conservative verification provided, along with a fully automatic symbolic model checking abstraction algorithm.
Lecture notes in computer scienceA practical integration of first-order reasoning and decision procedures
24 Citations1997Nikolaj Bjørner, Mark E. Stickel +1 more
A procedure for proving the validity of first-order formulas in the presence of decision procedures for an interpreted subset of the language, implemented as part of STeP, a tool for the formal verification of reactive systems.
Data Archiving and Networked Services (DANS)Practical symbolic model checking of the full µ-calculus using compositional abstractions
18 Citations1995Peter Kelb, Dennis Dams +1 more