정형기법의 실제 적용 절차

‘정형기법’의 역사는 1970년대 영국의 Oxford 대학과 Edinburough대학의 수학명제를 자동 증명할 수 있는 증명 개발로부터 시작한다. 특히 소프트웨어 공학에서의 정형 기법(formal methods)은 소프트웨어와 하드웨어 시스템의 명세, 개발, 형식 검증을 위한 특정한 종류의 수학적 기반 기술이다. 그만큼 새로운 기법은 아니라는 뜻도 된다. 하지만 최근 들어 각종 기능안전성(Functional Safety) 관련 국제표준의 권고에 따라 정형기법을 적용해야 하는 소프트웨어가 급격히 증가함에 따라, 효과적인 적용 방법에 대한 관심이 증가되고 있는 상황이다. 그럼에도 불구하고 정형기법(정형명세+정형검증)은 안전최우선(Safety-Critical) 시스템/소프트웨어의 검증(V&V : Verification & Validation) 기법으로서, 적용 대상이 한정되고 비용이 많이 소요되는 특징으로 인해, 그 구체적인 적용 방법과 사례가 널리 알려져 있지 않다. 때문에 여러 다양한 개발 현장에서 정형기법을 실제로 적용할 때 어려운 점이 많아, 건국대학교 유준범 교수로 부터 일반적으로 널리 사용되는 정형기법의 방법/절차에 대한 조언을 구했다.

1. 정형기법의 적용범위 2. 정형기법의 이상적인 적용방법 3. 정형명세 및 정형검증 4. 실제 적용사례

캡션 추가이상적인 정형기법 적용 방법

자세히 보기 →