공식적인 프로그램 verfication 방법이 업계에 자리가 있습니까?

Question

나는 엿볼 수 있었다 Hoare Logic 대학에서. 우리가 한 일은 정말 간단했습니다. 내가 한 대부분의 일은 while 루프, if 진술과 일련의 지시 사항이지만 더 이상 아무것도 없습니다. 이 방법은 매우 유용한 것 같습니다!

공식적인 방법은 업계에서 널리 사용됩니까?

이러한 방법은 미션 크리티컬 소프트웨어를 증명하는 데 사용됩니까?

Answer 1

이것은 내 마음에 가까운 질문입니다 (저는 공식 논리를 사용하여 소프트웨어 검증의 연구원입니다).이 기술이 유용한 장소라고 생각하고 아직 충분히 사용되지 않는다고 말할 때 놀라지 않을 것입니다. 산업.

"공식적인 방법"에는 여러 수준이 있으므로 엄격한 수학적 기준으로 휴식을 취하는 사람들 (예를 들어 6 시그마 스타일 프로세스에 이어)을 의미한다고 가정 할 것입니다. 일부 유형의 공식적인 방법은 큰 성공을 거두었습니다. 유형 시스템은 하나의 예입니다. 데이터 흐름 분석을 기반으로 한 정적 분석 도구도 인기가 있으며, 모델 점검은 하드웨어 설계에서 거의 어디에나 적이며, Pi-Calculus 및 CCS와 같은 계산 모델은 동시성을 위해 실제 언어 설계의 실제 변화를 고무시키는 것으로 보입니다. 종료 분석은 최근에 많은 언론을 보유한 것입니다. Microsoft의 SDV 프로젝트 및 Byron Cook의 작업은 최근 공식적인 방법의 연구/실습 교차의 예입니다.

Hoare 추론은 지금까지 업계에서 큰 진출을하지 않았습니다. 이것은 내가 나열 할 수있는 것보다 더 많은 이유이지만, 글쓰기의 복잡성과 실제 프로그램에 대한 사양을 증명하는 것 (그들은 얻는 경향이 있습니다. 큰, 많은 실제 환경의 속성을 표현하지 못합니다). 이러한 유형의 추론의 다양한 하위 필드가 이제 이러한 문제에 큰 영향을 미치고 있습니다. 분리 논리는 하나입니다.

이것은 부분적으로 진행중인 (어려운) 연구의 본질입니다. 그러나 저는 이론가로서 우리의 기술이 왜 유용한 지에 대해 업계에 교육하지 못하고, 산업 요구와 관련이 유지되고, 소프트웨어 개발자가 접근하기 쉽게 만들었다고 고백해야합니다. 어느 정도는 우리의 문제가 아닙니다. 우리는 연구원, 종종 수학자이며, 실질적인 사용법은 우리의 마음에 가장 중요하지 않습니다. 또한 개발중인 기술은 종종 대규모 시스템에서 사용하기에는 너무 배아입니다. 우리는 소규모 프로그램에서 일하고 단순화 된 시스템에서 작업하고 수학을 작동시키고 계속 진행합니다. 그래도 이러한 변명을 많이 구매하지는 않습니다. 우리는 아이디어를 추진하고 업계와 작업간에 피드백 루프를 얻는 데 더 적극적이어야합니다 (연구로 돌아간 주된 이유 중 하나).

아마도 내 웹 로그를 부활 시키고이 물건에 대해 더 많은 게시물을 만드는 것이 좋은 생각 일 것입니다 ...

Answer 2

Tony Hoare 경은 약 10 년 전에 Microsoft Research에 합류했으며 그가 시작한 것 중 하나는 Windows NT 커널의 공식적인 검증이었습니다. 실제로 이것은 Windows Vista의 긴 지연의 이유 중 하나였습니다. Vista로 시작하여 커널의 많은 부분 ~이다 실제로 공식적으로 확인 된 WRT. 교착 상태 부재, 정보 유출 부재 등과 같은 특정 속성에

이것은 확실히 일반적이지는 않지만, 아마도 그 영향 측면에서 공식 프로그램 검증의 가장 중요한 적용 일 것입니다 (결국 거의 모든 사람은 어떤 식 으로든, 모양 또는 형태가 Windows를 실행하는 것)입니다.

Answer 3

항공 전자 산업이 Hoare 스타일 방법을 포함하여 소프트웨어를 검증하기 위해 다양한 기술을 사용한다는 것을 알고 있지만 미션 크리티컬 소프트웨어에 대해서는 많이 언급 할 수 없습니다.

Edsger Dijkstra와 같은 초기 옹호자들은 어디에서나 사용해야한다고 주장했기 때문에 공식적인 방법이 어려움을 겪었습니다. 형식주의 나 소프트웨어 지원은 그 일에 달려 있지 않았습니다. 더 합리적인 옹호자들은 이러한 방법이 어려운 문제에 사용되어야한다고 믿습니다. 그들은 산업에서 널리 사용되지는 않지만 채택이 증가하고 있습니다. 아마도 가장 큰 내적은 공식적인 방법을 사용하여 확인했을 것입니다. 안전 특성 소프트웨어. 내가 가장 좋아하는 예는 다음과 같습니다 회전 Model Checker와 George Necula의 증거가 나오는 코드.

Microsoft 's 특이 운영 시스템 프로젝트는 공식적인 방법을 사용하여 보통 하드웨어 지원이 필요한 안전 보장을 제공하는 것입니다. 이로 인해 성능이 빨라지고 더 강력한 보증이 이루어집니다. 예를 들어, 특이점에서 그들은 타사 장치 드라이버가 시스템에 허용되면 (이는 기본 검증 조건이 입증되었음을 의미 함) 전체 OS를 내려 놓을 수 없다는 것을 증명했습니다. 자체 장치.

공식적인 방법은 아직 산업에서 널리 사용되지는 않지만 20 년 전보다 더 널리 사용되며 20 년 후에도 여전히 더 널리 사용될 것입니다. 그래서 당신은 미래에 대비합니다 :-)

Answer 4

예, 그들은 사용되지만 모든 영역에서 널리 사용되는 것은 아닙니다. 주어진 작업에 대한 적합성에 따라 Hoare Logic보다 더 많은 방법이 있으며 일부는 더 많이 사용됩니다. 일반적인 문제는 sofware가 biiiiiiiig이며 모든 것이 올바른지 확인하는 것이 여전히 너무 어렵다는 것입니다.

예를 들어, 정리-프로버 (인간이 프로그램 정확성을 입증하는 데 도움이되는 소프트웨어) ACL2는 특정 부동산 포인트 처리 장치에 특정 유형의 버그가 없음을 증명하는 데 사용되었습니다. 큰 작업 이었으므로이 기술은 너무 흔하지 않습니다.

예를 들어 Microsoft는 드라이버 개발 키트에 모델 검사기 유형을 제공하며 공통 버그 세트에 대해 드라이버를 확인하는 데 사용될 수 있습니다. 모델 체커는 종종 하드웨어 회로를 확인하는 데 사용됩니다.

엄격한 테스트는 공식적인 검증으로 생각할 수 있습니다. 프로그램 경로를 테스트 해야하는 공식적인 사양이 있습니다.

Answer 5

"공식적인 방법은 업계에서 사용됩니까?"

예.

그만큼 assert 많은 프로그래밍 언어의 명령문은 프로그램을 검증하기위한 공식적인 방법과 관련이 있습니다.

"업계에서 공식적인 방법이 널리 사용됩니까?"

아니.

"이러한 방법은 미션 크리티컬 소프트웨어를 증명하는 데 사용됩니까?"

때때로. 더 자주, 그들은 소프트웨어가 안전하다는 것을 증명하는 데 사용됩니다. 보다 공식적으로, 그들은 소프트웨어에 대한 특정 보안 관련 주장을 증명하는 데 사용됩니다.

Answer 6

업계에는 공식적인 방법에 대한 두 가지 접근 방식이 있습니다.

한 가지 방법은 개발 프로세스를 완전히 변경하는 것입니다. 언급 된 z 표기법과 B 메소드는이 첫 번째 범주에 있습니다. B는 파리의 무인 지하철 14 번의 개발에 적용되었습니다 (기회가 생기면 앞 마차를 타십시오. 종종 당신 앞에서 레일을 볼 기회가 없습니다).

더욱 점진적으로 접근하는 또 다른 접근 방식은 기존 개발 및 검증 프로세스를 보존하고 새로운 방법으로 한 번에 검증 작업 중 하나만 바꾸는 것입니다. 이것은 매우 매력적이지만 종종 분석하기가 쉽지 않은 종종 종종 사용되지 않은 언어를 개발하기위한 정적 분석 도구를 개발하는 것을 의미합니다 (그들이 설계되지 않았기 때문에). (예를 들어)에 가면

http://dblp.uni-trier.de/db/indices/a-tree/d/delmas:david.html

(죄송합니다. 하나의 하이퍼 링크 만 새로운 사용자에게 허용했습니다 :()

C 프로그램 검증 (정적 분석기 Astrée, Astrée, Caveat, Factuat, Frama-C) 및 이진 코드 (ABSINT GMBH의 도구 포함)에 대한 공식적인 방법의 실제 적용 사례를 찾을 수 있습니다.

그건 그렇고, Hoare Logic을 언급 한 이후, 위의 도구 목록에서 경고 만 Hoare Logic을 기반으로합니다 (Frama-C에는 Hoare Logic Plug-in이 있습니다). 다른 사람들은보다 자동 접근 방식의 다른 기술인 추상 해석에 의존합니다.

Answer 7

저의 전문 분야는 정적 코드 분석에 공식적인 방법을 사용하여 소프트웨어가 런타임 오류가 없음을 보여줍니다. 이것은 "추상 해석"으로 알려진 공식적인 방법 기술을 사용하여 구현됩니다. 이 기술은 본질적으로 AS/W 프로그램의 특정 방학을 증명할 수 있습니다. EG는 A+B가 오버플로되지 않거나 x/(xy)가 0으로 나누지 않을 것임을 증명합니다. 이 기술을 사용하는 예제 정적 분석 도구는 폴리 스페이스입니다.

귀하의 질문과 관련하여 : "업계에서 공식적인 방법이 널리 사용됩니까?" 그리고 "이러한 방법은 미션 크리티컬 소프트웨어를 증명하는 데 사용됩니까?"

대답은 예입니다. 이 의견은 자동차의 전자 스로틀, 열차 제동 시스템, 제트 엔진 컨트롤러, 약물 전달 주입 펌프, 약물 전달 주입 펌프, 약물 전달 주입 펌프, 약물 전달 주입 펌프, 약물 전달 시스템과 같은 안전성 중요 시스템을 제어하기 위해 임베디드 소프트웨어 사용에 의존하는 산업에 의존하는 산업에 의존하는 내 경험과 지원을 기반으로합니다. 이러한 산업은 실제로 이러한 유형의 공식적인 방법 도구를 사용합니다.

이러한 산업 부문의 100%가 이러한 도구를 사용하고 있다고 생각하지는 않지만 사용이 증가하고 있습니다. 저의 의견은 항공 우주 및 자동차 산업이 의료 기기 산업으로 이어지고 있다는 것입니다.

Answer 8

폴리 스페이스 프로그램 검증을 기반으로 AA (끔찍한 비싸지 만 매우 우수한) 상용 제품입니다. '일부 버그를 찾을 수있는 향상된 단위 테스트에서'다음 3 년 동안 당신의 인생의 다음 3 년 동안이 10 개의 파일에 결함이 없음을 보여주는 데 소비 될 것 '으로 확장된다는 점에서 상당히 실용적입니다.

그것은 부정적인 검증 ( '이 프로그램은 스택을 손상시키지 않을 것입니다')에 더 기초합니다.

Answer 9

Jorg에 추가합니다 대답, 여기에 있습니다 회견 Tony Hoare와 함께. Jorg가 언급하는 도구는 Prefast와 Prefix라고 생각합니다. 보다 여기 자세한 내용은.

Answer 10

다른보다 절차 적 접근법 외에도 Hoare Logic은 계약에 의한 디자인, Eiffel의 Bertrand Meyer의 객체 지향 기술로 소개되었습니다.1992 년 Meyer의 기사를 참조하십시오, 4 페이지). 계약에 의한 설계는 공식적인 검증 방법과 동일하지 않지만 입증하다 제 생각에는 소프트웨어가 실행될 때까지 모든 것이 더 실용적으로 사용됩니다.