스크린샷
한줄평
“분산·동시성 시스템의 설계 오류를 미리 잡으려는 사람을 위한 전문 검증 도구입니다.”
이런 분께 분산 시스템이나 동시성 알고리즘을 설계 단계에서 검증하려는 개발자
좋은 점
- 모델 검사로 설계 단계 오류를 자동 검출
- PlusCal·TLA+·증명 도구를 한 환경에서 사용
- 윈도우 등 주요 OS 공식 빌드 제공
아쉬운 점
- 형식 명세의 학습 곡선이 가파름
- 일반 애플리케이션 개발용 도구가 아님
TLA+ 툴박스 소개
TLA+ 는 시스템의 동작을 수학적으로 기술하고 검증하는 형식 명세 언어이며, 툴박스는 그 작성과 검증을 돕는 통합 개발 환경입니다. 레슬리 램포트가 설계한 언어로, 분산 시스템이나 동시성 알고리즘의 설계 오류를 코드 작성 전에 찾는 데 쓰입니다.
모델 검사기 TLC 를 이용해 명세가 만족해야 할 불변식과 속성을 자동으로 검증하고, PlusCal 알고리즘 언어 편집과 증명 도구 연동을 지원합니다. Java 기반으로 윈도우·macOS·리눅스용 빌드가 공식 제공됩니다.
