정형 기법

3. 분류

정형 기법은 개발 프로세스의 여러 지점에서 적용될 수 있다.

정형 기법은 다양한 기법을 포함한다.

; 적용 수준에 따른 분류

형식 기법은 몇 가지 수준으로 사용할 수 있다.

• 수준 0: 형식 명세 기술을 수행하고 프로그램 자체를 비형식적으로 수행한다. "가벼운 형식 기법"이라고 부른다. 비용 효과를 빠르게 얻을 수 있는 선택이다.
• 수준 1: 형식 기법을 사용하여 소프트웨어 개발과 형식적 검증을 수행하고, 보다 형식적으로 프로그램을 생성한다. 예를 들어, 명세 기술로부터의 프로그램 작성에서 상세화와 속성의 증명을 수행한다. 고신뢰 시스템에 적합한 선택이다.
• 수준 2: 자동 정리 증명에 의해 완전히 기계적인 증명을 수행한다. 도구를 정비하는 데 비용이 들거나, 엄격할 필요가 있으며 시스템을 기술하는 데 품이 많이 든다. 오류가 혼입됨으로써 생기는 손실에 상응하지 않으면 실시하지 않는다 (예를 들어, 마이크로프로세서 설계의 중요한 부분 등).

• 지시적 의미론: 시스템의 의미를 영역 이론으로 표현한다. 이 경우, 영역 이론의 성질에 의해 시스템의 의미를 부여한다. 그러나 모든 시스템이 함수로 직관적으로 표현될 수 있는 것은 아니다.
• 조작적 의미론: 보다 단순한 계산 모델의 일련의 동작에 의해 시스템의 의미를 표현한다. 이 경우, 모델의 단순성이 표현을 명확하게 한다. 그러나, 이것은 의미론적인 판단의 연기라고도 할 수 있다.
• 공리적 의미론: 시스템이 어떤 처리를 수행하기 전과 후의 (참된) 상태에 의해 시스템의 의미를 표현한다. 이 경우, 고전적 논리학과 관계가 깊다. 그러나 단순히 실행 전과 실행 후의 상태를 나타낸 것만으로 실제로 시스템이 무엇을 하는지를 표현한 것이 되는가 하는 의문도 제기된다.

3. 1. 적용 수준에 따른 분류

• 수준 0: 형식 명세 기술을 수행하고 프로그램 자체를 비형식적으로 수행한다. "가벼운 형식 기법"이라고 부른다. 비용 효과를 빠르게 얻을 수 있는 선택이다.
• 수준 1: 형식 기법을 사용하여 소프트웨어 개발과 형식적 검증을 수행하고, 보다 형식적으로 프로그램을 생성한다. 예를 들어, 명세 기술로부터의 프로그램 작성에서 상세화와 속성의 증명을 수행한다. 고신뢰 시스템에 적합한 선택이다.
• 수준 2: 자동 정리 증명에 의해 완전히 기계적인 증명을 수행한다. 도구를 정비하는 데 비용이 들거나, 엄격할 필요가 있으며 시스템을 기술하는 데 품이 많이 든다. 오류가 혼입됨으로써 생기는 손실에 상응하지 않으면 실시하지 않는다 (예를 들어, 마이크로프로세서 설계의 중요한 부분 등).

3. 2. 의미론에 따른 분류

• 지시적 의미론: 시스템의 의미를 영역 이론으로 표현한다. 이 경우, 영역 이론의 성질에 의해 시스템의 의미를 부여한다. 그러나 모든 시스템이 함수로 직관적으로 표현될 수 있는 것은 아니다.
• 조작적 의미론: 보다 단순한 계산 모델의 일련의 동작에 의해 시스템의 의미를 표현한다. 이 경우, 모델의 단순성이 표현을 명확하게 한다. 그러나, 이것은 의미론적인 판단의 연기라고도 할 수 있다.
• 공리적 의미론: 시스템이 어떤 처리를 수행하기 전과 후의 (참된) 상태에 의해 시스템의 의미를 표현한다. 이 경우, 고전적 논리학과 관계가 깊다. 그러나 단순히 실행 전과 실행 후의 상태를 나타낸 것만으로 실제로 시스템이 무엇을 하는지를 표현한 것이 되는가 하는 의문도 제기된다.

3. 3. 경량 정형 기법

4. 활용

형식 기법은 개발 공정의 다양한 부분에 적용 가능하다.

; 명세 (Specification)

정형 기법은 개발할 시스템에 대한 형식적 설명을 제공하며, 비형식적 요구 사항의 모호성을 발견하고 해결하는 데 사용될 수 있다.^[4] 또한 엔지니어는 개발 프로세스를 안내하기 위해 정형 명세를 참조 자료로 사용할 수 있다.^[4]

형식 명세 시스템의 필요성은 수년 동안 언급되어 왔다. ALGOL 58 보고서에서,^[5][50] 존 바커스는 프로그래밍 언어 구문을 설명하기 위한 형식적 표기법을 제시했으며, 이는 나중에 바커스-나우르 표기법(BNF)으로 명명되었다.^[6][51] 바커스는 또한 구문적으로 유효한 ALGOL 프로그램의 의미에 대한 형식적 설명이 보고서에 포함될 만큼 충분히 빨리 완성되지 않아 "후속 논문에 포함될 것"이라고 밝혔지만, 형식적 의미론을 설명하는 논문은 발표되지 않았다.^[7]

; 설계 (Design)

형식 명세 기술이 가능하면, 이에 따라 설계를 수행하고 실제 개발을 진행한다.^[8] 예를 들어, 조작적 의미론에 기초한 형식 명세 기술의 경우, 실제 시스템의 동작과 사양상의 동작을 비교하며, 도구에 따라서는 그러한 사양 기술로부터 자동으로 코드를 생성하는 것도 있다.^[8] 공리적 의미론에 기초한 형식 명세 기술의 경우, 사양에 기재된 사전 상태와 사후 상태가 실행 코드 내에 어설션으로 포함된다.^[8]

; 검증 (Verification)

정형 검증은 소프트웨어 도구를 사용하여 정형 명세의 속성을 증명하거나, 시스템 구현의 정형 모델이 해당 명세를 만족하는지 증명하는 데 사용된다. 정형 명세가 개발되면 해당 명세를 기반으로 명세의 속성을 증명하고, 추론을 통해 시스템 구현의 속성을 증명할 수 있다. Sign-off 검증은 신뢰도가 높은 정형 검증 도구를 사용하는 것이다. 이러한 도구는 기존의 검증 방식을 대체할 수 있다(해당 도구는 인증을 받을 수도 있다).

때때로 시스템의 정확성을 증명하려는 동기는 시스템의 정확성에 대한 확신보다는 시스템을 더 잘 이해하려는 욕구에서 비롯된다. 결과적으로, 몇몇 정확성 증명은 수학적 증명의 스타일로 제작된다. 즉, 자연어를 사용하여 손으로 쓰거나 (또는 활자화) 하며, 이러한 증명에 일반적으로 사용되는 비공식적인 수준을 사용한다. "좋은" 증명은 다른 사람도 읽고 이해할 수 있는 증명이다.

이러한 접근 방식에 대한 비판론자들은 자연어에 내재된 모호성 때문에 이러한 증명에서 오류가 감지되지 않을 수 있다고 지적한다. 종종, 미묘한 오류는 이러한 증명에서 일반적으로 간과되는 하위 수준의 세부 사항에 존재할 수 있다. 또한, 이러한 좋은 증명을 만드는 데 필요한 작업은 높은 수준의 수학적 정교함과 전문 지식을 요구한다.

자동화된 수단으로 이러한 시스템의 정확성에 대한 증명을 생성하는 데 관심이 높아지고 있다. 자동화된 기법은 자동 정리 증명, 모델 검사, 추상 해석의 세 가지 일반적인 범주로 나뉜다.

일부 자동 정리 증명은 어떤 속성이 추구할 만큼 "흥미로운지"에 대한 지침이 필요하지만, 다른 것은 사람의 개입 없이 작동한다. 모델 검사기는 충분히 추상적인 모델이 주어지지 않으면 수백만 개의 흥미롭지 않은 상태를 확인하는 데 빠르게 얽힐 수 있다.

이러한 시스템의 지지자들은 알고리즘적으로 모든 지루한 세부 사항이 검증되었으므로 결과가 사람이 생성한 증명보다 더 큰 수학적 확실성을 갖는다고 주장한다. 또한 이러한 시스템을 사용하는 데 필요한 교육은 손으로 훌륭한 수학적 증명을 생성하는 데 필요한 교육보다 적기 때문에 더 광범위한 실무자가 기술을 사용할 수 있게 된다.

비평가들은 이러한 시스템 중 일부가 마치 오라클 머신과 같다고 지적한다. 즉, 진실을 선언하지만 그 진실에 대한 설명을 제공하지 않는다. 또한 "감시자를 누가 감시하는가?"의 문제가 있다. 즉, 검증을 돕는 프로그램 자체가 증명되지 않은 경우 생성된 결과의 건전성에 의문을 제기할 이유가 있을 수 있다. 일부 최신 모델 검사 도구는 증명의 각 단계를 자세히 설명하는 "증명 로그"를 생성하여 적절한 도구가 주어지면 독립적인 검증을 수행할 수 있게 한다.

추상 해석 접근 방식의 주요 특징은 건전한 분석, 즉 거짓 음성이 반환되지 않는다는 것이다.^[9] 또한 분석할 속성을 나타내는 추상 도메인을 조정하고, 빠른 수렴을 얻기 위해 와이드닝 연산자를 적용하여 효율적으로 확장 가능하다.^[9]

; 정형 기법의 적용 분야

정형 기법은 라우터, 이더넷 스위치, 라우팅 프로토콜, 보안 응용 프로그램, 운영 체제 마이크로커널(seL4) 등 다양한 하드웨어 및 소프트웨어 분야에 적용된다.^[14][15] 데이터 센터에 사용되는 하드웨어 및 소프트웨어의 기능을 검증하는 데에도 활용된다.

IBM은 AMD x86 프로세서 개발 과정에서 정리 증명기인 ACL2를 사용했고, 인텔은 하드웨어 및 펌웨어(ROM) 검증에 정형 기법을 활용한다. 인텔은 캐시 일관성 프로토콜의 매개변수화된 검증,^[19] 인텔 코어 i7 프로세서 실행 엔진 검증,^[20] HOL light 정리 증명기를 사용한 인텔 IA-64 아키텍처 최적화,^[21] PCI Express 프로토콜 및 인텔 고급 관리 기술을 지원하는 고성능 듀얼 포트 기가비트 이더넷 네트워크 인터페이스 컨트롤러 검증 등에 정형 기법을 사용했다.^[22] IBM은 파워 게이트 검증,^[23] 레지스터 검증,^[24] IBM Power7 마이크로프로세서의 기능 검증에 정형 기법을 사용했다.^[25]

NASA의 차세대 항공 운송 시스템, 국가 항공우주 시스템의 무인 항공기 시스템 통합,^[16] 항공 조정 충돌 해결 및 감지(ACCoRD)^[17] 등에도 정형 기법이 적용된다.

알스톰과 지멘스는 B-Method를^[18] 사용하여 전 세계 지하철의 안전 자동화 장치를 개발했다. B-Method는 이 외에도 Common Criteria 인증, ATMEL 및 STMicroelectronics의 시스템 모델 개발에도 사용된다.

덴마크 데이터매틱 센터는 1980년대에 Ada 프로그래밍 언어용 컴파일러 시스템을 개발하기 위해 정형 기법을 사용했으며, 이 시스템은 장기간 사용된 상용 제품이 되었다.^[14][15]

정형 기법은 항공 전자 소프트웨어와 같이 안전 필수 또는 보안 필수 소프트웨어 및 시스템에 적용될 가능성이 높다. DO-178C와 같은 소프트웨어 안전 보증 표준은 보충을 통해 정형 기법의 사용을 허용하며, 공통 평가 기준은 가장 높은 수준의 범주에서 정형 기법을 의무화한다.

순차적 소프트웨어의 경우, 정형 기법의 예로는 B-Method, 자동 정리 증명에 사용되는 명세 언어, RAISE, Z 표기법 등이 있다. 함수형 프로그래밍에서 속성 기반 테스트는 개별 함수의 예상 동작에 대한 수학적 명세 및 테스트를 가능하게 한다.

객체 제약 언어(자바 모델링 언어)를 통해 객체 지향 시스템을 공식적으로 명세할 수 있지만, 반드시 공식적으로 검증할 필요는 없다. 동시 소프트웨어 및 시스템의 경우, 페트리넷, 프로세스 대수, 유한 상태 기계(자동 이론)는 실행 가능한 소프트웨어 명세를 허용하며, 응용 프로그램 동작을 구축하고 검증하는 데 사용될 수 있다.

설명 논리를 기반으로 하는 OWL 언어와 같이, 일계 논리의 변형으로 명세를 작성한 다음, 마치 프로그램인 것처럼 논리를 직접 실행하는 접근 방식도 있다. Attempto 제어 영어와 인터넷 비즈니스 로직은 영어(또는 다른 자연어)의 일부 버전을 자동으로 논리로 매핑하고, 논리에서 다시 영어로 매핑하는 작업, 그리고 논리를 직접 실행하는 작업을 수행한다. 이러한 시스템은 비즈니스 또는 과학 수준에서 영어로 결과에 대해 설명할 수 있다는 특징이 있다.

4. 1. 명세 (Specification)

4. 2. 설계 (Design)

4. 3. 검증 (Verification)

4. 4. 정형 기법의 적용 분야

5. 기술 및 도구

정형 기법은 다양한 기법을 포함한다.

다양한 형식 기법과 표기법이 존재한다.

명세 기술 언어

• 액터 모델
• 프로세스 대수
• * CSP
• * LOTOS/Language Of Temporal Ordering Specification^영어
• * π 계산/Pi-calculus^영어
• 페트리넷
• 추상 상태 기계/Abstract State Machines^영어 (ASM)
• Alloy
• ANSI/ISO C 명세 언어/ANSI/ISO C Specification Language^영어 (ACSL)
• B-Method
• CADP
• Common Algebraic Specification Language (CASL)
• Esterel
• Lustre
• mCRL2
• Perfect Developer
• RAISE
• Rebeca Modeling Language/Rebeca Modeling Language^영어
• SPARK Ada/SPARK (programming language)^영어
• Specification and Description Language (SDL)
• Temporal logic of actions (TLA)
• uppaal
• USL
• VDM
• * VDM-SL
• * VDM++
• Z 언어

• SPIN
• PAT
• MALPAS Software Static Analysis Toolset

5. 1. 명세 언어

• 추상 상태 기계 (ASMs)
• 응용 공통 리스프를 위한 계산 논리 (ACL2)
• 액터 모델
• Alloy
• ANSI/ISO C 명세 언어 (ACSL)
• 자율 시스템 명세 언어 (ASSL)
• B-Method
• CADP
• 공통 대수 명세 언어 (CASL)
• Esterel
• 자바 모델링 언어 (JML)
• 지식 기반 소프트웨어 어시스턴트 (KBSA)
• Lustre
• mCRL2
• Perfect Developer
• 페트리 망
• 예측 프로그래밍
• 프로세스 계산
• CSP
• LOTOS
• π-calculus
• RAISE
• Rebeca 모델링 언어
• SPARK Ada
• 명세 및 설명 언어
• TLA+
• USL
• VDM
• VDM-SL
• VDM++
• Z 표기법

5. 2. 모델 검사기

• ESBMC
• MALPAS Software 정적 분석 도구 세트 – 안전이 중요한 시스템의 형식적 증명에 사용되는 산업용 모델 검사기이다.
• PAT – 동시 시스템 및 CSP 확장(예: 공유 변수, 배열, 공정성)을 위한 무료 모델 검사기, 시뮬레이터 및 개선 검사기이다.
• SPIN
• UPPAAL

5. 3. 정형 기법 관련 자료 구조 및 솔버

• SAT 대회는 SAT 솔버를 비교하는 연례 대회이다.^[34] SAT 솔버는 Alloy와 같은 형식 기법 도구에 사용된다.^[35]
• CASC는 자동 정리 증명기의 연례 대회이다.
• SMT-COMP는 형식 검증에 적용되는 SMT 솔버의 연례 대회이다.^[36]
• CHC-COMP는 형식 검증에 적용되는 제약 혼 절(constrained Horn clauses) 솔버의 연례 대회이다.^[37]
• QBFEVAL은 모델 검사에 적용되는 참 정량화 부울 공식(true quantified Boolean formula) 솔버의 격년 대회이다.^[38][39]
• SV-COMP는 소프트웨어 검증 도구를 위한 연례 대회이다.^[40]
• SyGuS-COMP는 프로그램 합성 도구를 위한 연례 대회이다.^[41]

• 액터 모델
• 프로세스 대수
• * CSP
• * LOTOS
• * π 계산/Pi-calculus^영어
• 페트리넷
• 추상 상태 기계/Abstract State Machines^영어 (ASM)
• Alloy
• ANSI/ISO C 명세 언어/ANSI/ISO C Specification Language^영어 (ACSL)
• B-Method
• CADP
• Common Algebraic Specification Language (CASL)
• Esterel
• Lustre
• mCRL2
• Perfect Developer
• RAISE
• Rebeca Modeling Language/Rebeca Modeling Language^영어
• SPARK Ada/SPARK (programming language)^영어
• Specification and Description Language (SDL)
• Temporal logic of actions (TLA)
• uppaal
• USL
• VDM
• * VDM-SL
• * VDM++
• Z 언어

• SPIN
• PAT
• MALPAS Software Static Analysis Toolset

6. 한계 및 비판

정형 기법은 사람의 손으로 하는 증명이나 자동적인 증명 모두 많은 시간과 비용을 필요로 한다.^[52] 따라서 형식 기법은 그 비용이 충분히 이익에 부합하거나, 오류의 혼입이 막대한 손해로 이어지는 경우에만 사용된다. 예를 들어, 항공 우주 공학에서는 오류가 발생하면 사망 사고로 이어질수 있기 때문에, 다른 분야보다 형식 기법이 일반화되어 있다.^[52]

일부에서는 정형 기법이 소프트웨어 위기의 특효약이 될 것이라고 주장하지만, 많은 사람들은 소프트웨어 위기에 특효약은 존재하지 않는다고 생각하며, 형식 기법의 이점을 지나치게 강조하는 자세를 문제 삼기도 한다.^[52]

7. 관련 단체

• BCS-FACS
• 유럽 정형 기법 협회(Formal Methods Europe)
• Z 사용자 그룹

참조

_[1] 웹사이트 What is Formal Methods? http://shemesh.larc.[...] 2001-08-06
_[2] 간행물 Why Engineers Should Consider Formal Methods http://klabs.org/ric[...] 16th Digital Avionics Systems Conference (27–30 October 1997)
_[3] 문서 Monin, pp.3-4
_[4] 간행물 Teaching formal methods lite via testing https://onlinelibrar[...] 2001-08-31
_[5] conference The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference UNESCO
_[6] 문서 Backus Normal Form vs Backus Naur Form 1964
_[7] 서적 Algol-like Languages 1997
_[8] 간행물 Program Synthesis https://www.nowpubli[...] 2017
_[9] 문서 Widening and Narrowing Operators for Abstract Interpretation Elsevier 2011
_[10] 서적 Logics of Specification Languages 2008
_[11] 서적 Handbook of Model Checking 2018
_[12] 서적 Handbook of Model Checking 2018
_[13] 간행물 A survey of recent advances in SAT-based formal verification 2005-01-25
_[14] 서적 History of Nordic Computing 3: IFIP Advances in Information and Communication Technology Springer
_[15] conference FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings http://www.imm.dtu.d[...] Springer
_[16] 문서 Unmanned aerial systems integration to National Airspace System IEEE 2008-11-01
_[17] 웹사이트 Airborne Coordinated Conflict Resolution and Detection http://shemesh.larc.[...] 2016-03-05
_[18] 웹사이트 Atelier B http://www.atelierb.[...]
_[19] 문서 A simple method for parameterized verification of cache coherence protocols https://www.student.[...] 2004
_[20] 웹사이트 Formal Verification in Intel Core i7 Processor Execution Engine Validation http://cps-vo.org/no[...] 2015-05-03
_[21] 문서 Verified optimizations for the Intel IA-64 architecture Springer Berlin Heidelberg 2004
_[22] 문서 Best known methods for using Cadence Conformal LEC http://citeseerx.ist[...]
_[23] 문서 Functional verification of power gated designs by compositional reasoning ftp://nozdr.ru/bibli[...] Springer Berlin Heidelberg
_[24] 문서 Automatic verification of fault-tolerant register emulations https://core.ac.uk/d[...]
_[25] 문서 Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems https://ieeexplore.i[...]
_[26] 서적 X2R-2, deliverable D5.1
_[27] 문서 Lightweight Formal Methods http://people.csail.[...] 1996-04-01
_[28] 웹사이트 Application of Lightweight Formal Methods in Requirement Engineering http://www.stsc.hill[...] 2006-03-01
_[29] 문서 Alloy: A Lightweight Object Modelling Notation http://people.csail.[...] 2002-04-01
_[30] 서적 Succeeding with Use Cases: Working Smart to Deliver Quality Addison-Wesley Professional Publishing 2005
_[31] 웹사이트 A Lightweight Approach to Formal Methods http://home0.inet.te[...] Springer-Verlag 2006-03-09
_[32] 웹사이트 ESBMC http://esbmc.org/
_[33] 서적 Tools and Algorithms for the Construction and Analysis of Systems Springer International Publishing 2019
_[34] 간행물 SAT Competition 2020 2021-12-01
_[35] 서적 Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering Association for Computing Machinery 2021-01-27
_[36] 논문 6 Years of SMT-COMP https://doi.org/10.1[...] 2013-03-01
_[37] 논문 Competition Report: CHC-COMP-21 2021-09-13
_[38] 서적 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI) IEEE 2019-11
_[39] 논문 The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) 2019-09-01
_[40] 서적 Tools and Algorithms for the Construction and Analysis of Systems Springer International Publishing 2022
_[41] 논문 SyGuS-Comp 2017: Results and Analysis 2017-11-28
_[42] 웹사이트 What is Formal Methods? http://shemesh.larc.[...] 2001-08-06
_[43] 논문 Why Engineers Should Consider Formal Methods http://klabs.org/ric[...] 16th Digital Avionics Systems Conference (27–30 October 1997)
_[44] 문서 2003
_[45] 뉴스 Lightweight Formal Methods http://people.csail.[...] IEEE Computer 1996-04
_[46] 뉴스 Application of Lightweight Formal Methods in Requirement Engineering http://www.stsc.hill[...] Crosstalk: The Journal of Defense Software Engineering 2003-01
_[47] 논문 Alloy: A Lightweight Object Modelling Notation http://people.csail.[...] 2002-04
_[48] 서적 Succeeding with Use Cases: Working Smart to Deliver Quality Addison-Wesley Professional Publishing 2005
_[49] 간행물 A Lightweight Approach to Formal Methods http://home0.inet.te[...] Springer-Verlag 1998-10
_[50] 간행물 The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference UNESCO 1959
_[51] 간행물 Backus Normal Form vs Backus Naur Form 1964
_[52] 서적 銀の弾などない 1986
_[53] 웹인용 What is Formal Methods? http://shemesh.larc.[...] 2001-08-06
_[54] 저널 인용 Why Engineers Should Consider Formal Methods http://klabs.org/ric[...] 16th Digital Avionics Systems Conference (27–30 October 1997)
_[55] 문서