Coq에서의 실시간 분산 시스템 검증을 위한 네트워크 및 운영체제 행동의 정형 모델 정의 (Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq)

서지정보

· 발행기관 : 한국정보과학회
· 수록지 정보 : 정보과학회논문지 / 47권 / 11호 / 1071 ~ 1077페이지
· 저자명 : 김윤승, 허충길

초록

정형 검증을 적용하여 분산 시스템의 안전성을 높이는 것은 중요한 과제이다. 분산 시스템 중 항공, 의료기기와 같은 안전 우선 시스템은 안전성의 위협이 큰 사고와 직결될 수 있다. 하지만 분산 시스템을 정형 검증하기 위해서는 소프트웨어의 실행 의미뿐만 아니라, 소프트웨어를 실행시키는 운영체제와 메시지를 전달하는 네트워크의 환경 등에 대한 기술이 필요하다. 우리는 Coq 증명 보조 도구 안에서 네트워크와 운영체제의 추상적인 행동에 대한 모델을 정의하였다. 이 모델은 단계적으로 네트워크 각 지역의 실행 규칙을 제시하고, 이로부터 전체 시스템의 행동을 구성한다. 우리는 이 모델이 실제로 분산 시스템 검증에 유용하게 사용될 수 있음을 보이기 위해 간단한 서버-클라이언트 시스템 검증을 수행하였으며, 이후 실용적인 소프트웨어 검증에 적용되기를 기대하고 있다.

영어초록

Improving the safety and reliability of distributed systems using formal verification methods is an urgent problem. As many of these distributed systems are safety-critical, such as medical or avionics systems, failures of these systems may cause catastrophic results. However, applying formal verification to distributed systems requires not only execution semantics in software, but also behavioral models of the environments, including the operating systems and network involved. We designed a formal abstract model of network and operating system behaviors with the Coq proof assistant. This model consists of local-site execution semantics that model a single computer, the composition of these local-site semantics along with a message exchange model constitutes the global system semantics. We applied and tested this model to verify its applicability when used in a simple server-client system. We expect this model to be used in the verification of practical systems.

참고자료

· 없음