용어집

용어 안내

액션(Action): 상태가 어떻게 “진화하는지”를 기술하는 술어(predicate)다. 프라임 연산자가 들어간 불리언(boolean) 식(expression)이라면 무엇이든 액션이다(x' = x처럼). 액션은 다음 상태를 기술하면 참이고, 그렇지 않으면 거짓이다. 예를 들어 두 가지 일이 병렬로 일어나는 경우처럼, 여러 액션이 한꺼번에 참일 수도 있다.
행동(Behavior): 시스템 안에서 상태들이 이어진 시퀀스(sequence), 곧 “타임라인”이다.
활성화된(Enabled): 어떤 액션이 이번 스텝에 “일어날” 수 있다면, 즉 다음 스텝을 기술할 가능성이 있다면 그 액션은 “활성화되었다(enabled)”고 한다.
공정성(Fairness): 시스템이 언젠가는 “진전한다(make progress)”는 보장이다. 약한 공정성(weak fairness)은 주어진 액션이 영구히 활성화되어 있으면 그 액션이 언젠가는 일어난다고 말한다. 강한 공정성(strong fairness)은 그 액션이 영구히 비활성화되어 있지만 않으면 언젠가는 일어난다고 말한다.
정형 기법(Formal Methods): 엄밀하고 검증된 코드를 작성하는 분야다.
정형 명세 언어(Formal Specification Language): 만들고 있는 시스템을 기술해서, 그 안의 오류를 찾아낼 수 있게 해 주는 언어다.
함수(Function): 정의역(domain)이 고정된 수학적 함수다. 프로그래밍에서 말하는 함수는 연산자라고 부른다.
불변식(Invariant): 시스템의 모든 상태에서 참이어야 하는 것이다. 모든 불변식은 안전성 속성이다.
라이브니스(Liveness): 좋은 일이 반드시 일어난다고 보장하는 속성이다. 모든 라이브니스 속성은 시간 속성이다.
모델(Model): TLA+에서는 명세 + 주입한 매개변수와 요구하는 불변식의 집합을 말한다.
모델 체킹(Model checking): 명세가 그 속성들을 만족하는지 검증하는 가장 흔한 방법이다. 가능한 모든 행동을 생성하고, 그중 하나라도 속성을 깨뜨리는지 빠짐없이 테스트한다. TLA+의 모델 체커(model checker)는 TLC라고 부른다.
연산자(Operator): 프로그래밍의 함수에 해당하는 TLA+의 개념이다. 프라임 변수(primed variable)가 들어 있는 연산자는 액션이라고 부른다.
PlusCal: TLA+ 알고리즘을 작성하기 위한 DSL이다.
술어(Predicate): 불리언 식이다.
속성(Property): 시스템에 대해 참이기를 바라는 것이다. TLA+의 모든 속성은 안전성 속성과 라이브니스 속성으로 나눌 수 있다.
안전성(Safety): 나쁜 일이 일어나지 않는다는 속성이다. 안전성 속성의 대부분은 (전부는 아니지만) 불변식이다. 모든 불변식은 안전성 속성이다.
명세(Specification)
스펙(Spec): 만들고 있는 시스템을 엄밀하게 수학적으로 기술한 것이다.
상태 공간(State space): 한 모델에서 가능한 모든 행동으로 도달할 수 있는, 가능한 모든 상태의 집합이다.
스텝(Step): 시계가 한 번 “째깍”하는 것으로, 스펙의 상태 일부를 바꾼다. 행동은 스텝의 시퀀스로 이루어진다.
스터터 스텝(Stutter Step): 아무것도 바꾸지 않는 상태 전이다. 모든 TLA+ 스펙은 “스터터 불변(stutter-invariant)”이다. 즉 임의의 두 “진짜” 액션 사이에서 언제든 스터터링할 수 있다. 공정성 제약으로 따로 막지 않는 한, 행동은 영원히 스터터링할 수 있다.
시간 속성(Temporal Property): 둘 이상의 상태에 걸치는 속성이다. 예를 들어 “카운터는 절대 줄어들어서는 안 된다” 또는
정리 증명기(Theorem Prover): 명세를 정형 검증하는 또 다른 방법으로, 명세가 원하는 속성을 갖추었음을 수학적으로 증명한다. 모델 체커보다 훨씬 어려워서 이 가이드에서는 다루지 않는다. TLA+의 정리 증명기는 TLAPS라고 부른다.
TLA+: 동시적 시스템을 모델링하는 데 쓰이는 “액션의 시간 논리(Temporal Logic of Actions)”다. 정형 명세 언어의 하나다. TLA+로 직접 작성할 수도 있고, PlusCal DSL을 쓸 수도 있다.
TLA+ 툴박스(TLA+ Toolbox): 공식 TLA+ IDE다.
TLC: TLA+ 모델 체커의 이름이다. 이 사이트에서는 “TLC”와 “모델 체커”를 같은 뜻으로 섞어 쓴다.

상태 공간 폭발(State space explosion) 한정자(Quantifier) 모듈(Module) 기계(Machine) 세계(World)