기타 자료

학습 자료

Specifying Systems: TLA+를 포괄적으로 소개하고 정형적인 기초를 다져 주는 책이지만, 모델 체킹(model checking)은 거의 다루지 않는다. 2004년 무렵 이후에 나온 기능, 예컨대 PlusCal이나 재귀 연산자(recursive operator) 같은 것은 다루지 않는다.
TLA+ Video Course: TLA+ 창시자가 직접 만든 동영상 강좌다.

Introduction to Formal Pragmatic Modeling: 프로덕션 수준의 대형 스펙(specification) 세 개를 깊이 파고드는 환상적인 자료다. TLA+를 어느 정도 안다고 가정한다.

TLA+ Language Reference Manual: Apalache 개발자들이 만든 엄밀한 레퍼런스다. 아직 작업 중이다.
TLA+ Version 2: 재귀 연산자와 람다 식(lambda expression)을 다룬다.
Current Versions of the TLA+ Tools: TLC를 명령줄에서 실행할 때 쓰는 플래그 정보와 함께, (PlusCal을 제외한) 다른 도구들에 대한 정보도 담겨 있다. TLC 모듈의 연산자에 대한 정보도 있다.
Pluscal Manual: PlusCal의 정형적 정의, 플래그, 명령줄 옵션을 다룬다. 예컨대 스펙에 필요한 레이블(label)을 자동으로 생성해 주는 70쪽의 “label” 옵션을 보라.
Summary of TLA+: TLA+ 치트 시트다. 액션 합성(action composition)처럼 어떤 도구로도 검사할 수 없는 TLA+ 구문도 일부 들어 있다. ASCII 기호 대신 조판된 기호를 쓴다(그래서 ∈ 기호를 쓰고 \in은 쓰지 않는다).

How Amazon Web Services uses Formal Methods: 대기업들이 처음으로 TLA+ 도입에 관심을 갖게 만든 논문이다. 나도 이 논문을 보고 TLA+를 알게 됐다.
TLA+ Example Repository: 추상적인 알고리즘과 프로토콜을 모아 둔 저장소다.
TLA+ in Practice and Theory: TLA+의 바탕이 되는 수학 이론을 자세히 분석한 글이다.
Let’s Prove Leftpad: 여러 정형 기법(formal methods)으로 leftpad를 증명한 사례 모음이다. TLA+와 전적으로 관련된 것은 아니지만 <뻔뻔한 자기 홍보 삽입>

Designing Distributed Systems with TLA+: TLA+를 써 보라고 권할 때 내가 늘 하는 강연이다.
Weeks of Debugging can save you Hours of TLA+: Markus(툴박스 핵심 개발자)가 TLA+ 사용을 권하는 강연이다.

TLA+ Community Modules: 최소한만 갖춘 TLA+ 표준 라이브러리에 보탤 만한 유용한 모듈(module)을 모아 둔 것이다.

TLA+용 대안 모델 체커(model checker)다. 모든 상태(state)를 열거하는 대신 기호 모델 체킹(symbolic model checking)을 사용한다.

(밝혀 두자면, 나는 현재 Informal Systems의 컨설팅 일을 일부 맡고 있다.)

TLAPS: TLA+를 정리 증명기(theorem prover)로 쓰고 싶을 때를 위한 TLA+ 증명 시스템이다.

conf.tlapl.us: 매년 여는 우리 TLA+ 콘퍼런스 정보를 올리는 공식 사이트다. 보통 Strange Loop와 공동 개최한다.
TLA+ Google Group: 핵심 개발자들이 모두 여기 모여서 사람들의 질문에 답해 준다.
r/tlaplus: TLA+ 서브레딧이다.