[레포트(report) ] 航空기에서 경고 계통 간단한 Auto Pilot 시스템의 정형명세 및 검증
페이지 정보
작성일 23-05-05 04:59
본문
Download : 항공기에서 경고 계통 - 간단한 Auto-Pilot 시스템의 정형명세 및 검증.hwp
따라서 시스템의 개발에 있어서 정확성과 안전성을 보장하기 위해서 많은 testing을 시도하고 있다. 이러한 단점을 해결하기 위해 본 논문에서는 간단한 Auto-pilot 시스템을 statechart로 정형명세하고 정형 검증 언어인 SMV 및 PROMELA로 변환하여 검증하는 방법에 대해 논한다.
레포트 항공기에서 경고 계통 간단한 Auto Pilot 시스템의 정형명세 및 검증
간단한 Auto-Pilot 시스템의 정형명세 및 검증 (Formal Sp...
설명
레포트 > 기타
[레포트(report) ] 航空기에서 경고 계통 간단한 Auto Pilot 시스템의 정형명세 및 검증
간단한 Auto-Pilot 시스템의 정형명세 및 검증 (Formal Sp...
간단한 Auto-Pilot 시스템의 정형명세 및 검증 (Formal Specification and Verification of Simple Auto-Pilot System) 박명환 방기석 남원홍 최진영 고려대학교 컴퓨터학과 요약 Statechart는 다른 정형 명세와는 달리 그림으로 시스템을 명세하기 때문에 정형기법에 익숙하지 않은 사람도 쉽게 이해할 수 있다. 그러나명세가 올바르게 되었는지 증명하는 정형 검증의 기능이 없다. 이러한 문제를 해결하기 위해서 최근에는 정형기법(Formal method)[1]을 이용해서 시스템의 설계단계부터 그 안정성을 확인하려는 노력을 가하고 있다. 특히 원자력 발전소나 비행기 컨트롤 시스템과 같은 safety critical system의 경우 작은 오류가 시스템 전체 및 사용자에게 매우 위험한 결과를 초래할 수 있는 것이 사실이다. 정형기법은 수학과 논리학을 기반으로 하여 시스템의 동작을 표현하는 정형명세(Formal specification)와 명세된 시스템이 만족해야 할 特性(특성)(property)을 역시 논리적인 방법을 이용해서 증명하는 정형검증(Formal verification)으로 이루어져 있다. 또한 시스템의 동작을 보다 명확하고 가시적으로 시뮬레이션 할 수 있는 장점(長點)이 있다. 그러나 이러한 testing에 들어가는 시간과 비용이 시스템의 크기에 비례해서 기하급수적으로 증가하기 때문에 대부분의 시스템이 이러한 안정성을 완벽하게 보장하지 못하고 있는 현실이다.Ⅰ. 서론 시스템이 복잡해지고 대형화되면서 그 정확성이 더욱 중요하게 대두되고 있다. 이번 연구에서는 많은 정형 명세 방법 중 시스템의 ...
순서
Download : 항공기에서 경고 계통 - 간단한 Auto-Pilot 시스템의 정형명세 및 검증.hwp( 38 )
다.
