시간에 따른 성질 표현
현재 값만으로 설명하기 어려운 시스템 성질은 시간 흐름을 고려한 논리로 표현할 수 있다. Spot은 LTL 공식을 조작하고 오토마타로 변환하는 기능을 제공한다. 무한히 이어지는 실행을 받아들이는 조건도 분석의 일부다.
공식과 오토마타 연산
공식 단순화, 함의와 동치 검사, 오토마타의 곱과 공집합 검사 등 여러 알고리즘을 제공한다. 상태 기반과 전이 기반의 수용 조건을 다루는 방식도 구분된다. 변환된 그래프의 크기만으로 분석 결과의 의미를 판단하지 않는다.
변환 도구를 비교하기
ltlcross는 논리식을 오토마타로 바꾸는 도구들을 검사하고 비교하는 데 쓰이며 autcross는 오토마타 변환 도구를 다룬다. 상호 비교는 구현 차이를 발견하는 데 유용하지만 원래 명세가 시스템 요구를 제대로 표현했는지도 별도로 검토한다.
관련 문서
Owl 오토마타 도구 / Spin 모델 검사기 / NuSMV / NuXmv