المفاهيم الأساسية
실제 사용을 위해 배포된 다양한 분야의 검증 소프트웨어 시스템들을 분석하여 산업계가 형식 검증 기술과 도구로부터 얻을 수 있는 교훈을 제시한다.
الملخص
이 논문은 실제로 배포되어 사용되고 있는 다양한 분야의 검증 소프트웨어 시스템들을 분석한다.
-
서론에서는 소프트웨어 정확성의 중요성과 형식 검증 기술의 실용성에 대한 논란을 소개한다. 이 논문은 이 문제에 대한 객관적인 근거를 제공하기 위해 실제 배포된 검증 시스템들을 분석한다.
-
2장에서는 분석 대상 시스템 선정 기준과 분석 기준을 설명한다.
3-4장에서는 형식 검증의 기본 개념과 다양한 검증 접근법을 소개한다.
5장에서는 검증 프로세스의 전반적인 맥락을 설명한다. 검증 프로파일과 검증 체계에 대해 설명한다.
6장은 이 논문의 핵심으로, 선정된 개별 시스템들을 분석한다. 각 시스템의 범위, 구성 요소, 검증 속성, 프로젝트 맥락, 주요 결정 사항, 도구 스택, 스타일, 소프트웨어 특성, 프로젝트 특성, 교훈 등을 설명한다.
7장에서는 전반적인 교훈과 한계, 그리고 산업계로의 일반화 가능성을 논의한다.
الإحصائيات
CompCert 컴파일러는 135,000줄의 코드로 구현되었으며, 6 인년의 개발 및 검증 노력이 투입되었다.
CakeML 컴파일러는 100,000줄의 코드로 구현되었다.
Vericert 컴파일러는 3,630줄의 코드로 구현되었으며, 1.5 인년의 개발 및 검증 노력이 투입되었다.
Vermillion 컴파일러는 8,000줄의 코드로 구현되었으며, 0.75 인년의 개발 및 검증 노력이 투입되었다.
EiffelBase2 라이브러리는 9,370줄의 코드로 구현되었으며, 6 인년의 개발 및 검증 노력이 투입되었다.
HACL* 라이브러리는 3,300줄의 코드로 구현되었으며, 1 인년 미만의 개발 및 검증 노력이 투입되었다.
DICE* 라이브러리는 4,700줄의 코드로 구현되었다.
Signal* 라이브러리는 4,000줄의 코드로 구현되었다.
Amazon s2n 라이브러리는 860줄의 코드로 구현되었으며, 3 인년 이상의 개발 및 검증 노력이 투입되었다.
seL4 OS 커널은 100,000줄의 코드로 구현되었으며, 31.2 인년의 개발 및 검증 노력이 투입되었다.
Verve OS는 3,000줄의 코드로 구현되었으며, 0.75 인년의 개발 및 검증 노력이 투입되었다.
mCertiKOS OS는 6,000줄의 코드로 구현되었으며, 1 인년의 개발 및 검증 노력이 투입되었다.
mC2 OS는 17,000줄의 코드로 구현되었으며, 2 인년의 개발 및 검증 노력이 투입되었다.
Hyper-V 하이퍼바이저는 5,000줄의 코드로 구현되었으며, 1.5 인년의 개발 및 검증 노력이 투입되었다.
SHOLIS 항공 시스템은 3,070줄의 코드로 구현되었으며, 19 인년의 개발 및 검증 노력이 투입되었다.
NATS iFACTS 항공 시스템은 300줄의 코드로 구현되었으며, 50 인년 이상의 개발 및 검증 노력이 투입되었다.
Roissy Shuttle 시스템은 1,160줄의 코드로 구현되었다.
Dutch Tunnel CS 시스템은 150줄의 코드로 구현되었으며, 8 인년의 개발 및 검증 노력이 투입되었다.
Sizewell B 원전 시스템은 150,000줄의 코드로 구현되었으며, 250 인년의 개발 및 검증 노력이 투입되었다.
Ironclad Apps는 500줄의 코드로 구현되었으며, 3 인년의 개발 및 검증 노력이 투입되었다.
Quark 시스템은 200줄의 코드로 구현되었으며, 0.83 인년의 개발 및 검증 노력이 투입되었다.
CoCon 시스템은 670줄의 코드로 구현되었으며, 0.25 인년의 개발 및 검증 노력이 투입되었다.
CoSMed 시스템은 1,000줄의 커널 코드와 330줄의 애플리케이션 코드로 구현되었으며, 0.33 인년의 개발 및 검증 노력이 투입되었다.
Ynot 시스템은 3,030줄의 코드로 구현되었으며, 8 인년의 개발 및 검증 노력이 투입되었다.
Flover 검증 도구는 10,000줄의 코드로 구현되었으며, 2 인년의 개발 및 검증 노력이 투입되었다.
اقتباسات
"형식 검증 기술이 눈부신 발전을 이루었지만, 실제 소프트웨어 개발에 얼마나 도움이 되는가에 대해서는 여전히 상당한 이견이 있다."
"형식 검증이 단지 몇몇 비용이 많이 드는 생명 관련 프로젝트에만 국한된 것인지, 아니면 소프트웨어 산업의 광범위한 부문에 적용될 수 있는 아이디어인지에 대한 의문이 제기되고 있다."
"이 조사는 실제로 배포된 형식 검증 시스템들을 검토함으로써 이 문제에 대한 객관적인 근거를 제공한다."