Automatic Extraction of Pre- and Postconditions from Z Specifications

Formal methods are especially useful in writing requirements specification of safety-critical systems due to their unambiguous and precise syntax and semantics. They also hold a special place in software testing phase because formal specifications provide a good opportunity for automation of the testing process. Many formal specification based software testing techniques use Finite State Machines (FSMs) because they are quite useful in test sequencing, test case generation and test case execution. Therefore, extraction of a FSM from the formal specification is an interesting problem. Although some techniques for FSM generation from formal specifications exist in the literature but none of them is fully automated. A major challenge in automatic generation of a FSM from Z specification is the identification and extraction of pre- and postconditions, since it is difficult to separate the input and output predicates when intermediate variables are used in the specification. In this paper, we present an automated approach to separate input and output predicates and extract pre- and postconditions from these predicates for a given Z operation schema. The proposed approach is supported by a tool and is also demonstrated on an example.