0
최근에 나는 공식 검증 기술을 연구하기 시작했습니다. 문헌에서 모델 검사기 및 솔버은 어떻게 든 사용합니다. 그러나 모델 검사기와 해석기가 서로 어떻게 연결되어 있습니까?SMT/SAT 솔버 대 모델 검사기
p.s. 일부 논문이나 링크가 제안되면 감사하겠습니다.
A
답변
0
모델 검사를 수행하려면 도달 가능성 분석이 필요하며이를 위해 프로그램 전환이 종종 상징적으로 실행됩니다. 결과 만족 문제에 대한 해답은 솔버에 의해 생성됩니다.
에드워드 A. 리와 Sanjit A. Seshia, 임베디드 시스템 소개하는 사이버 : 아주 기본적이고 아주 좋은 소개는이 무료 교과서 (: 분석 및 검증 파트 III)에서 발견된다 물리적 시스템 접근법, Second Edition, MIT Press, ISBN 978-0-262-53381-2, 2017
0
모델 검사에서는 모델과 사양 (또는 속성)이 있고 모델이 사양.
SAT 해결에 수식이 있으며 만족스러운 할당을 찾으려고합니다.
이제 모델 검사에서 하나의 수식을 제공하기 위해 모델과 속성의 부정을 결합 할 수 있습니다. 솔버를 사용하여이 공식을 푸십시오. 그것이 당신에게 해결책을 준다면, 재산이 때때로 위반된다는 것을 의미 할 것입니다 (당신이 부정 된 재산을 연결했기 때문에). unsat을 얻으면 모델이 속성/사양을 충족한다는 것을 의미합니다.