한 번에 증명하지 않기
구현의 복잡한 동작을 단순한 프로그램으로 바꾸는 단계를 여러 층으로 구성한다. 각 변환이 보존해야 할 관계를 나누어 확인하면 큰 증명을 작은 문제로 관리할 수 있다. 낮은 수준 구현과 높은 수준 명세를 같은 구조화된 프로그램 언어로 표현해 연결한다.
동시성 명세의 구성
원자적 동작과 실행 양보 지점의 불변식 및 접근 권한 같은 개념을 이용해 스레드 사이의 관계를 기술한다. 단순히 가능한 실행을 많이 돌려보는 방식과 달리 명시한 구조와 논리 조건을 확인한다. 어떤 상호작용을 모델에 넣었는지와 무엇을 추상화했는지가 검증 범위를 결정한다.
구현과 증명의 연결
Civl은 Boogie 도구에 포함되어 있으며 생성된 일반 Boogie 모델을 확인할 수도 있다. 계층의 변환과 가정을 바꾸면 기존 증명이 유지되는지 다시 검사해야 한다. 모델이 성공했다고 운영 환경의 모든 프로세스나 외부 서비스를 자동으로 보장하지는 않는다. 대상 구현과 모델의 대응 및 남은 가정을 함께 유지한다.
관련 문서
Boogie / TLAplus / Alloy 모델링 / Loom 동시성 테스트