서지주요정보
Verification of finite state machine using temporal logic specification = 시간논리 사양으로 주어진 유한상태 Machine 의 검증
서명 / 저자 Verification of finite state machine using temporal logic specification = 시간논리 사양으로 주어진 유한상태 Machine 의 검증 / Seh-Woong Jeong.
저자명 Jeong, Seh-Woong ; 정세웅
발행사항 [서울 : 한국과학기술원, 1987].
Online Access 제한공개(로그인 후 원문보기 가능)원문

소장정보

등록번호

4104486

소장위치/청구기호

학술문화관(문화관) 보존서고

MEE 8774

SMS전송

도서상태

이용가능

대출가능

반납예정일

초록정보

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에 대해 이 방법이 적용됨을 보였다.

서지기타정보

서지기타정보
청구기호 {MEE 8774
형태사항 [ii], 71, [4] p. : 삽도 ; 26 cm
언어 영어
일반주기 저자명의 한글표기 : 정세웅
지도교수의 영문표기 : Myung-Hwan Kim
지도교수의 한글표기 : 김명환
학위논문 학위논문(석사) - 한국과학기술원 : 전기 및 전자공학과,
서지주기 Includes references
주제 Petri nets.
Negation (Logic)
RTL (Computer program language)
그래프 이론. --과학기술용어시소러스
시간 논리. --과학기술용어시소러스
논리 설계. --과학기술용어시소러스
Graph theory --Data processing.
QR CODE qr code