Formal Verification of Generalised State Machines

The demand for more complex software is constantly increasing while at the same time the need for reliability leads modern software engineering to use more formally based development techniques. One of the most successfully employed formalisms to address the reliability issue were Finite State Machines (FSM) but they are too simple to capture the modelling needs of modern software that normally require manipulation of non-trivial data structures. X-machines is a formal method that provides such a data structure in form of a memory. On the other hand, FSM models are suitable for verification through model checking, i.e. to prove that certain properties are satisfied by a system model. However, with existing logics, it is obscure how one can describe properties that refer to the memory structure of an X-machine. This paper describes how a new logic, namely XmCTL, which extends temporal logic with memory quantifiers, facilitates model checking of X-machine models. XmCTL is defined and its use is demonstrated through the verification of a steam-boiler system which acts as a case study for our contribution.