형식적인 방법

Formal methods

컴퓨터 과학에서 공식 방법은 소프트웨어 및 하드웨어 [1]시스템의 사양, 개발 및 검증을 위한 수학적으로 엄격한 기술입니다.소프트웨어 및 하드웨어 설계를 위한 공식 방법의 사용은 다른 공학 분야와 마찬가지로 적절한 수학적 분석을 수행하는 것이 [2]설계의 신뢰성과 견고성에 기여할 수 있다는 기대에 의해 동기 부여된다.

공식 방법은 논리 계산, 형식 언어, 자동 이론, 제어 이론, 프로그램 의미론, 유형 시스템 및 유형 [3]이론을 포함한 다양한 이론적 컴퓨터 과학 기초를 사용합니다.

배경

세미포멀 메서드는 완전히 "포멀"로 간주되지 않는 형식주의 및 언어입니다.의미론을 완성하는 작업을 나중 단계로 늦추고, 그 작업은 인간의 해석에 의해 수행되거나 코드나 테스트 케이스 [4]생성기와 같은 소프트웨어를 통한 해석에 의해 수행된다.

분류법

정식 메서드는 여러 수준에서 사용할 수 있습니다.

레벨 0: 정식 사양을 수행한 후 이를 통해 비공식적으로 프로그램을 개발할 수 있습니다.이를 정식 메서드 라이트라고 부릅니다.이것은 많은 경우 가장 비용 효율이 높은 옵션일 수 있습니다.

레벨 1: 정식 개발 및 정식 검증을 사용하여 보다 정식적인 방법으로 프로그램을 제작할 수 있습니다.예를 들어, 명세서에서 프로그램으로의 특성 증명 또는 개량을 실시할 수 있다.이는 안전 또는 보안을 수반하는 높은 무결성 시스템에 가장 적합합니다.

레벨 2: 정리 프로버는 완전 정식 기계 점검 증명에 사용할 수 있습니다.툴의 개선이나 코스트의 삭감에 수반해, 코스트가 매우 비싸고, 실수의 코스트가 매우 높은 경우(예를 들면, operating system이나 마이크로프로세서 설계의 중요한 부분)에만, 실질적으로 가치가 있습니다.

이에 대한 자세한 내용은 다음과 같습니다.

프로그래밍 언어 의미론과 마찬가지로 형식 메서드의 스타일은 대략 다음과 같이 분류할 수 있습니다.

  • 표현적 의미론, 영역의 수학적 이론에서 시스템의 의미가 표현되는 의미론.이러한 방법의 지지자들은 시스템에 의미를 부여하기 위해 잘 이해된 도메인의 특성에 의존합니다. 비평가들은 모든 시스템이 직관적으로나 자연스럽게 기능적으로 보이지 않을 수 있다고 지적합니다.
  • 시스템의 의미가 (추정적으로) 단순한 계산 모델의 일련의 동작으로 표현되는 운영 의미론.이러한 방법의 지지자들은 표현 명확성을 위한 수단으로 모델의 단순성을 지적한다. 비평가들은 의미론 문제가 지연되었다고 반박한다(간단한 모델의 의미론을 정의하는 것은 누구인가?).
  • 시스템이 작업을 수행하기 전과 후에 각각 참인 전제조건과 사후조건의 관점에서 시스템의 의미를 표현하는 공리적인 의미론.찬성론자들은 고전 논리와의 연관성에 주목한다; 비판론자들은 그러한 의미론들이 시스템이 실제로 무엇을 하는지 설명하지 않는다고 지적한다(단순히 전후로 무엇이 진실인지).

경량 포멀 방식

일부 실무자들은 공식 방법 커뮤니티가 규격 또는 [5][6]설계의 완전한 공식화를 지나치게 강조했다고 생각한다.그들은 관련된 언어의 표현력과 모델링되는 시스템의 복잡성으로 인해 완전한 형식화가 어렵고 비용이 많이 든다고 주장한다.대안으로 부분 사양과 집중 적용을 강조하는 다양한 경량 형식 방법이 제안되었다.공식 방법에 대한 이러한 경량 접근방식의 예로는 합금 객체 모델링 표기법,[7] Denney가 Z 표기법의 일부 측면을 유스케이스 주도 [8]개발로 통합한 것, CSK VDM Tools [9]등이 있습니다.

사용하다

개발 과정을 통해 다양한 지점에서 정식 방법을 적용할 수 있습니다.

사양

공식 방법을 사용하여 개발 대상 시스템에 대한 설명을 원하는 세부 수준에서 제공할 수 있습니다.이 공식 설명은 추가 개발 활동을 안내하기 위해 사용할 수 있습니다(다음 섹션 참조). 또한 개발 중인 시스템의 요건이 완전하고 정확하게 지정되었는지 확인하거나 정확하고 모호하지 않은 공식 언어로 시스템 요건을 표현하여 공식화할 수 있습니다.정의된 구문과 의미론입니다.

공식 사양 시스템의 필요성은 수년간 지적되어 왔습니다.ALGOL 58 [10]보고서에서 John Backus는 프로그래밍 언어 구문을 기술하기 위한 공식 표기법을 제시했는데, 나중에 Backus normal 형식으로 명명되고 Backus-Naur 형식(BNF)[11]으로 이름이 변경되었습니다.Backus는 또한 구문적으로 유효한 ALGOL 프로그램의 의미에 대한 공식적인 설명이 보고서에 포함될 때까지 완료되지 않았다고 썼다."따라서 법률 프로그램의 의미론에 대한 공식적인 처리는 다음 논문에 포함될 것입니다."그것은 나타나지 않았다.

발전

정식 개발은 도구 지원 시스템 개발 프로세스의 통합 부분으로서 정식 방법을 사용하는 것입니다.

정식 사양이 작성되면 설계 프로세스 중에 콘크리트 시스템이 개발되는 동안(즉, 소프트웨어에서 일반적으로 실현되지만 하드웨어에서도 실현될 수 있음) 이 사양은 가이드로 사용할 수 있다.예를 들어 다음과 같습니다.

  • 형식 사양이 운영 의미론일 경우, 구체적인 시스템의 관찰된 동작을 사양의 동작(실행 가능 또는 시뮬레이션 가능해야 함)과 비교할 수 있습니다.또, 사양의 조작 커맨드는, 실행 가능한 코드로의 직접 변환을 실시할 수 있다.
  • 형식 사양이 자명한 의미론일 경우, 사양의 전제 조건 및 사후 조건은 실행 가능한 코드에서 어설션이 될 수 있다.

검증

형식 검증은 소프트웨어 도구를 사용하여 정식 사양의 속성을 증명하거나 시스템 구현의 형식 모델이 사양을 충족함을 증명하는 것입니다.

일단 정식 규격이 개발되면, 규격은 규격의 속성을 증명하기 위한 기초로서, 그리고 추론에 의해 시스템 구현의 속성을 증명하기 위한 기초로서 사용될 수 있다.

사인오프 확인

사인오프 검증은 신뢰성이 높은 정식 검증 툴을 사용하는 것입니다.이러한 툴은 기존의 검증 방법을 대체할 수 있습니다(인정된 툴도 있습니다).

인간이 지시하는 증거

때때로, 시스템의 정확성을 증명하는 동기는 시스템의 정확성에 대한 확신에 대한 명백한 요구가 아니라 시스템을 더 잘 이해하고자 하는 욕구입니다.그 결과, 정확성의 일부 증명은 수학적 증명 스타일로 생산된다. 즉, 자연어를 사용하여 손으로 쓴(또는 조판) 증명에 공통적인 비공식적 수준을 사용한다."좋은" 증거는 다른 인간 독자들이 읽고 이해할 수 있는 것이다.

이러한 접근법에 대한 비판자들은 자연어에 내재된 모호성이 이러한 증명에서 오류를 발견하지 못하게 한다고 지적한다; 종종, 그러한 증명에서 일반적으로 간과되는 낮은 수준의 세부 사항에서 미묘한 오류가 존재할 수 있다.또한, 이러한 좋은 증거를 만들기 위한 작업은 높은 수준의 수학적 정교함과 전문성을 필요로 합니다.

자동화된 증명

이와는 대조적으로, 이러한 시스템의 정확성을 증명하는 자동화된 방법에 대한 관심이 높아지고 있다.자동화된 기술은 세 가지 일반적인 범주로 분류됩니다.

  • 자동 정리 증명.시스템에 대한 설명, 논리 공리 세트 및 추론 규칙 세트가 주어지고 시스템이 처음부터 정식 증명을 생성하려고 시도합니다.
  • 모델 체크: 시스템이 실행 중에 입력될 수 있는 모든 가능한 상태를 철저히 검색하여 특정 속성을 검증합니다.
  • 추상적 해석: 시스템이 프로그램을 나타내는 (아마도 완전한) 격자에 대한 고정점 계산을 사용하여 프로그램의 행동 속성의 과도한 근사치를 검증합니다.

어떤 자동 정리 프로버는 어떤 특성이 추구하기에 충분히 "흥미로운"지에 대한 지침을 필요로 하는 반면, 다른 것들은 인간의 개입 없이 일한다.모델 체커는 충분히 추상적인 모델이 주어지지 않으면 수백만 개의 재미없는 상태를 확인하는 데 금방 빠져들 수 있습니다.

이러한 시스템의 지지자들은 모든 지루한 세부 사항들이 알고리즘적으로 검증되었기 때문에 결과가 인간이 만든 증거보다 수학적 확실성이 더 크다고 주장한다.또한 이러한 시스템을 사용하기 위해 필요한 훈련은 손으로 좋은 수학적 증거를 만드는 데 필요한 훈련보다 적기 때문에 다양한 실무자들이 이 기술에 접근할 수 있다.

비평가들은 그 시스템들 중 일부는 신탁과 같다고 지적한다: 그들은 진실을 발표하지만, 그 진실에 대해서는 아무런 설명도 하지 않는다.검증에 도움이 되는 프로그램 자체가 검증되지 않으면 결과의 건전성을 의심할 이유가 있을 수 있다.일부 최신 모델 검사 도구는 증빙의 각 단계를 자세히 설명하는 "증빙 로그"를 생성하므로 적절한 도구가 제공되면 독립적인 검증을 수행할 수 있습니다.

추상적 해석 접근법의 주요 특징은 건전한 분석을 제공한다는 것이다. 즉, 잘못된 부정은 반환되지 않는다.또, 분석 대상의 성질을 나타내는 추상 영역을 튜닝 해, 확폭[12] 연산자를 적용해 고속의 컨버전스를 실현하는 것으로, 효율적으로 측정할 수 있다.

적용들

정식 방법은 라우터, 이더넷스위치, 라우팅 프로토콜, 보안 애플리케이션, seL4 등의 운영체제 마이크로커널 등 하드웨어 및 소프트웨어의 다양한 영역에 적용됩니다.DC에서[clarification needed] 사용되는 하드웨어 및 소프트웨어의 기능을 검증하기 위해 사용되는 예는 몇 가지 있습니다.IBM은 AMD x86 프로세서 개발 [citation needed]프로세스에서 정리 프로세서인 ACL2를 사용했습니다.인텔은 이러한 방법을 사용하여 하드웨어와 펌웨어를 검증합니다(읽기 전용 [citation needed]메모리에 프로그램된 영구 소프트웨어).Dansk Datamatik 센터는 1980년대에 정식 방법을 사용하여 에이다 프로그래밍 언어를 위한 컴파일러 시스템을 개발하였고, 이는 오래 지속된 상용 [13][14]제품이 되었다.

에는 나사의 차세대 항공 교통 System[표창 필요한], 국립 영공 System,[15]과 주요국 갈등 해결과 검출에 무인 항공기 시스템 통합 등에서 공식적인 방법 적용된다 B-Method 아틀리에 B,[17]이 안전 automa을 개발하는 데 사용되는 몇몇 다른 작업(ACCoRD)[16] 있다.다양한은 지하철 Tisms.Alstom 및 Siemens에 의해 전 세계에 설치되었으며, 또한 ATMEL 및 STMicroelectronics에 의한 공통 기준 인증 및 시스템 모델 개발을 위해 설치되었습니다.

IBM, Intel 및 AMD와 같은 대부분의 유명 하드웨어 벤더가 하드웨어에서 공식 검증을 자주 사용해 왔습니다.하드웨어가의 인텔cache-coherent protocol,[18]인텔 코어 i7 프로세서 실행 엔진 유효성 검사[19](, BDDs다는 것을 증명하고 상징적인 평가 정리를 사용하여), 인텔 IA-64 건축 HOL 빛 정리를 사용하여 경로에 대한 최적화 증명의 매개 변수 확인 같은 제품의 근무를 확인할 FMs 사용된 많은 지역이 있다.r,[20]고PCI Express 프로토콜 및 Cadence를 [21]사용한 인텔의 고급 관리 테크놀로지를 지원하는 고성능 듀얼 포트 기가비트 이더넷 컨트롤러 검증마찬가지로 IBM은 IBM Power7 마이크로프로세서의 [24]파워게이트,[22] 레지스터 [23]및 기능 검증에 공식적인 방법을 사용했습니다.

소프트웨어 개발 중

소프트웨어 개발에서 정식 방법은 소프트웨어(및 하드웨어) 문제를 요건, 사양 및 설계 수준에서 해결하기 위한 수학적 접근법입니다.정식 방법은 항전 소프트웨어 등의 안전 또는 보안에 중요한 소프트웨어 및 시스템에 적용될 가능성이 높습니다.DO-178C와 같은 소프트웨어 안전보증 표준은 보완을 통한 공식 방법의 사용을 허용하며, 공통 기준은 최고 수준의 분류에서 공식 방법을 요구한다.

순차 소프트웨어의 경우 형식 방법의 예로는 B-Method, 자동 정리 증명에 사용되는 사양 언어, RAISE 및 Z 표기법이 있습니다.

기능 프로그래밍에서, 속성 기반 테스트는 개별 함수의 예상 동작에 대한 수학적 사양 및 테스트(전체 테스트는 아닐지라도)를 가능하게 했다.

객체 제약 언어(및 Java 모델링 언어 등의 전문화)는 객체 지향 시스템을 반드시 공식적으로 검증할 필요는 없지만 공식적으로 지정할 수 있도록 허용했습니다.

동시 소프트웨어 및 시스템의 경우, Petri nets, 프로세스 대수 및 유한 상태 머신(가상 유한 상태 머신 또는 이벤트 기반 유한 상태 머신 참조)은 실행 가능한 소프트웨어 사양을 허용하고 애플리케이션 동작을 구축하고 검증하는 데 사용할 수 있습니다.

소프트웨어 개발에서 공식적인 방법에 대한 또 다른 접근법은 어떤 형태의 논리(일반적으로 First-order Logic(FOL; 1차 논리)의 변형)로 사양을 작성한 후 프로그램인 것처럼 직접 논리를 실행하는 것입니다.Description Logic(DL; 설명 논리)에 근거한 OWL 언어가 그 예입니다.또한 논리를 직접 실행할 뿐만 아니라 영어의 일부 버전(또는 다른 자연 언어)을 자동으로 논리 간에 매핑하는 작업도 있습니다.예를 들어 Attemo Controlled English 및 Internet Business Logic은 어휘 또는 구문을 제어하려고 하지 않습니다.양방향 영어-로직 매핑과 로직의 직접 실행을 지원하는 시스템의 특징은 비즈니스 또는 과학 수준에서 [citation needed]결과를 영어로 설명할 수 있다는 것입니다.

정식 방법 및 표기법

사용 가능한 공식 방법 및 표기법에는 여러 가지가 있습니다.

사양 언어

모델 체커

주요 기사:모델 확인 도구 목록
  • ESBMC[25]
  • MALPAS Software Static Analysis Toolset – 안전에 중요한 시스템의 정식 증명에 사용되는 산업용 강도 모델 검사기
  • PAT – 동시 시스템 및 CSP 확장(공유 변수, 어레이, 공정성 등)을 위한 무료 모델 체커, 시뮬레이터 및 미세 조정 체커
  • 회전하다
  • 우파알

단체들

메인 페이지:카테고리:정식 방법 조직

「 」를 참조해 주세요.

레퍼런스

  1. ^ Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ^ Holloway, C. Michael. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from the original (PDF) on 16 November 2006. Retrieved 2006-11-16. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)
  3. ^ 모닌, 페이지 3-4
  4. ^ X2R-2, deliverable D5.1.
  5. ^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, 1996년 4월
  6. ^ Vinu George와 Rayford Vaughn, "요건 엔지니어링에서의 경량 형식 방식 적용" 2006-03-01년 Wayback Machine, Crosstalk: 국방 소프트웨어 엔지니어링 저널, 2003년 1월
  7. ^ Daniel Jackson, "Alloy: 경량 객체 모델링 표기법", 소프트웨어 엔지니어링 및 방법론에 관한 ACM 트랜잭션(TOSEM), 제11권, 제2호(2002년 4월), 페이지 256-290
  8. ^ Richard Denney, 사용 사례 성공: 품질을 제공하는 스마트한 작업, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  9. ^ Sten Agerholm과 Peter G. Larsen, "A Lightweight approach to Formal Methods" 2006-03-09, Boppard, Germal, Springer-Verlag, 1998년 10월, Wayback Machine에서 아카이브된 "포멀 메서드의 경량화 접근법"
  10. ^ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
  11. ^ Knuth, Donald E.(1964), Backus Normal Form vs Backus Naur Form.ACM 통신, 7(12) : 735 ~736 。
  12. ^ A. Cortesi와 M. Zanioli, 추상 해석을 위한 확대 및 축소 연산자.컴퓨터 언어, 시스템 및 구조제37권(1), 페이지 24-42, 엘세비어, ISSN 1477-8424 (2011).
  13. ^ Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.
  14. ^ Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings (PDF). Springer. pp. 42–61.
  15. ^ Gheorghe, A. V. 및 Ancel, E. (2008년, 11월)무인항공시스템이 국립공역시스템으로 통합되었습니다.인프라스트럭처 시스템 및 서비스:밝은 미래를 위한 네트워크 구축(INFRA), 2008년 제1회 국제회의(1-5페이지).IEEE.
  16. ^ 공중 조정 충돌 해결 및 탐지, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  17. ^ "Atelier B". www.atelierb.eu.
  18. ^ C. T. Chou, P. K. Mannava, S. Park, "캐시 일관성 프로토콜의 매개 변수화된 검증을 위한 간단한 방법", 컴퓨터 지원 설계의 형식 방법, 382–398, 2004.
  19. ^ 인텔®Core™i7 프로세서 이그제큐션 엔진 검증의 정식 검증, http://cps-vo.org/node/1371, 는 2013년 9월 13일에 액세스 합니다.
  20. ^ J. Grundy, "인텔 IA-64 아키텍처를 위한 검증된 최적화", Springer Berlin Heidelberg, 2004 페이지 215-232.
  21. ^ E. Seligman, I. Yarom, 인텔의 "Cadence Conformal LEC를 사용하는 가장 알려진 방법"
  22. ^ C. 아이스너, A.나히르, K.Yorav, "구성 추론에 의한 동력 게이트 설계의 기능 검증", 컴퓨터 지원 검증, 스프링거 베를린 하이델베르크, 페이지 433–445.
  23. ^ P. C. Attie, H. Chockler, "내결함성 레지스터 에뮬레이션의 자동 검증", 이론 컴퓨터 과학 전자 노트, vol. 149, no. 1, 페이지 49-60.
  24. ^ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "IBM POWER7 마이크로프로세서 및 POWER7 멀티프로세서 시스템의 기능 검증", IBM Journal of Research and Volvelopment, 55,
  25. ^ "ESBMC". esbmc.org.

추가 정보

외부 링크

아카이브 자료