Towards Model Checking of Finite State Machines Extended
with memory through Refinement
Abstract: Model checking is a successful verification
technique for models expressed as finite state machines (FSM). Although
FSM are able to describe the control part of a system, they lack the ability
to efficiently describe data. As a consequence, FSM are not suitable to
model several systems, which include complex data structures. This paper
proposes a model checking technique for a type of FSM, namely the X-machine,
which extends the FSM in two ways: (a) memory attached to each state, and
(b) functions describing transitions between states. These features give
the ability to the software engineer to intuitively as well as formally
create a model of a system and then automatically check if this model has
certain desired properties. The use of this formal method in the development
of systems in safety critical domains can assure that the final product
is valid with respect to the user requirements by revealing errors during
the development life cycle. The proposed model checking technique is accompanied
by an example, which demonstrates the use of X-machines in specification
and verification.
Keywords: Formal Modeling, Specification, Verification
Appeared in: In Proceedings of the 5th World MultiConference
on Circuits, Systems, Communications & Computers (CSCC 2001), Crete,
July 2001
Available: Hardcopy on request from the authors.
Back
to Dept. of Computer Science, CITY Liberal Studies
Back
to Petros Kefalas home page