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.
본 논문에서는 시간논리로 사양이 주어진 finite state machine의 검증 방법이 제시되었다. 검증의 기본원리는 refutation 방법과 유사하다. 우선 시간논리로 주어진 사양이 부정 (negation)되고, 그리고 검증기(verifier)는 부정된 사양이 만족되는지를 결정한다. 만약 만족되어 진다면 그 finite state machine은 주어진 사양에 대해서 옳지 않은 것이다. 만약 만족되어지지 않는다면 그 finite state machine은 주어진 사양을 만족하는 것이다. 일반적으로 Model Graph가 시간논리식으로부터 사건의 순서를 알아내는 방법으로 쓰여 왔었다. 그러나 이 방법은 Model Graph를 만들기 위해 시간논리식을 disjunctive 표준형으로 바꿔야한다. 본 논문에서는 사건 순서를 꺼내기 위해 disjunctive 표준형이 필요 없는 Petri Net Modeling 방법을 이용하였다. 부정된 사양은 계층적 치환 방법에 의해 대응하는 Petri Net으로 변환된다. 검증기는 Prolog로 구현되었는데, 그 이유는 Prolog 환경이 검증기가 필요로 하는 pattern matching과 tree traversal 기능을 내재적으로 갖고 있기 때문이다. 마지막으로 RTLL(Register Transfer Level Language) description과 synchronous hardware에 대해 이 방법이 적용됨을 보였다.
