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