Verification of finite state machine using temporal logic specification

Abstract

A method for verification of finite state machines specified by temporal logic is suggested. The basic principle is closely related to the refutation method. The given specification by temporal logic is first negated and then the verifier decides whether the negated specification is satisfiable or not. If it is satisfiable, the finite state machine is not correct with regard to the given specification. Otherwise, the machine satisfies the given specification. Conventionally, the model graph has been used for the extraction of event sequences from the temporal logic formula. However, the temporal logic formula should be transformed into the disjunctive normal form for the model graph construction. In this thesis, Petri net model in which the normal form transformation is not necessary, is used to extract the event sequence which is represented by the corresponding firing sequences. The negated specification is converted into the equivalent Petri net model by using a hierarchical substitution technique. The verifier is implemented in Prolog because the Prolog environment provides inherently tree traversal and pattern matching mechanism which are required for the verifier. Finally, this method is shown to be applied to verify synchronous hardware given by net list form and RTLL (Register Transfer Level Language) description.