- 증명보조기 Coq을 이용한 래더 다이어그램 의미구조의 정형화
- ㆍ 저자명
- 신승철,Shin. Seung-Cheol
- ㆍ 간행물명
- 정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용
- ㆍ 권/호정보
- 2010년|37권 1호|pp.54-59 (6 pages)
- ㆍ 발행정보
- 한국정보과학회
- ㆍ 파일정보
- 정기간행물| PDF텍스트
- ㆍ 주제분야
- 기타
이 논문은 한국과학기술정보연구원과 논문 연계를 통해 무료로 제공되는 원문입니다.
산업자동화 분야에는 특수목적 마이크로콘트롤러인 PLC가 널리 사용된다. PLC 프로그램 분석과 검증을 위한 연구에서 우선적으로 해야 할 일은 PLC 프로그래밍 언어의 의미구조를 정형적으로 제시하는 것이다. 본 논문은 PLC 프로그래밍에 널리 사용하는 LD 언어의 의미구조를 정의한다. LD 언어는 그래픽 언어이기 때문에 먼저 텍스트 언어 Symbolic LD로 구문구조를 정형화한 다음에, Symbolic LD에 대한 의미구조를 정의할 수가 있다. 본 논문은 Symbolic LD의 의미구조를 자연 의미구조 기법으로 정의하고, 증명 보조기 Coq을 이용하여 정형화하였다.
Special-purpose microcontrollers PLCs have been widely used in the area of industrial automation. For the research of analysis and verification for PLC programs, first of all we have to specify formal sematics of PLC programming languages. This paper defines formally the operational semantics of LD language. After we transform the graphical language LD into its textual representation Symbolic LD, we give semantics of Symbolic LD since LD language is a graphical language. This paper defines the natural sematics of Symbolic LD and formalizes it in Coq proof assistant.