산업자동화 분야에 널리 사용되는 컨트롤러 PLC는 그래픽 언어 래더 다이어그램(Ladder Diagram: LD)을 사용한다. LD프로그램의 검증을 위해서 검증 조건 생성기 Why를 이용해 증명거리를 생성하고 정리증명기 Coq으로 증명하는 방법을 보인다. 이런 방식을 LD에 적용하기 위해서는 LD프로그램을 Why의 명세언어로 작성하고 검증명세를 부여해야 한다. 본 논문은 LD프로그램을 Why 명세언어로 변환한 후에 Why를 통해서 LD프로그램을 검증하는 과정을 보여준다.
A special-purpose microcontroller PLC, widely used in industrial automation, is using a specially designed graphical language LD(Ladder Diagram). This paper proposes a method to use a verification condition generator Why for verifying LD programs. For proof of the verification requirement you can use a theorem prover such as Coq to prove the proof obligations. In order to apply Why to LD programs, LD programs should be represented in the why specification and verification requirements be given. This paper shows the verification process of LD programs by using automatic translation and Why.
