Uppaal

시간을 포함한 상태

제어 구조에 실수 값의 시계를 더해 지연과 마감 같은 조건을 표현한다. 프로세스는 채널이나 공유 변수로 상호작용하며 제한된 정수와 배열 등 자료도 사용할 수 있다. 시간 단위와 환경의 입력 시점을 어떻게 모델링했는지가 중요하다. 실제 장치의 지연을 지나치게 단순화하면 검증 범위가 달라진다.

시뮬레이션과 모델 검사

시뮬레이터는 가능한 실행을 살펴보며 설계 오류를 찾는 데 쓰인다. 모델 검사기는 기호 상태 공간을 분석해 도달 가능성과 불변식 등을 확인한다. 몇 번의 시뮬레이션에서 문제가 없었다는 결과를 전체 상태 공간의 검증과 혼동하지 않는다. 진단 경로를 시뮬레이터에서 살펴보면 성질이 깨지는 과정을 이해하는 데 도움이 된다.

확장 기능과 사용 조건

통계적 모델 검사는 여러 실행을 관찰해 확률을 추정하는 방식이며 전통적인 모델 검사와 결과 의미가 다르다. 필요한 기능과 모델의 가정을 맞춰 선택한다. 학계의 비상업적 용도와 상업적 사용의 라이선스 조건도 구분해 확인한다. 확인한 시간 성질이 실제 시스템에 적용되려면 구현과 시계 및 외부 환경이 모델의 가정을 만족해야 한다.

관련 문서

Spin 모델 검사기 / NuXmv / TLAplus / Alloy 모델링