Programmable Logic Controller (PLC) is an industrial computer applied to wide range of control system. In this paper, we suggest formal verification method of XML based PLC program implemented with FBD and LD through Verilog translation. To verify FBD and LD program, XML based FBD and LD programs are translated automatically into Verilog model. And then we conduct model checking of Verilog model with Cadence SMV. PLCVerifier was developed to support automatic translation of FBD and LD programs. PLCVerifier enables us to verify more various FBD programs than FBDVerifier which is developed in previous research. Also PLCVerifier allows us to verify LD program. PLC experts commonly use FBD and LD together. Therefore it is important that verification tool of PLC program can support FBD and LD together. PLCVerifier is compatible with PLCopen standard XML based programming, testing and simulation tools, because PLCVerifier supports PLCopen standard XML as input format. For more usefulness of PLCVerifier, PLCVerifier can translate automatically POSCON pSET format into PLCopen standard XML format.
본 연구에서는 산업용 컴퓨터의 일종으로 제어 시스템에 널리 이용되는 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포맷으로 자동 변환하는 기능도 제공한다.
