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

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한 시스템은 디지털과 아날로그 부품으로 구성 되어있다. 이러한 하이브리드 시스템은 이산수학과 연속수학 양쪽의 추론을 요구한다. 시스템 개발자는 설계한 시스템이 현장에서 어떻게 동작할 것인가를 예측하여야 하며, 그때 정확성보다는 성능에 더 관심을 갖는다. 이때 성능 모델링은 확률과 통계, 대기행렬 이론(Queueing theory)을 이용하여 수행한다. 마지막으로 대규모 검색 공간과 시스템을 취급하기 위해서 부울함수를 표현하기 위한 간결한 데이터 구조와 알고리즘이 필요하다.

3.2 기법과 툴

 모든 목적에 사용할 수 있는 기법이나 툴은 존재하지 않지만 지금까지의 경험으로부터 실제 사용자에게 어떤 부류의 형식기법이 영향력을 미치는가를 알고 있다. 따라서 개발하는 기법과 툴이 사용자에게 더욱 관심을 끌기 위해 그것들이 만족해야하는 기준이 있지만 본 논문에서는 생략하기로 한다. 다만 단일 툴을 구축하는 것보다는 Steffen, Cleaveland Gordon과 Kindred 이 제안한 특별한 문제에 맞춘 툴을 스스로 생성하거나  형식기호 또는 논리를 생성하는 메타툴(Meta-Tool)을 구축하는 것이 더 바람직하다. 컴파일러 생성기와 같은 이러한 메타툴은 특수한 모델검사기 또는 증명검사기를 자동으로 구축한다. 마지막으로 새로운 기법과 툴에 대해서 개발자는 그것의 장점, 제한 요소, 모델링 가정, 다른 기법과 툴 사이의 통합의 용이함, 비용 등에 대한 분명한 언급이 있어야한다. 이러한 분명한 기준들은 사용자가 문제 해결을 위해서 가장 알맞은 기법과 툴을 결정하는데 도움이 된다.

3.3 기법의 통합

 복잡한 시스템의 모든 특성을 표현하고 분석할 수 있는 하나의 형식기법은 존재하지 않기 때문에 서로 다른 기법을 조합하여 사용하는 것이 실질적인 방법이다. 서로 다른 기법들을 조합할 때 함께 통합하는 서로 다른 기법의 알맞은 표현법과 의미를 찾는 것은 중요하다. 알맞은 표현법을 찾는데 실패하는 것은 조합하는 방법들의 진정한 장점을 놓치는 것이다. 예를 들면 'Z 언어'는 충분한 자연어로 접근 가능한 형태에서 명세서의 표현의 중요성을 강조한다. 이러한 이유로 Z 언어의 사용이 확대되어가고 있으며, 임의의 조합에서 이러한 표현법은 유지되어야 한다.
 또한 조합의 이론적 기초에 주의하는 것을 실패하면 형식화(Formality)의 진정한  장점을 놓치게 된다. 그것이 의미하는 것은 화학에서 혼합(단지 재료를 섞는 의미)과  합성(재료를 섞어 화학적으로 하나가 됨)이라는 용어의 구별과 같은 결과를 낳게된다. 만약 조합의 의미가 적절하게 설명되지 못하면 결과는 분리된 하나의 툴 보다 결합기술로부터 추론할 수 있는 것은 아무 것도 없는 단지 혼합의 의미일 뿐이다. 서로 다른 두 가지 견해에서 시스템 명세서와, 추론, 서로의 견해에서의 결과를 이해하는 것이 가능하다면 훨씬 강력한 기법이나 툴이 될 것이다. 형식 기법의 통합 연구는 Kurshan과 Lamport, Rajan등이 모델 검사와 정리 증명을 이용하여  양쪽 기법의 장점만을 취한 사례가 있다.  

4. 철도에서의 형식기법 적용

 국제규격이나 철도신호업체 자체 규격 등에서 철도신호제어시스템 대부분을 안전도 등급(SIL : Safety Integrity Level) '레벨 3' 또는 '레벨 4'를 요구하고 있다. 이처럼 철도신호제어시스템 대부분을 Safety-critical한 시스템으로 분류하고 있다. 이에 따라 이에 요구되는 높은 안전성과 신뢰성의 확보를 위해 형식기법의 적용이 적극 검토되어지고 있다. 특히 유럽 철도신호규격 중 EN50128(Railway Applications : Software for Railway Control and Protection Systems)에서는 이 요구되는 SIL등급의 만족을 위해 정규기법의 적용을 'Highly Recommended'하고 있다. 하지만 아직은 권고사양에 머무르고 있다. 철도신호분야는 아니지만 영국의 국방성(U. K. Ministry of Defence)에서는 정규기법의 적용을 강제규격으로 채택하도록 하고 있다.
 현재 철도 시스템에 형식기법을 적용하는 연구는 NASA Langley FM 연구팀과 Union Switch Signal 기술자들이 1993년에 연구를 시작하여 첫 번째 연구 결과로 2 레벨로 정의한 철도 분기기 모델(Railway Switching Model)의 수학적 형식 모델을 발표하였다. 이 연구팀의 목표는 기본적인 개념 즉, 궤도회로(Track Circuit), 선로전환기(Point), 열차(Train)와 열차 위치, 열차 제어 등에 대한 매커니즘을 제공하는 상위 모델을 개발하는 것이다. 유럽의 형식기법 단체는 철도제어시스템의 부품들의 안전도 특성을 설명하고 있고, 일본의 RTRI와 영국의 AEA Technology의 경우 전자연동장치의 연동로직 중 일부분의 동작사양을 Z 언어로 개발하려하고 있지만 아직은 연구차원에 머무르고 있다. 특히 프랑스 파리지하철 14호선의 열차제어장치의 경우  형식기법의 의해 요구사항 분석단계에서부터 설계 및 검증까지 형식기법이 적용되어 1999년부터 무인운전이 가능할 정도의 높은 안전성과 신뢰성을 확보한 것으로 파악되고 있다.
 국내 현황으로는 한국철도기술연구원에서 IEC에서 표준언어로 채택된 Grafcet(GRAphe Fonctionnel de Commande Etape/Transition)을 이용한 연동로직을 표현하고 분석하려고 시도하고 있고, 일부 대학에서 철도신호시스템 분야에 적용을 위한 기초연구를 수행하고 있다. 철도 이외의 분야에서는 1998년 12월부터 Chrysalis Symbolic Design 사의 검증 툴을 대우전자에서 제품개발에 사용하는 것으로 발표되고 있다.

5. 결 론

 전기전자 기술의 발달에 힘입어 많은 분야에서 컴퓨터를 이용한 제어시스템이 보편화되어가고 있다. 하지만 이러한 컴퓨터를 기반으로 한 제어시스템은 본질적인 특성으로 인해 위험도 분석 및 예측이 거의 불가능하여 시스템에서 요구하는 안전성 및 신뢰성을 확보하기 어렵다. 특히, 철도신호제어시스템은 높은 안전성 및 신뢰성이 요구되어진다. 이러한 문제점들의 해결을 위한 방안으로 철도선진국, 특히 유럽을 중심으로 형식기법에 대한 연구가 진행 중에 있다.
 많은 연구개발들을 통해 Safety-Critical한 소프트웨어 명세화와 하드웨어 설계, 프로토콜 표준화 검증에 있어서 형식기법의 유용함은 이미 입증되었다. 가까운 장래에 전체적인 시스템 개발과정에 형식기법의 적용이 이루어 질 것으로 기대되며, 그렇게 되기 위해서 기법과 툴을 개발해야하는 연구수행자와 개발된 툴을 이용하는 사용자가 해결 해야할 문제를 설명하는 것으로 본 고를 맺고자 한다.
 먼저 형식기법에 대한 연구자는 새로운 명세 언어와 검증기술에 대한 기본 연구를 계속적으로 수행해야 할 것이다. 특히 사용자를 위해서 비전문가도 접근 가능한 툴과 기호를 고안하기 위한 꾸준한 노력이 요구된다. 개발된 툴이나 기법을 사용해야하는 시스템 개발자는 그들이 형식기법을 사용하고 있다는 생각조차 하지 않을 정도로 충분한 훈련이 요구되며, 그들의 생각을 다른 사람에게 전달하는 수단으로 형식명세 언어 기호를 사용할 줄 알아야하며, 모델 검사기와 증명 검사기 같은 툴을 고급언어의 번역기를 사용하듯이 쉽게 사용할 줄 알아야 할 것이다.

< 참고문헌 >

[1] McDermid J.A, 'Formal Methods : Use and Relevance for the Development of Safety-critical systems', pp. 96-153. oxford: Butterworth-Heinemann, 1993.
[2] Rushby J, 'Formal Methods and the Certification of Critical Systems', Technical report CSL-93-7, SRI International, Menlo Park, CA., 1993.
[3] Butler, Ricky W. and Finelli, George B. 'The Infeasibility of Quantifying the  Reliability of Life-Critical Real-Time Software', IEEE Transactions on Software Engineering, vol. 19, no. 1, Jan., pp. 3-12., 1993.
[4] Butler, Ricky W. and Finelli, George B., 'The Infeasibility of Experimental Qualification of Life-Critical Software Reliability', Proceedings of ACM SIGSOFT '91 Conference on Software for Critical Systems, New Oleans, Louisiana, Dec., pp.66-76., 1991.
[5] Holloway, C. Michael and Holloway, C. Michael, 'Why Engineers Should Consider Formal Methods', Proceedings of the 16th AIAA/IEEE Digital Avionics Systems Conference, October 26-30, Irvine CA, Volume 1, pages 1.3-16-1.3-22, 1991.
[6] M. Ingleby and I. Mitchell, 'Formal Mathematics for Signalling', Report of an IRSE Seminar, 15th April 19096.
[7] 福岡 博, 福田 光芳, 'ペトリネツトによる連動仕樣の檢　', RTRI Report Vol. 9, No. 11, pp. 19-24, 1995.