2
기호 실행과 모델 검사 (예 : 모델 변환)의 차이점은 무엇입니까? 나는 그들의 차이점을 이해하지 못한다. 그들은 같은가요?!기호 실행 및 모델 검사
A
답변
2
모델 검사에서는 시스템을 유한 상태 시스템으로 인코딩하고 해당 FSM을 모델 검사기 및 사양에 제공해야합니다. 그런 다음 모델 검사기는 사양이 항상 해당 시스템에서 유지되는지 확인합니다.
기호 실행에서는 프로그램 만 제공하고 기호 실행 엔진은 가능한 모든 경로를 검사하여 테스트 입력 또는 어설 션 확인을 생성합니다.
간단한 차이점 : 동시성. 모델 검사는 입력으로 제공된 FSM에 지정되어 있기 때문에 다중 스레드 시스템을 처리 할 수 있지만 기호 실행은 두 개 이상의 스레드를 처리 할 수 없습니다.
2
모델 검사 : 프로그램이 사양을 충족하는지 공식적으로 확인하는 방법. 명세는 대개 일시적인 논리 공식으로 주어집니다 : "입력이 x이면 프로그램의 모든 실행 (전체적으로)에 대해 y - hold 여야합니다"(예 : Edward A Lee 참조).
기호 모델 검사 대 명시 상태 검사 : 프로그램은 유한 상태 시스템 (FSM) 일 수 있습니다. 여기서 명시적인 상태 검사만으로 충분합니다. 그러나 다행스럽게도 확장 된 FSM의 동시 발생 확률 론적 실시간 응용 프로그램에도 모델 검사기가 있습니다. 매우 큰 (무한) 상태의 시스템에서 상태 폭발을 방지하기 위해 기호 모델 검사가 사용됩니다. 기호 모델 검사에서 상태 및 입력 등은 기호 및 명제식 (또는 상태 집합, 집합 연산 등)으로 처리됩니다. 모델 검사를 수행하려면 도달 가능성 분석이 필요하며이를 위해 프로그램 전환이 상징적으로 실행됩니다. 이러한 체커는 인스트루먼트 된 네이티브 코드의 정상적인 실행을 사용할 수 없습니다.
기호 실행 : 기호 실행 중에 다른 인코딩 방법이 있습니다. 일부는 모델 검사에 매우 특화되어 있고 일부는 독립 실행 형 기호 실행 프레임 워크에서 모듈화되고 사용되며 기호 실행의 발명가가 정의했기 때문에 사용됩니다. 상징적 실행 프레임 워크는 종종 등을 테스트하기 위해 사용할 수도 확인하는 상징적 인 모델의 일부 요소 (탐사, 검색)를 사용
마지막으로 몇 가지 예:
JPF, 자바 패스 파인더 : 모델 검사기, 체크 명시 적 상태 입력 : 자바 바이트 코드
SPF, 상징적 파인더 : 상징적 실행, JPF
JCBMC의 확장자 경계 모델 검사기 JPF 연장, SPF
XRTs : 탐사 및 심볼 IC 실행, 입력 : CIL 바이트 코드
IntelliTest : 모델 기반 테스트가 XRTs 당신의 친절한 도움을
감사를 사용하여 매개 변수화 된 단위 테스트는 XRTs
사양 탐색기
를 사용합니다. Java Path Finder는 모델 검사 도구 또는 기호 실행 도구이거나 둘 다입니까? 모델 검사를 사용하지 않는 기호 실행 도구가 있습니까? – any