형식 검증
형식 검증(Formal verification)은 하드웨어 및 소프트웨어 시스템의 맥락에서 공식 수학 방법을 사용하여 특정 형식 사양 또는 속성과 관련하여 시스템의 정확성을 증명하거나 반증하는 행위이다.[1] 형식 검증은 시스템의 형식 사양을 위한 주요 인센티브이며 형식 방법의 핵심이다. 이는 전자 설계 자동화에서 분석 및 검증의 중요한 차원을 나타내며 소프트웨어 검증에 대한 한 가지 접근 방식이다. 공식 검증을 사용하면 컴퓨터 보안 인증에 대한 공통평가기준 프레임워크에서 가장 높은 평가 보증 수준(EAL7)이 가능하다.
공식 검증은 암호화 프로토콜, 조합 회로, 내부 메모리가 있는 디지털 회로, 프로그래밍 언어의 소스 코드로 표현된 소프트웨어와 같은 시스템의 정확성을 입증하는 데 도움이 될 수 있다. 검증된 소프트웨어 시스템의 대표적인 예로는 CompCert 검증 C 컴파일러와 seL4 높은 보증 운영 체제 커널이 있다.
이러한 시스템의 검증은 시스템의 수학적 모델에 대한 공식적인 증거가 존재하는지 확인함으로써 수행된다.[2] 시스템을 모델링하는 데 사용되는 수학적 개체의 예로는 유한 상태 기계, 레이블이 있는 전환 시스템, 혼 절, 페트리 넷, 벡터 추가 시스템, 시간 제한 오토마타, 하이브리드 오토마타, 프로세스 대수, 프로그래밍 언어의 형식 의미(예: 연산 의미론, 표시 의미론, 공리적 의미론 및 호어 논리) 등이 있다.[3]
같이 보기[편집]
각주[편집]
- ↑ Sanghavi, Alok (2010년 5월 21일). “What is formal verification?”. 《EE Times Asia》.
- ↑ Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). 〈Chapter 3: Modeling for Verification〉. Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick. 《Handbook of Model Checking》. Springer. 75–105쪽. doi:10.1007/978-3-319-10575-8. ISBN 978-3-319-10574-1.
- ↑ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013
