Towards Model Checking of Finite State Machines Extended with memory through Refinement

G.Eleftherakis, and P. Kefalas

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