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을 얻으면 모델이 속성/사양을 충족한다는 것을 의미합니다.
관련 문제
- 1. 두 검사기 한 모델
- 2. 간단한 모델 검사기 도구
- 3. 레일 모델 유효성 검사기
- 4. 솔버
- 5. 모델 기반 양식 - 검사기 문제
- 6. Django 사용자 모델 유효성 검사기
- 7. 는 검사기 모델 기반 (반응성)
- 8. 개념 모델 대 논리적 모델 대 정규 모델
- 9. 지속성 모델 대 뷰 모델
- 10. 서비스 모델 대 Extender 모델?
- 11. dReal SMT 솔버 반경
- 12. 사용 솔버
- 13. MATLAB 솔버
- 14. 레일 : 모델 대 배열
- 15. 도우미 대 모델
- 16. 네이밍 모델 대 MonoBehaviours
- 17. 엔티티 대 모델
- 18. ViewBag는 모델 대, MVC.NET
- 19. Angular2 모델 기반 폼 유효성 검사기 패턴
- 20. 모델 날짜 범위 유효성 검사기 (mvc)
- 21. Julia challange - FitzHugh-Nagumo 모델 PDE Runge-Kutta 솔버
- 22. Erlang 동시성 모델 대 스칼라 대 Go
- 23. Z3 만족 모델을 출력하는 솔버?
- 24. 활성 모양 모델 대 활성 모양 모델
- 25. MVC에서 푸시 모델 대 풀 모델
- 26. 모델 대 모델 변환을위한 ATL과 QVT 선택
- 27. Django 모델 상속 대 추상 기본 모델
- 28. Rally API 2.0 모델 대 모델
- 29. 액터 모델 대 객체 지향 모델
- 30. 랜덤 솔루션 Yices 솔버