날으는 우돼지♡

양성현 | 광운대학교 전자공학부 부교수
황종규 | 철도신호통신연구팀 주임연구원
이종우 | 철도신호통신연구팀 책임연구원

1. 서 론

 컴퓨터 시스템은 물리적인 구성성분(하드웨어 부품/소프트웨어 모듈)에서의 결함 또는 설계 오류 등에 의한 원인으로 인해 시스템이 의도하는 임무를 수행하는 중 고장을 일으킬 수  있다. 이러한 경우 초 신뢰성과 안전성을 요구하는 응용분야에 이용되는 시스템은 최소한 위의 두 가지 원인이 시스템 고장발생의 원인이 되지 않도록 해야 한다. 물리적인 부품에서 발생 가능한 결함을 취급하는 기술로는 현재 여분(Redundancy)과 투표기(Voter)를 이용하는 기술이 대표적인 기술로 이용되고 있으며, 이러한 기술을 적용한 시스템에 대해 신뢰성 평가는 마코브 모델링 등을 일반적으로 사용하고 있다.
 설계 오류 문제는 취급하기가 더욱 복잡하며, 현재 사용하고 있는 설계오류 취급 기술에 대해 과학적으로 정당성을 확보할 수 있는 이론이 존재하지 않는다. 단지 설계오류를 취급하기 위해서 검사(Testing), 설계의 다양화(N-버전 프로그래밍, Recovery Block 등), 결함회피(Fault-Avoidance) 기법 등이 제안되고 있다.
 위의 방법들에 따른 문제점으로는 첫째 시험을 수행하는데 있어서 시험기간이 실행 불가능할 정도로 길다는 것이다. 예를 들어 1시간 동안의 시스템이 임무를 수행하는데 있어 고장확률이 10-9라는 확률을 측정하기 위해서 114,000년 이상을 시험해야 한다. 이러한 점들을  극복하기 위한 방법으로 설계의 다중화(Diversity)가 주장되고 있으며, 이 방법의 기본적인 개념은 같은 명세서(Specification)로부터 독립된 설계 및 구현팀으로 부터의 다중버전을 만들자는 것이다. 그리고 하나의 버전에서 발생하는 설계오류의 영향을 은닉(Masking)하기 위해서 임계투표기(Threshold Voter)가 이용되어지고 있다.
 이 방법은 설계상의 결함이 독립적인(Independence) 결함이라는 것이 확인될 때 가능할 것이다. 그러나 물리적 법칙에 의한 하드웨어 결함과는 달리, 소프트웨어 모듈은 주관적인  논리 의하기 때문에 각 버전의 결함이 독립적인 결함이라 확신할 수 없다. 따라서 초신뢰성을 필요로 하는 Safety-critical한 시스템을 위해서는 단지 하나의 방법을 될 수 있을 지라도 궁극적인 방법은 아니다. 따라서 유용한 시험시간 내에서 초 신뢰성을 성취할 수 있는 설계 다양화는 불가능하다. 결과적으로 설계 다양화 기법은 실제적으로 충분한 검증 없이는 초신뢰성을 만족할 수 없다.
 초신뢰성 시스템은 통상 1-10-9 신뢰도 가진 시스템을 의미하며, 이는 정량화 영역을 넘어서기 때문에, 이용 가능한 가장 엄격한 방법에 의해서 시스템을 설계하는 방법을 사용하여야 한다. 따라서 언급한 문제점으로부터 설계상의 오류 문제를 취급하기 위한 방법으로 형식기법(Formal Methods)의 사용을 들 수 있다. 형식기법은 컴퓨터 시스템의 하드웨어 또는 소프트웨어 구현에 앞서 설계하고자 하는 시스템 행위(Behavior)가 어떠한가를 계산 및 예측하는 방법을 제공하는 컴퓨터공학의 응용수학이다. 특히 시스템의 기능은 물론이고 높은 안전성 특성을 만족해야하는 Safety-critical한 시스템 설계와 구현과정에서, 형식기법을 이용하여 설계명세화(Specification), 구현모델(Implementation Model) 및 검증(Verification) 과정의 수행을 통하는 것은 높은 안전성과 신뢰성을 갖는 시스템을 설계 및 개발하는 방법이 될 것이다.
 본 고에서는 Safety-critical한 시스템 설계시 형식기법의 적용을 위한 기본지식을 설명하고자 한다. 즉, 형식기법의 개요, 형식 명세서 및 형식검증기법을 설명하고, 사용자 입장에서의 형식기법 툴의 사용시 주의점, 형식기법을 연구하는데 있어서의 문제점 등을 제시하고자 한다.

2. 형식 기법(Formal Method)

2.1. 형식기법의 개요

 일반적으로 공학분야에서는 설계에 대한 검증을 위해서 수학적인 모델과 계산에 의하고 있다. 형식기법은 컴퓨터시스템(하드웨어 및 소프트웨어) 설계에 응용 가능한 다양한 수학적 모델링 기법을 나타낸다. 즉 형식기법은 컴퓨터공학의 응용수학이며, 그것을 적절하게 컴퓨터공학에 적용할 때 컴퓨터를 기반으로 한 제어시스템 설계시 중요한 역할을 하게된다.
 형식기법은 시스템의 행위를 명세화 및 모델링하는데 사용되어진다. 또한 시스템을 설계하고 구현하는데 있어서 요구되는 시스템 기능과 안전성 특성이 만족된다는 것을 수학적으로 검증하기 위해 사용된다. 이러한 명세화, 모델링 및 검증행위는 엄격함(Rigorousness)의 등급을 갖는 다양한 기술을 이용하여 수행한다. 이러한 적용의 엄정함을 Rushby는 다음과 같이 3가지로 분류하였다. 또한 이것을 엄정함의 등급이라기 보다는 형식기법이 취해야하는 과정으로 표현하는 연구자도 있으나, 이는 모든 세 단계를 거쳐 구현된 시스템은 정확도가 그만큼 향상되기 때문에 결과적으로는 엄정함의 등급과 같은 결과로 볼 수 있다.

 ▶ Level 1 : 시스템 전체 또는 일부의 형식 명세서(Formal Specification)

 ▶ Level 2 : 구현 모델(Implementation Model) 및 검증(Verification)

 ▶ Level 3 : Mechanical Theorem Prover에 의한 형식 증명(Formal Proof) 검사

 형식기법은 일반적으로 시스템 전체에 적용하지는 않는다. 즉, 시스템의 가장 민감한 부분에 형식기법을 적용하는 것이 실제적이고 유용한 방법이다. 대규모의 복잡한 시스템에 대해서 전체적으로 형식기법의 적용은 현재로는 매우 어렵고 많은 시간을 필요로 하지만, 시스템의 핵심부에 형식기법을 이용함으로써 시스템의 신뢰성 및 안전성을 크게 향상시킬 수 있다. 형식기법의 적용과정은 먼저 설계기준을 표현하는 명세서를 작성하고, 그 다음 설계 및 제작을 위한 구현모델을 작성한다. 마지막으로 모든 경우에 대해서 구현모델이 명세서와 일치한다는 것을 형식 검증을 통해 입증해야 한다. 이러한 과정에 대한 세부적인 설명은 2-2, 2-3절에서 논한다.

2.2. 형식 명세서(Formal Specification)

 명세서는 시스템과 시스템의 정확한 특성을 나타내는 것이다. 형식명세서는 수학적으로 정의된 문법과 의미론을 갖는 언어를 사용하여 표현한다. 시스템의 특성에는 기능적 행위(Functional behavior), 타이밍 동작, 성능특성, 내부구조 등을 포함한다. 지금까지 행위적 특성에 대해서는 명세서가 가장 적절하며, 현재의 경향은 시스템의 각기 다른 형태를 취급할 수 있는 서로 다른 명세언어를 통합하는 것이다. 명세서 작성에 있어서의 또 다른 경향은 시스템의 성능, 실시간 제약조건, 보안정책, 구조적 설계와 같은 시스템의 비행위적 특성을 취급하는 것이다. 명세서 작성 과정은 시스템의 동작행위 및 특성을 엄밀하게 서술하는 과정이다. 그렇게 함으로써 시스템에 대한 충분한 이해를 하게 되고, 이로서 개발자가 발견할 수 없는 설계상의 약점, 모호성, 불완전성을 파악할 수 있게 된다. 명세서는 시스템의 최종 사용자와 설계자, 설계자와 구현자, 구현자와 평가자 사이의 유용한 전달 수단이 된다. 형식명세서는 형식논리로부터 유래한 기호를 사용하여 다음 사항을 표현한다.

 ▶시스템이 운용될 환경에 대한 가정

 ▶ 시스템이 달성해야 할 요구사항

 ▶ 요구사항에 부합하기 위한 설계

예 1 : 형식명세서

 ▶ 명세서 : 길이 N의 배열 A는 1....N으로 색인되었다.  X값을 배열에서 찾는 과정이다. 만약 원소를 찾으면 Y는 X와 등가인 배열 원소의 색인과 같은 값이다. X와 등가인 배열 요소가 없다면 Y는 0이 된다.
 
 ▶ 형식 명세서 :
   pre_condition : N>0
   post_condition : {(X=A[Y])\land(1\leq Y\leq N)}\lor{(Y=0)\land(\forall k\(1\leq k\leq N)\aupset A[k]\leq X)}  

 ▶ 구문론적 형태의 형식 명세서 :
  .pre_condition   N>0
  .post_condition IF(\forall k\(1\leq k\leq N)\supset A[k]\neq X)THEN(Y=0)ELSE X=A[Y]AND(1\leq Y\leq N)}

2.3. 형식검증(Formal Verification)

 형식검증에 대한 확립된 방법으로는 모델 검사(Model Checking)와 정리 증명(Theorem Proving)이 있다. 형식검증은 명세서 작성 다음 단계로서, 이러한 형식 기법은 시스템의 바람직한 특성을 분석하는데 이용한다.

2.3.1. 모델검사(Model Checking)

 모델 검사는 시스템의 유한모델을 구축하고, 그 모델이 바람직한 시스템 특성을 유지하는지를 검사하는 기술이다. 모델검사에서의 기술적인 어려움은 대규모 검색공간이 가능한 데이터구조와 알고리즘에 있다. 이러한 모델검사는 기본적으로 하드웨어와 프로토콜 검증에 유용하지만, 현재는 소프트웨어의 명세서 분석 및 검증에도 방법을 적용하고 있다. 현재 실질적으로 사용되고 있는 모델검사에 대한 일반적인 방법으로는 명세서를 시간논리(Temporal Logic)로 표현하고 시스템을 유한상태천이(Finite State Transition) 시스템으로 모델링하는 시간모델 검사(Temporal Model Checking)와 명세서와 시스템 모델이 자동으로  만들어지고 모델된 시스템의 행위가 명세서의 행위와 일치하는지 결정하기 위해서 서로 비교하는 방법이 있다. 모델검사는 부분적인 명세서를 검사하는데 이용될 수 있기 때문에, 시스템이 완전하게 명세화되지 않은 경우에도 일부분에 대한 모델검사를 통해 시스템의 정확도에 관한 유용한 정보를 얻을 수 있다. 특히 모델검사 기술은 설계시 미묘한 오류를 나타내는 논리나 규칙에 대한 검사가 가능하므로 명세서의 오류를 수정하는데 유용하게 이용되어질 수 있다.

2.3.2. 정리증명(Theorem Proving)

 정리증명은 시스템과 시스템의 정확한 특성을 수학적 논리(Mathematical Logic) 내에서 공식으로 표현하고 증명하는 것이다. 수학적 논리는 공리(Axiom)와 추론규칙(Inference Rule)의 집합을 정의하는 형식시스템(Formal System)에 의해서 주어진다. 정리증명은 시스템의 특성을 공리와 규칙, 유도된 정의, 중간 이론 등을 이용하여 증명한다. 증명은 수작업에 의해서도 수행할 수 있지만, 현재 기계의 도움에 의한 정리증명에 연구의 초점이 맞추어 지고 있다. 오늘날 정리증명기(Theorem Prover)는 하드웨어와 소프트웨어 설계에 있어서의  Safety-Critical한 특성의 검증에 점차적으로 이용되고 있다. 정리증명기는 자동화한 범용 프로그램으로부터 특별한 목적을 갖는 대화형 시스템까지 광범위하게 분류될 수 있다. 자동화한 시스템은 일반적인 검색절차로서 이용가능하고 여러 가지 조합적인 문제를 해결하는데 있어 주목할만한 성과를 이루고 있다. 대화형 시스템은 체계적인 수학적 형식개발과 기계적 형식기법에 보다 알맞은 시스템이다.
 모델 검사와 대조적으로 정리 증명은 유한상태공간을 직접적으로 취급할 수 있으며, 이를 위해 유한 영역 상에서 증명하기 위해 구조적 귀납법(Structural Induction)을 사용한다. 대화형 정리 증명기라는 정의에서 알 수 있듯이 이 시스템은 인간과의 대화를 요구하며, 정리 증명 과정이 늦고, 오류를 범하기 쉽다. 대신 증명과정에서 사용자는 시스템  또는 증명된 특성을 간파할 수 있는 장점이 있다.

2.3.3  등가성 검사(Equivalence Checking)

 등가성 검사의 목적은 하드웨어 특히, 반도체 설계분야에서 게이트나 스위치 레벨 시뮬레이션을 줄이거나 제거하는데 있다. 따라서 게이트나 스위치 기능 검사가 필요로 하는 어디에서나 적용되어질 수 있다. 등가성 검사에는 조합 등가성 검사, 순서 등가성 검사, 상태 등가성 검사와 같은 3가지의 서로 다른 레벨의 기술이 있다.

3. 형식기법의 연구 및 사용

 형식기법의 사용 목적은 높은 안전성과 신뢰성이 확보되는 시스템을 설계하자는 데 있다.  형식기법의 기초는 수학을 근거로 하며, 시스템의 하드웨어 및 소프트웨어 설계시 적용되어질 수 있다. 또한 형식기법의 잠재적 사용자는 시스템공학 과정에 포함된 모든 개발자가 될 것이다. 과거 10여년 동안에 형식기법 분야에 대한 많은 연구가 있어왔다. 그 결과 보다 다루기 어렵고 규모가 큰 문제점들에 대해서도 형식기법을 적용할 수 있게 되었다. 형식기법에서의 더 많은 진전이 있기 위해서는 기초연구, 새로운 기법의 고안, 새로운 툴의 구축, 서로 다른 기법의 통합, 실제 사용자를 위한 효과적인 기술이전에 대한 연구자의 노력 등이 요구된다. 이러한 노력들을 바탕으로 형식기법의 적용에 대한 연구자와 산업계 사이의 인식차이 등이 줄여질 때 그리고 산업계에서 형식기법의 필요성을 느낄 때 이 방법이 Safety-critical한 시스템의 설계 및 개발에 있어서의 대안이 될 것이다. 본 장에서는 형식 기법을 연구하는데 필요한 언급된 사항에 대해서 논한다.

3.1 기본 개념

 형식 기법의 연구는 일반적인 컴퓨터 분야의 기본적인 개념을 근거로 한다. 기법, 명세서, 모델, 정리증명 등을 어떻게 구성할 것인가로 부터 계산적으로 요구하는 포괄적 특성을 검증이 간단한 한정된 특성으로 분할하기 위한 효과적인 방법을 개발할 필요가 있다. 또한 추상화 없이 실제 시스템을 명세화하고 검증하는 것은 어렵기 때문에 일정한 시스템이나 문제에 맞춘 모델링이 필요하고, 형식적으로(Formal) 그들을 정당화하고 검증하기 위한 방법의  개발이 필요하다.
 시스템의 설계 및 개발에 있어서는 일시적으로 사용되는 모델링이나 규칙보다는 재사용가능하고 매개변수화하는 모델과 규칙을 확보하는 것이 바람직하다. 대부분의 Safety-critical한 시스템은 디지털과 아날로그 부품으로 구성 되어있다. 이러한 하이브리드 시스템은 이산수학과 연속수학 양쪽의 추론을 요구한다. 시스템 개발자는 설계한 시스템이 현장에서 어떻게 동작할 것인가를 예측하여야 하며, 그때 정확성보다는 성능에 더 관심�