FBD 및 LD로 구현된 PLC 프로그램의 Verilog 변환을 통한 정형검증Formal verification of PLC programs in FBD and LD via verilog translation
본 연구에서는 산업용 컴퓨터의 일종으로 제어 시스템에 널리 이용되는 PLC에서 실행되는 FBD 및 LD로 작성된 XML기반 PLC프로그램에 대한 정형검증 기법에 대하여 제안한다. 이를 위해 FBD 및 LD로 명세된 PLC 프로그램을 자동으로 Verilog 모델로 변환하고 이를 Cadence SMV로 모델체킹한다. 자동화 지원 도구로 PLCVerifier를 개발하였다. PLCVerifier는 FBD를 정형검증 할 수 있는 기존 결과물인 FBDVerifier에 비하여 검증 대상 FBD의 범위를 대폭 확장하였으며 LD도 정형 검증할 수 있다. FBD와 LD는 PLC를 위한 IEC 61131-3 표준 5가지 언어 중 산업 현장에서 가장 선호 되는 언어들이다. 따라서 FBD와 LD를 모두 정형 검증 할 수 있는 기법은 매우 중요하다. 또한 이 도구는 PLCopen의 표준 XML 포맷을 입력으로 사용하여 표준 XML 포맷을 지원하는 PLC 프로그래밍 도구, 테스팅, 시뮬레이션 도구와 상호 연동 될 수 있다. PLCVerifier는 PLC프로그램을 위한 국제 표준 IEC61131-3 5가지 언어 중 PLC 프로그램에 자주 이용되는 FBD와 LD 프로그램 모두를 검증할 수 있다. 또한 PLCVerifier는 POSCON pSET과의 호환을 위하여 pSET 포맷을 PLCopen 표준 XML포맷으로 자동 변환하는 기능도 제공한다.
- Advisors
- 배두환researcher; Bae, Doo-Hwanresearcher
- Description
- 한국과학기술원 : 전산학전공,
- Publisher
- 한국과학기술원
- Issue Date
- 2009
- Identifier
- 308889/325007 / 020073068
- Language
- kor
- Description
학위논문(석사) - 한국과학기술원 : 전산학전공, 2009.2, [ vi, 52 p. ]
- Keywords
Formal Method; Formal Verification; FBD; LD; 정형 기법; 정형 검증; FBD; LD; Formal Method; Formal Verification; FBD; LD; 정형 기법; 정형 검증; FBD; LD
- Appears in Collection
- CS-Theses_Master(석사논문)
- Files in This Item
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.