산업자동화 분야에 널리 사용되는 컨트롤러 PLC는 그래픽 언어 래더 다이어그램(Ladder Diagram: LD)을 사용한다. LD프로그램의 검증을 위해서 검증 조건 생성기 Why를 이용해 증명거리를 생성하고 ...
http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
국문 초록 (Abstract)
산업자동화 분야에 널리 사용되는 컨트롤러 PLC는 그래픽 언어 래더 다이어그램(Ladder Diagram: LD)을 사용한다. LD프로그램의 검증을 위해서 검증 조건 생성기 Why를 이용해 증명거리를 생성하고 ...
산업자동화 분야에 널리 사용되는 컨트롤러 PLC는 그래픽 언어 래더 다이어그램(Ladder Diagram: LD)을 사용한다. LD프로그램의 검증을 위해서 검증 조건 생성기 Why를 이용해 증명거리를 생성하고 정리증명기 Coq으로 증명하는 방법을 보인다. 이런 방식을 LD에 적용하기 위해서는 LD프로그램을 Why의 명세언어로 작성하고 검증명세를 부여해야 한다. 본 논문은 LD프로그램을 Why 명세언어로 변환한 후에 Why를 통해서 LD프로그램을 검증하는 과정을 보여준다.
다국어 초록 (Multilingual Abstract)
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...
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.
목차 (Table of Contents)
MOnCa : 온톨로지 기반 상황 인지 스마트 폰 어플리케이션을 위한 프레임워크
햅틱 렌더링을 위한 거리 영역과 포인트 쉘 기반의 실시간 변형체 충돌 검사
특징점 레이블 간의 지지도 계산에 의한 부분적으로 가려진 이진 객체의 인식
속성 가중치의 지역적 최적화에 의한 유추기반 공수 예측 정확도의 향상