SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Construction of abstract state graphs with PVS
 by Dr. Hassen Sadi & Sussane Graf.

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....,φi 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.
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy