1996년 4월 ESA(European Space Agency)는 프랑스 Kourou에서 아리안 5호기를 발사했다. 아리안 5호기는 이륙한지 40여초 만에 자폭 기전이 발동하여 공중에서 폭발하고 말았다. 이 사고의 원인은 아리안 4호기에 사용된 일부 소프트웨어를 그대로 사용하면서 발생하였다. 아리안 5호기는 4호기의 디자인을 변경하여 센서로부터 유동소수점(floating-point)으로 값을 받아들였고, ADA 프로그래머는 이 값이 정수(integer)로 데이터 전환이 이루어지는 경우에 대해서 무시했다. 그 결과 예외 처리(exception handling)를 프로그램에 추가하지 않았고, 아리안 5호기는 하늘의 별똥별이 되어 사라졌다.

소프트웨어로 인한 사고는 로켓이나 미사일 같은 시스템에서도 발생하고, 현대인이 한시라도 손에서 놓지 않는 휴대폰에서도 발생한다. 전자의 경우 많은 경제적 손실과 인명 피해가 발생하여 사회적 이슈로 등장하고 후자의 경우는 한번 짜증을 낼 뿐이지만, 그 경제적·사회적 떠나서 사고는 지속적으로 발생하고 있다. 특히 개발 환경이 임베디드(embedded) 시스템(일반적으로 특정 시스템에 포함되어 특수 목적을 수행하는 시스템을 의미하나, 컴퓨터의 경우 특정 역할을 수행하는 응용소프트웨어가 탑재된 컴퓨터 시스템을 의미한다. PDA·PDP·생활가전·자동차 등과 같이 광범위한 분야에 사용되고 있다)으로 접어들면서 그 피해는 더욱 가속화되고 있다.
이러한 크고 작은 피해를 미연에 방지하는 정확한 소프트웨어를 만들기 위한 노력은 계속되고 있다. 특히 우주항공·자동차·원자력과 같이 사고가 발생했을 때 경제적 손실과 인명 피해를 발생시키는 분야에서는 고 안전성(safety-critical) 시스템을 개발하기 위해 V-개발 모델을 중심으로 소프트웨어를 개발하고 있다. 지금부터 V-개발 모델(또는 Multiple V-개발 모델)과 V-개발 모델에서 주요한 위치를 차지하는 정형 기법(formal methods)에 대해서 알아보자.

V-개발 모델은 기본적으로 소프트웨어 개발 모델 가운데 하나인 폭포수(waterfall) 개발 모델을 기반으로 하여 각 단계에 적절한 검증과 테스트 작업을 일대일로 연관시킨다. 그 결과 폭포수 개발 모델이 V-개발 모델의 왼쪽 날개를 담당하고, 그에 대응되는 검증 및 테스트작업이 V-개발 모델의 오른쪽 날개를 담당하게 구성함으로써 검증을 통해 발생한 오류가 요구명세·분석·디자인·구현의 어떤 단계에서 발생했는지 추적할 수 있는 장점을 가진다. 즉 V-개발 모델은 각 단계의 작업 결과의 검증에 초점을 두고 있다. <그림 1>의 오른쪽 그림은 V 모델의 일반적인 모습으로 시스템에 따라 적용되는 테스팅 기법이 달라지기도 하고, 코드 자동 생성을 통해 ‘유닛(unit) 테스트’ 과정이 생략되어 Y-모델로 변형되기도 한다.

V-모델에 적용되는 기초적·핵심적인 개념은 위에서 언급했지만 검증과 확인 절차이고, 이를 V&V(verification and validation)라고 부른다. 이 두 개념은 유사하여 혼돈하기 쉽지만 명확한 차이를 가지고 있다. IEEE/ANSI에서 내린 검증과 확인의 정의는 다음과 같다.
“검증(verification)은 개발 단계의 산출물이 그 단계의 초기에 설정된 조건을 만족하는지 여부를 결정하기 위해 구성요소나 시스템을 평가하는 프로세스이다.”
“확인(validation)은 명시된 요구사항들을 만족하는지 확인하기 위해 개발단계의 끝이나 중간에 구성요소나 시스템을 평가하는 프로세스이다.”

‘확인’(또는 타당성 검증)은 항상 요구사항과 관계가 있다. 사용자의 요구사항이 만들려고 하는 소프트웨어를 제대로 설명한 것인지 여부를 확인하는 것이다. 다시 말하면 사용자의 요구사항을 가지고 정확한 모델을 만들 수 있는가를 확인하는 작업이다. 반면에 ‘검증’(또는 오류 검증)은 요구사항으로부터 만들어진 모델이 의도한대로 정확하게 동작하는지 여부를 확인하고, 모델에 존재하는 논리적 오류나 데이터 오류를 찾는 과정을 의미한다. 검증 활동(verification activities)에는 모델에 대한 시뮬레이션·테스팅·정형검증 등이 모두 포함된다.

V&V를 효율적으로 실행하기 위한 방법으로 정형기법(formal methods)이 있다. 정형기법은 하드웨어 논리회로 검사를 위해서 개발되었지만, 현재는 소프트웨어 개발에서도 중요한 위치를 차지하고 있다. 정형기법은 정형명세(formal specification)와 정형검증(formal verification) 과정으로 크게 나눌 수 있다.
정형 명세(formal specification)는 개발하려는 하드웨어 또는 소프트웨어의 요구사항을 수학적이거나 논리(logic)을 이용해 기술하는 것을 말한다. 시스템 개발과정 초기에 요구사항은 일반적으로 자연어로 기술된다. 자연어로 기술한 경우 시스템의 전반적인 사항을 손쉽게 기술할 수 있지만, 읽는 사람에 따라 요구사항의 뜻을 잘못 해석할 수도 있다. 우리나라 속담에 “아 다르고 어 다르다”라는 말이 있듯이 모호한 요구사항이 처음부터 잘못 해석되면 전체적으로 잘못된 시스템이 개발된다. 이러한 문제점을 제거하기 위해서 수학적이거나 논리적 의미론을 가지는 정형명세를 사용하는 것이다. 예를 들어 ‘x = x + 1’이라는 방정식을 보고 다르게 해석하는 사람은 없을 것이기 때문이다.

현재는 상태 머신(state machine) 기반의 정형명세 방식과 방정식이나 논리회로를 표현하는 방식의 정형명세가 많이 사용되고 있다. 전자의 경우 <그림 2>의 D.Harell이 개발한 Statechart를 많이 사용하고 있으며, 후자의 경우 Mathlab이나 SCADE등이 있다. 이 외에도 Promela, Esterel, Z(Zed), 그리고 Process Algebra와 같은 많은 명세 언어들이 사용되고 있다. 이러한 정형명세 언어들은 대부분 사용자 편의를 위해 소프트웨어 개발도구에 포함되어 있으며 I-Logix에서 개발한 STATEMATE는 GM에서 자동차 바디 ECU(Electronic Control Unit) 요구사항을 명세하고 개발하는데 사용하고 있다.

다음으로 정형검증에 대해서 알아보자. 정형검증(formal verification)은 수학적·논리적 증명방법 및 상태 탐색을 통해서 정형명세로 명세된 모델이 요구사항을 올바르게 만족하는지 증명하는 것을 말한다. 앞에서 언급했지만 검증에는 다양한 방법과 기술들이 존재한다. 시뮬레이션 방법도 있고 요구사항이 정확히 반영되었는지 테스트케이스(test-case)를 이용한 적용범위 테스트(coverage test)도 있다. 하지만 단순히 시뮬레이션이나 테스트로는 시스템이 할 수 있는 행위를 100% 확인해볼 수 없기 때문에 정형검증이 필요하다. 정형검증을 이용하면 시스템 모델이 가질 수 있는 모든 상태를 탐색할 수 있기 때문이다. 하지만 정형검증에도 문제가 있다. 모든 요구사항에 대해서 정형검증을 사용하면 가장 정확한 시스템이 나오겠지만, 모든 상태를 확인하기 위해서는 속도가 빠른 컴퓨터를 사용해도 시간이 오래 걸리고, 검증 모델 자체가 큰 경우에는 상태 폭발(state explosion ; 모델 체킹 기술에서 고려해야 할 소프트웨어 상태의 개수가 지수적으로 증가하여, 특정 순간부터 상태의 개수가 기하급수적으로 증가하는 현상. 상태 증가는 결과적으로 메모리의 사용을 의미하기 때문에 메모리 사용률의 증가와 컴퓨터 성능저하를 유발한다) 문제가 발생한다. 그래서 요구사항의 안전속성(safety property)을 검증하는 부분에 많이 사용된다.

비행기 착륙바퀴 제어 소프트웨어를 만들 때 요구사항에 다음과 같은 안전 속성이 포함되어 있다면 정형검증의 대표적인 기술인 모델 체킹(model-checking)을 이용하여 어떤 방식으로 정형검증이 이루어지는지 간단하게 알아보자.
“이 제어기에서 할 수 있는 모든 행위들은 비행기가 착륙해 있거나, 착륙 상태에 있을 경우, 절대로 바퀴를 접으라는 명령을 보내서는 안 된다”
먼저 이렇게 자연어로 기술되어 있는 안전속성을 <그림 3>과 같은 일반적인 논리회로나 시제논리로 변경해야 한다. 그리고 정형명세된 안전속성을 제어기에 연결하여 제어기에서 발생하는 모든 상태에서 안전속성을 위배하지 않는지 검증한다. 아래의 그림은 에어프랑스 항공기 제어 소프트웨어 개발에 사용한 SCADE Suite의 정형검증 환경이다.

정형기법은 사고가 발생했을 경우 인명피해와 재산피해가 발생하는 소프트웨어를 보다 안전하게 개발하기 위한 방법이다. 올바르고 정확한 소프트웨어를 만드는 왕도는 없다. 정형기법 역시 정확한 소프트웨어를 만들기 위해 적용해야 하는 하나의 과정이자 방법이며, 다른 방법들과 조화를 이루어야 더욱 좋은 효과를 발생시킬 수 있다. 하지만 임베디드 환경이 점점 가속화 되어가고 있는 소프트웨어 개발환경에서의 필수적인 선택이라고 할 수 있다.