간단한 모델 검사기 도구

간단한 모델 검사기 도구가 있습니까? 미리 정의 된 일부 속성에 대한 코드를 분석 할 모델 검사기 도구를 구현할 계획입니다.간단한 모델 검사기 도구

출처

2008-10-20 Vinay

당신이 찾고있는 것을 조금 더 자세히 설명해야한다고 생각합니다. –

나는 당신이 질문을 수정해야 더 명확해질 것이라고 생각합니다. 이 질문은 12 가지 모델 검사 시나리오와 관련 될 수 있습니다. –

스타를 유지 관리하는 모델 검사기 도구입니다. 즉, 응용 프로그램이 종료되는지 여부를 알 수있는 도구를 구현할 계획입니다. (오직 정적 분석) – Vinay

중요한 도구 중 하나는 Promela 언어 인 SPIN입니다. LaTeX를 사용하는 경우 TLA+도 있습니다.

이러한 코드는 코드를 분석하지는 않지만 가정 및 주 변환에 대한 모델을 표현한 다음 유효하지 않은 상태를 분석합니다. 즉, 모델 구현이 아니라 모델의 문제를 감지합니다.

나는 Goanna의 데모를 보았지만 전혀 사용할 수 있는지 모르겠다. 이것은 실제로 소스 코드를 분석하는 이점이 있습니다.

질문에 대한 귀하의 질문과 의견을 다시 한 번 살펴보면, 먼저 문헌을 먼저 읽어야하는 것처럼 들립니다. 아마도 The Spin Model Checker 또는 Specifying Systems (Leslie Lamport's website에서 다운로드 가능) 일 수 있습니다. 정지 문제를 해결하지 않으려면 문제점을 다시 찾아야합니다.

출처

2008-10-21 10:34:49 janm

CBMC은 코드에서 실제로 작동한다는 것을 알고있는 간단한 도구입니다. 모델 검사는 일반적으로 많이 연구 된 분야이지만, 사람들이 이미 주석을 달았으므로이 폭은 제공되는 정보로 무언가를 제안하는 것을 어렵게 만듭니다. 수천 개의 SAT 해결사, HDL/상태 머신 검증을위한 공식 도구, 상용 상용 정적 분석기가 많이 있습니다.

어쨌든 CBMC는 좋은 도구이지만 내 말을 듣지는 못합니다. 이 작품의 주요 교수진 인 Ed Clarke가 올해 Turing Award를 수상했습니다.

출처

2008-10-20 16:17:03

상태를 유지 관리하는 모델 검사기 도구입니다. 즉, 응용 프로그램이 종료되는지 여부를 알 수있는 도구를 구현할 계획입니다. (정적 분석 만) – Vinay

정말요? 그건 조금 어려워 보입니다 (http://en.wikipedia.org/wiki/Halting_problem) ;-) –

@MattJ 어렵지만 불가능하지는 않습니다. CBMC가 귀사의 프로그램이 런타임 오류/예외가 없거나 올바르지 않다는 것을 입증하면 해지를 증명합니다. 중지 문제는 AFAIK 모든 프로그램에 대해 결정적이지는 않습니다. 여러 종류의 프로그램에서는 결정하기가 쉽습니다! +1 CBMC 언급에 대한, 그것은 훌륭한 도구입니다. –

간단한 모델 검사기 도구

답변

관련 문제