TLA+ - 프로그램 및 동시/분산 시스템을 모델링하기 위한 고급 언어

4 days ago 5

TLA+는 코드 수준이 아닌 상위 수준에서 소프트웨어를 모델링하고, 회로 수준이 아닌 상위 수준에서 하드웨어를 모델링하기 위한 언어임
모델을 작성하고 이를 검사할 수 있는 통합 개발 환경(IDE)을 제공
엔지니어들이 가장 많이 사용하는 도구는 TLC 모델 검사기이며, 증명 검사기도 제공
TLA+는 수학에 기반하며 어떤 프로그래밍 언어와도 유사하지 않음
대부분의 엔지니어는 TLA+보다 PlusCal을 통해 시작하는 것이 더 쉬움
TLA+ 모델은 일반적으로 "스펙(Specification)"으로 불림. 아래 소개에서는 모델이라고 부름

PlusCal

TLA+는 코드 수준 이상의 시스템 모델링에 사용됨
예를 들어, 유클리드 알고리듬은 코드가 아닌 절차로서 최대공약수(GCD)를 계산하는 방식으로 설명 가능함
- 변수 x를 M, y를 N으로 설정함
- x와 y 중 작은 값을 큰 값에서 반복적으로 뺌
- x와 y가 같아질 때까지 반복하고, 그 값이 GCD임
이러한 설명은 변수 타입이나 예외 처리 등의 세부사항을 생략하며, 본질적인 알고리듬 개념만 표현함
코딩에만 집중할 경우 좋은 알고리듬을 찾기 어려움 → 추상적 사고가 필요함
대부분의 프로그래머는 고수준 모델 없이 코딩을 시작하며, 이로 인해 설계 오류가 발생함
TLA+는 코드의 동작과 방법을 명확하게 기술할 수 있는 고수준 모델 언어임
복잡한 시스템일수록 단순화가 중요하며, 이는 코드 기술이 아니라 고차원 사고를 통해 달성됨
한 산업 프로젝트에서, TLA+ 모델링으로 실시간 운영체제의 코드 크기를 10분의 1로 줄인 사례가 있음
모델링은 설계 오류를 사전에 찾는 데 효과적이며, 테스트나 코드 수정보다 신뢰성 높음

TLA+는 다음 두 요소로 행동 집합을 정의함:
- 초기 조건: 가능한 시작 상태 지정
- 다음 상태 관계: 가능한 단계(연속된 상태 쌍) 지정
이 두 조건을 만족하는 행동들의 집합이 모델임
이러한 모델은 상태 기계(state machine)라 불림
유한 상태 기계(finite-state machine)는 상태 수가 유한한 상태 기계임
튜링 기계는 상태 기계의 예로, 결정적 튜링 기계는 상태마다 다음 상태가 최대 하나임
프로그래밍 언어의 의미를 정확히 설명하는 실용적인 방법은 상태 기계로 변환하는 운영 의미론임
다음 상태 동작은 발생 가능한 단계만 지정하며, 반드시 발생해야 한다는 것을 의미하지 않음
단계의 필수 발생을 명시하려면 공정성 조건(fairness property)을 추가해야 함
공정성 없이도 오류(commission)를 찾는 데 충분하지만, 누락 오류(omission)는 검출되지 않음
대부분의 경우 오류는 commission이 많으며, 초보자는 초기 조건과 다음 상태 관계 작성부터 시작해야 함