컴퓨터를 이용한 검증 도구를 사용해야합니까?

Question

일부 로봇 컨트롤러가 결함 상태에 도달하지 못했다는 것을 증명하는데 관심이 있습니다. 이는 술어 집합으로 정의 할 것입니다. 나는 그것을 달성하기위한 오픈 소스 소프트웨어 도구가 있다는 것을 알고있다. 예를 들어, BLAST (Berkeley Lazy Abstraction Software Verification Tool)에 대해 들어 봤지만, 특정 애플리케이션을 사용하기 쉽고 타겟이 명확한 다른 애플리케이션에 대해 알고 있습니까?

프로젝트 중 하나에서 BLAST 또는 다른 도구를 사용한 적이 있습니까? 그런 도구를 배포하는 데 필요한 노력보다 이점이 더 중요하다고 생각하십니까?

Answer 1

Frama-C이 유용 할 수 있습니다.

Frama-C 개발자가 아닌 사람들의 평가는 these two articles을 참조하십시오. 안전성이 중요한 코드 (예 : DO-178B 레벨 A)를 개발 한 일부 엔지니어는 가장 약한 선행 조건 기술 worth the investment을 기반으로하는 공식적인 주석과 분석을 발견했지만 전통적 테스트는 매우 비쌉니다. 이 마지막 링크는 Frama-C가 정시에 교체 할 예정인 폐쇄 소스 분석기 인 Caveat에 관한 것입니다.

Frama-C의 Aoraï 플러그인에 감사드립니다.

이 모든 것이 귀하의 경우에 잘 소요되었는지 여부는 아마도 이러한 기술에 대한 학습이 기쁨이나 자질구레 한 것인지 고려하는 것이 더 중요 할 것입니다.