Combined Algorithm for Approximating a Finite State Abstraction of a Large System

We study the problem of abstracting a finite state machine (FSM) from a given software system whose operational behavior is described by an abstract state machine (ASM). ASMs are typically infinite state systems and the problem of extracting a finite abstraction, the true FSM, from an ASM with respect to a given abstraction function is in general undecidable. To approximate the true FSM we utilize the two key features of ASMs, that they are executable and have precise mathematical semantics that allows for a symbolic representation of the overall system behavior. On one hand, executability of ASMs is exploited for true computation path exploration; this yields an under-approximation of the true FSM. On the other hand, the symbolic representation of the system behavior enables us to use theorem proving to exclude impossible computation paths; this yields an over-approximation of the true FSM. In this paper we discuss an algorithm that combines both into a unified approach.