정식 검증

Formal verification
검증주의와 혼동하지 말 것.
여기서 "검증 가능성"이 리다이렉트 됩니다.Wikipedia 정책에 대해서는 Wikipedia를 참조하십시오.검증 가능성그 외의 용도는, 검증(동음이의)을 참조해 주세요.

하드웨어 및 소프트웨어 시스템의 맥락에서 공식 검증은 [1]수학의 공식 방법을 사용하여 특정 공식 사양 또는 속성과 관련하여 시스템의 기초가 되는 의도된 알고리즘의 정확성을 증명하거나 반증하는 행위이다.

정식 검증은 암호화 프로토콜, 조합 회로, 내장 메모리를 갖춘 디지털 회로 및 소스 코드로 표현되는 소프트웨어와 같은 시스템의 정확성을 입증하는 데 도움이 됩니다.

이러한 시스템의 검증은 시스템의 추상적인 수학적 모델, 수학적 모델과 구성에 의해 다른 방법으로 알려진 시스템의 특성 사이의 대응성에 대한 공식적인 증거를 제공함으로써 이루어집니다.시스템 모델링에 자주 사용되는 수학적 객체의 예로는 유한 상태 기계, 라벨이 붙은 전이 시스템, 페트리 네트, 벡터 덧셈 시스템, 타임 오토마타, 하이브리드 오토마타, 프로세스 대수, 운영 의미론, 표시 의미론, 호어 [2]로직과 같은 프로그래밍 언어의 형식 의미론 등이 있다.

접근

한 가지 접근법과 형성은 모델 검사로, 수학 모델의 체계적 철저한 탐사로 구성됩니다(이는 유한 모델에 대해 가능하지만, 무한 상태의 집합이 추상화를 사용하거나 대칭을 이용하여 효과적으로 표현될 수 있는 일부 무한 모델에 대해서도 가능합니다).통상, 이것은 스마트한 도메인 고유의 추상화 기술을 사용해, 단일의 조작으로 상태의 그룹 전체를 고려해 컴퓨팅 시간을 단축하는 것으로, 모델내의 모든 상태와 트랜지션을 탐색하는 것으로 구성됩니다.구현 기술은 상태 공간 열거, 기호 상태 공간 열거, 추상 해석, 기호 시뮬레이션,[citation needed] 추상 정교화를 포함한다.검증되는 속성은 LTL(Linear Temporal Logic), PSL(Property Specification Language), SystemVerilog Assertions(SVA),[3] CTL(Computational Tree Logic) 등의 시간 로직으로 기술되는 경우가 많습니다.모델 체크의 큰 장점은 종종 완전 자동이라는 것입니다.그 주된 단점은 대규모 시스템으로의 일반적인 스케일이 아니라는 것입니다.심볼 모델은 일반적으로 수백 비트의 상태로 제한되지만 명시적 상태 열거에서는 상태 공간이 상대적으로 작아야 합니다.

또 다른 접근법은 연역적 검증이다.그것은 시스템과 그 사양(및 다른 주석)으로부터 시스템의 사양에 대한 준수를 암시하는 수학적 증명 의무의 집합을 생성하고, 이러한 의무들을 증명 보조자(대화적 정리 프로버) 중 하나를 사용하여 이행하는 것으로 구성된다(HOL, ACL2, Isabelle, Coq o).r PVS) 또는 자동 정리 프로세서(특히 만족도 모듈로 이론(SMT) 솔버를 포함한다).이 접근방식은 사용자가 시스템이 올바르게 작동하는 이유를 상세하게 이해하고 검증해야 하는 일련의 이론 또는 시스템 컴포넌트(예: 기능)의 사양(불변, 전제조건, 사후조건)의 형태로 검증 시스템에 이 정보를 전달해야 하는 단점이 있다.s 또는 절차) 및 서브 컴포넌트(루프 또는 데이터 구조 등)가 포함될 수 있습니다.

소프트웨어

소프트웨어 프로그램의 공식 검증에는 프로그램이 동작의 공식 사양을 충족한다는 것을 증명하는 것이 포함됩니다.형식 검증의 하위 영역에는 연역 검증(위 참조), 추상 해석, 자동 정리 증명, 형식 시스템 및 경량 형식 방법이 포함됩니다.유망한 유형 기반 검증 접근방식은 의존형 프로그래밍이며, 여기서 함수의 유형은 해당 함수의 사양(적어도 일부)을 포함하며, 코드 유형 검사는 이러한 사양에 대한 정확성을 확립한다.모든 기능을 갖춘 의존형 언어는 특별한 경우로서 연역적 검증을 지원합니다.

또 다른 보완적 접근법은 프로그램 도출으로, 일련의 정확성 보존 단계에 의해 기능 사양에서 효율적인 코드가 생성된다.이 접근방식의 예로는 Bird-Merertens 형식주의가 있으며, 이 접근방식은 구조에 의한 정확성의 또 다른 형태로 볼 수 있다.

이러한 기술은 타당할 수 있으며, 이는 검증된 속성이 의미론에서 논리적으로 추론될 수 있음을 의미하며, 즉 그러한 보장이 없음을 의미합니다.음향 기술은 모든 가능성을 포괄한 후에만 결과를 낳는다.불건전한 기법의 예로는 예를 들어 특정 수까지의 정수만 포함하면 "충분한" 결과를 얻을 수 있습니다.기술은 결정 가능하므로 알고리즘 구현이 응답 또는 결정 불가능과 함께 종료되는 것이 보증됩니다. 즉, 결코 종료되지 않을 수 있습니다.이러한 기법은 경계가 있기 때문에 건전한 기법보다 종종 더 쉽게 결정될 수 있습니다.

검증 및 검증

주요 기사:검증 및 검증

검증은 제품의 목적에 대한 적합성을 테스트하는 한 측면입니다.검증은 상호 보완적인 측면입니다.일반적으로는 전체적인 체크 프로세스를 V&V라고 부릅니다.

  • 검증: "우리는 올바른 것을 만들기 위해 노력하고 있는가?" 즉, 제품이 사용자의 실제 요구에 맞게 지정되어 있는가?
  • 검증: "만들려고 했던 것을 만들었는가?" 즉, 제품이 사양에 적합한가?

검증 프로세스는 정적/구조적 측면과 동적/동작 측면으로 구성됩니다.예를 들어 소프트웨어 제품의 경우 소스 코드를 검사하고(정적), 특정 테스트 케이스에 대해 실행할 수 있습니다(동적).검증은 통상 동적으로만 실행할 수 있습니다.즉, 제품은 일반적인 사용법과 비정형 사용법을 통해 테스트됩니다("모든 사용 사례를 만족스럽게 충족합니까?").

자동 프로그램 복구

주요 기사:자동 버그 수정

생성된 픽스의 검증에 사용되는 프로그램의 원하는 기능을 포함하여 오라클에 대해 프로그램 복구를 실시한다.간단한 예는 테스트 스위트입니다.입출력 쌍은 프로그램의 기능을 지정합니다.다양한 기법이 채용되고 있으며, 특히 만족성 모듈로 이론(SMT) 해결사 [4]및 유전자 [5]프로그래밍을 사용하여 수정 가능한 후보를 생성하고 평가합니다.전자의 방법은 결정론적인 반면 후자의 방법은 무작위화된다.

프로그램 수리는 정식 검증과 프로그램 합성의 기술을 결합합니다.정식 검증에서의 장애 현지화 기술은 합성 모듈에 의해 타깃이 될 수 있는 버그 로케이션 가능성이 있는 프로그램 포인트를 계산하기 위해 사용됩니다.복구 시스템은 검색 공간을 줄이기 위해 미리 정의된 작은 종류의 버그에 초점을 맞추는 경우가 많습니다.기존 기법의 계산 비용 때문에 산업적 사용이 제한된다.

산업용도

설계의 복잡성이 증가함에 따라 하드웨어 [6][7]업계에서 공식적인 검증 기술의 중요성이 커지고 있습니다.현재 대부분의 주요 하드웨어 기업 또는 [8]모든 기업이 공식적인 검증을 사용하고 있지만 소프트웨어 산업에서의 공식적인 검증은 여전히 [citation needed]부진합니다.이는 오류가 상업적으로 [citation needed]더 큰 의미를 갖는 하드웨어 업계의 필요성이 커진 데 기인할 수 있습니다.요소들 간의 잠재적인 미묘한 상호작용 때문에, 시뮬레이션을 통해 현실적인 가능성을 행사하는 것이 점점 더 어려워지고 있다.하드웨어 설계의 중요한 측면은 자동화된 증명 방법을 사용할 수 있기 때문에 정식 검증을 도입하기 쉽고 [9]생산성이 향상됩니다.

2011년 현재, 복수의 operating system이 정식으로 검증되고 있습니다.NICTA의 Secure Embedded L4 마이크로커널은 OK [10]Labs에서 seL4로 상업적으로 판매되고 있습니다.OSEK/VDX 기반의 실시간 운영체제 [citation needed]ORIENTAIS는 동중국사범대학에서 [citation needed]제공되고 있습니다.Green Hills Software의 SYSGO는 SYSGO입니다.OS.[11][12]

2016년 현재 예일대·컬럼비아대 중사오·룽후이 구 교수가 블록체인을 위한 [13]정식 검증 프로토콜인 CertiKOS를 개발했다.이 프로그램은 블록체인 세계 최초의 공식 검증 사례이며, 보안 [14]프로그램으로 명시적으로 사용되는 공식 검증 사례입니다.

2017년 현재 네트워크의 [16]수학적 모델을 통해 대규모 컴퓨터[15] 네트워크의 설계에 정식 검증이 적용되었으며, 새로운 네트워크 기술 범주인 의도 기반 [17]네트워킹의 일환으로 적용되고 있습니다.정식 검증 솔루션을 제공하는 네트워크 소프트웨어 벤더에는 Cisco Forward[19][20] Networks 및 Veriflow [21]Systems가 있습니다[18].

CompCert C 컴파일러는 ISO C의 대부분을 구현하는 정식 검증된 C 컴파일러입니다.

「 」를 참조해 주세요.

무료사전인 Wiktionary에서 검증가능성을 찾아보세요.

레퍼런스

  1. ^ Sanghavi, Alok (May 21, 2010). "What is formal verification?". EE Times Asia.
  2. ^ 공식 검증 소개, 캘리포니아 버클리 대학교, 2013년 11월 6일 취득
  3. ^ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog Assertions Handbook (4th ed.). CreateSpace Independent Publishing Platform. ISBN 978-1518681448.
  4. ^ Favio DeMarco; Jifeng Xuan; Daniel Le Berre; Martin Monperrus (2014). Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT. Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2014). pp. 30–39. arXiv:1404.3186. doi:10.1145/2593735.2593740. ISBN 9781450328470. S2CID 506586.
  5. ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Transactions on Software Engineering. 38 (1): 54–72. doi:10.1109/TSE.2011.104. S2CID 4111307.
  6. ^ Harrison, J. (2003). "Formal verification at Intel". 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. pp. 45–54. doi:10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8. S2CID 44585546.
  7. ^ 실시간 하드웨어 설계의 정식 검증.Portal.acm.org (1983년 6월 27일)2011년 4월 30일에 취득.
  8. ^ "Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015.
  9. ^ "Formal Verification in Industry" (PDF). Retrieved September 20, 2012.
  10. ^ "Abstract Formal Specification of the seL4/ARMv6 API" (PDF). Archived from the original (PDF) on May 21, 2015. Retrieved May 19, 2015.
  11. ^ Christoph Baumann, Bernhard Beckert, Holger Blasum 및 Thorsten Bormer 운영체제 정확성 요소 Pike의 정식 검증에서 얻은 교훈OS
  12. ^ 잭 간슬의 'Getting it Right'
  13. ^ Harris, Robin. "Unhackable OS? CertiKOS enables creation of secure system kernels". ZDNet. Retrieved June 10, 2019.
  14. ^ "CertiKOS: Yale develops world's first hacker-resistant operating system". International Business Times UK. November 15, 2016. Retrieved June 10, 2019.
  15. ^ Heller, Brandon. "Seeking truth in networking: from testing to verification". Forward Networks. Retrieved February 12, 2018.
  16. ^ Scroxton, Alex. "For Cisco, intent-based networking heralds future tech demands". Computer Weekly. Retrieved February 12, 2018.
  17. ^ Lerner, Andrew. "Intent-based networking". Gartner. Retrieved February 12, 2018.
  18. ^ Kerravala, Zeus. "Cisco brings intent based networks to the data center". NetworkWorld. Retrieved February 12, 2018.
  19. ^ "Forward Networks: Accelerating and De-risking Network Operations". Insights Success. Retrieved February 12, 2018.
  20. ^ "Getting Grounded in Intent=based Networking" (PDF). NetworkWorld. Retrieved February 12, 2018.
  21. ^ "Veriflow Systems". Bloomberg. Retrieved February 12, 2018.