Automated generation of finite state machine from object-oriented formal specifications

Finite state automata are widely used in specification-based testing. However, the existing specification- based testing techniques do not fully automate the generation of an FSM from a formal specification. Major challenges in automatic generation of FSM are the identification of disjoint states and transitions from the implicit pre- and postconditions of operations specified in a formal language like Z or Object-Z. It is important to extract pre- and postconditions from the specification because they form the basis for identification of pre- and post-states of the transitions of an FSM. In this paper, we present an automated approach to construction of an FSM from Object-Z formal specification. The proposed approach is supported by a tool and is also demonstrated on an example.