MPI-I-1999-2-006
A deductive model checking approach for hybrid systems
Nonnengart, Andreas
November 1999, 40 pages.
.
Status: available - back from printing
In this paper we propose a verification method for hybrid systems
that is based on a successive elimination of the various system
locations involved. Briefly, with each such elimination we compute
a weakest precondition (strongest postcondition) on the predecessor
(successor) locations such that the property to be proved cannot be
violated.
This is done by representing a given verification problem as a
second-order predicate logic formula which is to be solved (proved
valid) with the help of a second-order quantifier elimination method.
In contrast to many ``standard'' model checking approaches
the method as described in this paper does not perform a forward or
backward reachability analysis.
Experiments show that this approach is particularly interesting
in cases where a standard reachability analysis would require to travel
often through some of the given system locations.
In addition, the approach offers possibilities to proceed where
``standard'' reachability analysis approaches do not terminate.
-
- Attachement: MPI-I-1999-2-006.ps (521 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-2-006
BibTeX
@TECHREPORT{NonnengartMPI-I-1999-2-006,
AUTHOR = {Nonnengart, Andreas},
TITLE = {A deductive model checking approach for hybrid systems},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-1999-2-006},
MONTH = {November},
YEAR = {1999},
ISSN = {0946-011X},
}