실제 프로그램 검증

몇 가지 질문에 대해 간결한 답변을 드리겠습니다.이것은 엄격히 제 연구 분야가 아니므로 제 정보 중 일부는 오래되었거나 부정확 할 수 있습니다.

1. 특별히 속성을 증명하기 위해 특별히 고안된 많은 도구가 있습니다. Java 및 C ++의.

   하지만 여기서 약간의 여담이 필요합니다. 프로그램의 정확성을 증명한다는 것은 무엇을 의미합니까? Java 유형 검사기는 Java 프로그램의 공식 속성을 증명합니다. 즉, float 및 int 추가와 같은 특정 오류는 나오다! 나는 당신이 훨씬 더 강력한 속성, 즉 당신의 프로그램이 결코 원치 않는 상태에 들어갈 수 없거나 특정 함수의 출력이 특정 수학적 사양을 따르는 것에 관심이 있다고 생각합니다. 간단히 말해서, 간단한 보안 속성에서 프로그램이 세부 사양을 충족한다는 완전한 증명에 이르기까지 “프로그램이 올바른지 증명하는 것”이 의미하는 바에 대한 광범위한 변화가 있습니다.

   이제 저는 다음과 같이 가정하겠습니다. 프로그램에 대한 강력한 속성을 입증하는 데 관심이 있습니다. 보안 속성에 관심이 있다면 (프로그램이 특정 상태에 도달 할 수 않음 ) 일반적으로 가장 좋은 방법은 모델 검사 . 그러나 Java 프로그램의 동작을 완전히 지정하려는 경우 가장 좋은 방법은 해당 언어에 대한 사양 언어를 사용하는 것입니다 (예 : JML . C 프로그램의 동작을 지정하는 언어 (예 : ACSL )가 있지만 C ++.

2. 사양이 확보되면 프로그램이 해당 사양을 준수 함을 증명해야합니다.

   이를 위해서는 둘 다에 대한 공식적인 이해 적절성 정리 를 표현하기위한 언어 (Java 또는 C ++)의 사양 및 작동 의미, 즉 실행 프로그램의 사양을 존중합니다.

   이 도구를 사용하면 해당 정리의 증거를 공식화하거나 생성 할 수도 있습니다. 이제이 두 작업 (지정 및 증명)은 매우 어렵 기 때문에 두 가지로 분리되는 경우가 많습니다.

   • 코드, 사양을 구문 분석하고 적절성 정리를 생성하는 하나의 도구입니다. Frank가 언급했듯이 Krakatoa 는 이러한 도구의 예입니다.

   • 정리를 증명하는 도구 ( s), 자동 또는 대화식. Coq는 이러한 방식으로 Krakatoa와 상호 작용하며 Z3 와 같은 강력한 자동화 도구도 사용할 수 있습니다.

   한 가지 (사소한) 요점 : 자동화 된 방법으로 증명하기에는 너무 어려운 몇 가지 정리가 있으며, 자동 정리 증명에는 때때로 안정성이 떨어지는 버그가있는 것으로 알려져 있습니다. 이것은 Coq가 비교하여 빛을 발하는 영역입니다 (그러나 자동이 아닙니다!).

3. Ocaml 코드를 생성하려면 먼저 Coq (Gallina)로 작성하십시오. 그런 다음 코드를 추출하십시오. 그러나 Coq는 가능하다면 C ++ 또는 Java 생성에 끔찍합니다.

4. 위의 도구가 스레딩 및 성능 문제를 처리 할 수 있습니까? 성능 및 스레딩 문제는 특히 어려운 문제이기 때문에 특별히 설계된 도구로 가장 잘 처리 할 수 있습니다. Martin Hofmann의 PolyNI 프로젝트가 흥미로워 보이지만 여기에 추천 할 도구가 있는지 잘 모르겠습니다.

결론 : “실제”Java 및 C ++ 프로그램의 공식 검증은 크고 잘 개발 된 분야이며 Coq는 해당 작업의 일부에 적합합니다. 예를 들어 여기 에서 개략적 인 개요를 찾을 수 있습니다.

댓글

• 이 게시물과 추가 한 참조에 감사드립니다. IMHO, 소프트웨어 엔지니어의 목표는 1) 항상 올바른 결과를 제공하고 2) 절대 실패하지 않는 시스템을 신속하게 출시 할 수 있도록하는 것입니다. 여기서 회귀 문제를 볼 수 있습니다. 여기서 사양 자체가 ” 버그가 없음 ” 🙂 종류의 메타 언어를 사용하여 ” 진정한 언어 제안 “을 정의하려고 시도한 다음 다른 메타 언어가 필요합니다. 하나 …
• 문제는 사용자가 ” 원하는 “가 일반적으로 형식으로 표현되지 않는다는 것입니다. 언어! 일반적으로 질문에 대한 공식 답변은 없습니다. “이 공식 사양이 내 비공식 아이디어와 일치합니까? “. 공식 사양을 테스트 하고 특정 수학적 속성이 있음을 증명하는 것이 ‘ 가능하지만 궁극적으로 수학을 실제 세계와 연결해야합니다. 이것은 비공식적 인 과정입니다.
• 물론입니다. 저는 항상 공식적인 방법이 잘 정의 된 지점에서만 시작할 수 있다는 것을 깨달았습니다.해당 사양이 실제 사용자의 의식적 / 무의식적 / 발견되지 않은 요구 사항을 준수하는지 여부는 공식적인 방법으로는 처리 할 수없는 또 다른 문제입니다 (하지만 확실히 엔지니어에게는 문제임).
• 정리는 정의상 a입니다. 증명 된 명제. 따라서 ” 정리를 증명하려는 것은 아닙니다 “.
• @nbro Wikipedia도 동의하는 것 같습니다. 너와 함께. 그러나 Mathworld는 ” 할 수있는 수학적 연산이 참임을 증명할 수있는 명제로 정리를 정의합니다. “. 이 경우 정리 증명을 제공하는 것은 가능할뿐만 아니라 그들을 그렇게 부르는 것을 정당화하는 데 필요합니다! 🙂 (물론 대위법입니다.)

세 가지 주목할만한 응용 프로그램을 언급하고 싶습니다. 산업 또는 사소하지 않은 실제 시스템의 공식 방법 / 공식 검증 도구. 이 주제에 대한 경험이 거의 없으며 논문을 통해서만 배울 수 있습니다.

1. 오픈 소스 도구 Java Pathfinder (줄여서 JPF) 2005 년 NASA에서 출시 는 실행 가능한 Java 바이트 코드 프로그램을 확인하는 시스템입니다 ( Java Pathfinder @ wiki ). NASA Ames에서 K9 Rover 용 실행 소프트웨어의 불일치를 감지하는 데 사용되었습니다.

2. 이 문서 : 모델 검사를 사용하여 심각한 파일 시스템 오류 찾기 @OSDI “04 는 사용 방법을 보여줍니다. 모델 검사를 통해 파일 시스템의 심각한 오류를 찾습니다. FiSC라는 시스템은 널리 사용되는 세 개의 파일 시스템 인 ext3, JFS, ReiserFS에 적용되었으며 32 개의 심각한 버그가 발견되었습니다. Best Paper Award를 수상했습니다.

3. 이 문서 : Amazon Web Services가 형식적인 메서드를 사용하는 방법 @CACM “15 는 AWS가 형식적인 메서드를 적용하는 방법을 설명합니다. S3, DynamoDB, EBS 및 내부 분산 잠금 관리자와 같은 제품. Lamport의 TLA + 도구에 중점을 둡니다. 그런데 Lamport는 자체 TLA 도구 상자를 집중적으로 사용했습니다. 그는 종종 TLA에서 (아주 완전한) 공식 검증을 제공합니다. 논문의 부록에서 자신 (공저자 포함)이 제안한 알고리즘 / 이론의 목록.

이제 안전이 중요한 임베디드 시스템 용으로 설계된 C ++의 하위 집합으로 작성된 프로그램에 대해 공식 검증이 가능합니다. http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt를 참조하십시오. 짧은 프레젠테이션, http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf 전체 논문입니다.

댓글

• 링크에 감사드립니다. 특히 링크가 기업 웹 사이트로 연결되어 있기 때문에 링크 부패를 방지하기 위해 적어도 해당 콘텐츠에 대한 간략한 개요가 유용 할 것입니다. 이들은 주기적으로 재구성되어 사이트로 연결되는 모든 링크를 제거하는 경향이 있습니다.

공식 프로그램의 사양은 다른 프로그래밍 언어로 작성된 프로그램입니다. 결과적으로 사양에는 확실히 자체 버그가 포함됩니다.

정식 검증의 장점은 프로그램과 사양이 두 개의 개별 구현이므로 버그가 달라진다는 것입니다. 그러나 항상 그런 것은 아닙니다. 버그의 공통 소스 중 하나 인 간과 된 사례가 종종 일치합니다. 따라서 공식 검증은 만병 통치약이 아닙니다. 여전히 사소한 버그 수를 놓칠 수 있습니다.

공식 검증의 단점은 구현 비용의 두 배, 아마도 더 많은 것을 부과 할 수 있다는 것입니다. 공식 사양의 전문가이며 함께 제공되는 다소 실험적인 도구를 사용해야합니다.이 도구는 저렴하지 않습니다.

테스트 케이스를 설정하고이를 실행하기위한 스캐 폴딩을 사용합니다. 자동으로 시간을 더 효율적으로 사용할 수 있습니다.

댓글

• 공식 검증의 장점 은 … . 공식 검증의 두 번째 단점 은 … 이것은 혼란 스럽습니다.
• 사양과 비공식 작업 간의 불일치는 프로그래밍 문제가 아닌 소프트웨어 요구 사항 분석 문제라고 생각합니다.

몇 가지 다른 질문을합니다. 나는 산업 / 상업용 응용 프로그램에 대한 공식적인 검증 방법이 그다지 일반적이지 않다는 데 동의합니다. 그러나 프로그램의 정확성을 결정하기 위해 많은 “형식적 검증”원칙이 컴파일러에 내장되어 있음을 알아야합니다! 따라서 최신 컴파일러를 사용하는 경우 “정식 검증에 최신 기술을 많이 사용하게됩니다.

“나는 테스트에 지쳤습니다 “라고 말하지만 공식 검증은 실제로 테스트를 대신 할 수 없습니다. 테스트에서 변형 입니다.

자바를 언급합니다.실제로 대규모 코드베이스에서 실행할 수있는 FindBugs 라는 Java 검증 프로그램에 내장 된 많은 고급 공식 검증 방법이 있습니다. “가양 성 및 거짓 음성”이 모두 나타나며 결과는 인간 개발자가 검토 / 분석해야합니다. 그러나 실제 기능적 결함을 나타내지 않더라도 일반적으로 코드에서 피해야하는 “반 패턴”이 나타납니다.

“산업용”이외의 특정 애플리케이션에 대해서는 더 이상 언급하지 않습니다. . 실제로 공식 검증은 특정 애플리케이션에 의존하는 경향이 있습니다.

공식 검증 기술은 EE에서 회로 정확성을 증명하기 위해 널리 사용되는 것 같습니다. 마이크로 프로세서 설계

다음은 Lars Philipson 이 EE 분야의 공식 검증 도구를 조사한 예입니다.

댓글

• ‘는 ” a 많은 ” 공식 검증 ” 원칙이 프로그램 정확성을 결정하기 위해 컴파일러에 내장되어 있습니다 “. 당신이 언급하는 것은 일부 컴파일러가 수행하는 정적 유형 검사이지만 그 방식으로 확인 된 속성은 다소 간단합니다. 숫자와 문자열을 추가하지 마십시오. 이것은 도움이되지만 일반적으로 ” 공식 확인 “에서 이해하는 것과는 거리가 멀습니다.
• 아닙니다. 간단하고 일반적인 예이지만 정적 유형 검사를 구체적으로 참조하십시오. 널리 퍼져 있고 고급 인 imho 컴파일러 최적화 기술은 최적화 된 프로그램 변형의 동등성을 결정 / 표시하는 고급 기술을 포함하기 때문에 공식 검증 원칙과 거의 유사합니다. 따라서 여기서 ” 움직이는 골대 ” 문제를 피하는 것이 중요하며 단지 컴파일러가이를 수행하거나 빌드했다고 가정하지 않는 것이 중요합니다. 공식적인 검증이 아닙니다.
• 이것은 일반적인 이해가 아니라는 데 동의했습니다. 최적화 기술은 대략 루프 또는 서브 루틴과 같은 프로그램 동작의 모델을 만들고 해당 모델을 최적화 한 다음 동일한 것으로 입증 된 새 코드를 생성하는 것입니다. 따라서 이러한 최적화 중 일부는 공식적인 검증 원칙을 사용하는 코드 &를 재정렬하는 데 매우 정교합니다. 컴파일러에는 공식적인 검증 방법의 다른 많은 예가있는 것 같습니다. 원래 질문은 많은 사람들이 언급 한 것처럼 여러 가지 다른 질문을 던졌습니다. 여기에 포함 된 모든 질문에 답하려고하는 것은 아닙니다.
• by the JRE, Java 런타임 엔진 (예 : 동적 최적화 등)에서도 사용되는 공식적인 검증 원칙이있는 것 같습니다.
• 즉, ” 의 filmus에서 언급 한 공식 검증 “을 꿈꾸며, 키메라 추상화를 imho로, 실용적 / 실용 주의적 / 현실적인 업계는이를 대체로 인식하고 있습니다. 대규모 코드베이스는 본질적으로 $ y $ K- 라인 코드 당 $ x $ 버그 / 결함을 가지고있는 것으로 수십 년 동안 알려져 왔으며 이론 / 기술이 어떻게 발전하든 상관없이 이것은 절대 변하지 않을 것입니다. i> 인간 본성. 실제로 인간이 만든 수학적 정리는 동일한 속성을 갖지만 널리 인정되지는 않습니다!

아마도 모델 검사기가 도움이 될 수 있습니다.

http://alloytools.org/documentation.html Alloy는 모델 검사기입니다. .

Alloy를 사용한 모델 확인의 개념을 설명하는 멋진 프레젠테이션 : https://www.youtube.com/watch?v=FvNRlE4E9QQ

동일한 도구 제품군에서 “속성 기반 테스트”가 제공되며, 모두 소프트웨어의 지정된 사양 모델에 대한 반례를 찾으려고합니다.