Affordable Access

Construction of Abstract State Graphs with PVS

Authors
  • Graf, Susanne
  • Saidi, Hassen
Publication Date
Jun 22, 1997
Source
HAL-UPMC
Keywords
Language
English
License
Unknown
External links

Abstract

In this paper, we propose a method for the automatic construction of an abstract state graph of an arbitrary system using the Pvs theorem prover.Given a parallel composition of sequential processes and a partition of the state space induced by predicates ϕ1, ..., g4 l on the program variables which defines an abstract state space, we construct an abstract state graph, starting in the abstract initial state. The possible successors of a state are computed using the Pvs theorem prover by verifying for each index i if ϕi or ¬ϕi is a postcondition of it. This allows an abstract state space exploration for arbitrary programs.

Report this publication

Statistics

Seen <100 times