Coq에서의 실시간 분산 시스템 검증을 위한 네트워크 및 운영체제 행동의 정형 모델 정의 


47권  11호, pp. 1071-1077, 11월  2020
10.5626/JOK.2020.47.11.1071


PDF

  요약

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


  통계
2022년 11월부터 누적 집계
동일한 세션일 때 여러 번 접속해도 한 번만 카운트됩니다. 그래프 위에 마우스를 올리면 자세한 수치를 확인하실 수 있습니다.
  논문 참조

[IEEE Style]

Y. Kim and C. Hur, "Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq," Journal of KIISE, JOK, vol. 47, no. 11, pp. 1071-1077, 2020. DOI: 10.5626/JOK.2020.47.11.1071.


[ACM Style]

Yoonseung Kim and Chung-Kil Hur. 2020. Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq. Journal of KIISE, JOK, 47, 11, (2020), 1071-1077. DOI: 10.5626/JOK.2020.47.11.1071.


[KCI Style]

김윤승, 허충길, "Coq에서의 실시간 분산 시스템 검증을 위한 네트워크 및 운영체제 행동의 정형 모델 정의," 한국정보과학회 논문지, 제47권, 제11호, 1071~1077쪽, 2020. DOI: 10.5626/JOK.2020.47.11.1071.


[Endnote/Zotero/Mendeley (RIS)]  Download


[BibTeX]  Download



Search




Journal of KIISE

  • ISSN : 2383-630X(Print)
  • ISSN : 2383-6296(Electronic)
  • KCI Accredited Journal

사무국

  • Tel. +82-2-588-9240
  • Fax. +82-2-521-1352
  • E-mail. chwoo@kiise.or.kr