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

> Clean Markdown view of GeekNews topic #19971. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=19971](https://news.hada.io/topic?id=19971)
- GeekNews Markdown: [https://news.hada.io/topic/19971.md](https://news.hada.io/topic/19971.md)
- Type: news
- Author: [xguru](https://news.hada.io/@xguru)
- Published: 2025-03-26T12:43:52+09:00
- Updated: 2025-03-26T12:43:52+09:00
- Original source: [lamport.azurewebsites.net](https://lamport.azurewebsites.net/tla/tla.html)
- Points: 21
- Comments: 3

## Summary

TLA+는 소프트웨어와 하드웨어를 상위 수준에서 모델링하기 위한 수학 기반의 언어로, 코드 수준 이상의 시스템 모델링을 가능하게 하며, 특히 병렬 및 분산 시스템의 모델링에 유용합니다. PlusCal은 알고리즘을 테스트 가능한 코드로 작성할 수 있는 언어로, TLA+ 모델로 변환되어 검증할 수 있으며, 복잡한 모델 구조화에는 TLA+가 더 적합합니다. TLA+는 상태 기반 모델링 언어로 시스템의 실행을 상태들의 순서로 표현하며, 모델링을 통해 설계 오류를 사전에 발견하고 시스템의 신뢰성을 높일 수 있습니다.

## Topic Body

- TLA+는 코드 수준이 아닌 상위 수준에서 **소프트웨어를 모델링**하고, 회로 수준이 아닌 상위 수준에서 **하드웨어를 모델링**하기 위한 **언어**임  
- 모델을 작성하고 이를 검사할 수 있는 [통합 개발 환경(IDE)](https://github.com/tlaplus/tlaplus)을 제공  
- 엔지니어들이 가장 많이 사용하는 도구는 TLC 모델 검사기이며, 증명 검사기도 제공  
- TLA+는 수학에 기반하며 어떤 프로그래밍 언어와도 유사하지 않음  
- 대부분의 엔지니어는 TLA+보다 PlusCal을 통해 시작하는 것이 더 쉬움  
- TLA+ 모델은 일반적으로 "스펙(Specification)"으로 불림. 아래 소개에서는 `모델`이라고 부름  
  
### PlusCal  
- PlusCal은 알고리듬, 특히 **병렬 및 분산 알고리듬을 작성하기 위한 언어**  
- 의사코드 대신 테스트 가능한 정확한 코드로 알고리듬을 작성하는 데 사용됨  
- 간단한 프로그래밍 언어처럼 보이며, 병행성과 비결정성을 표현할 수 있는 구조를 제공함  
- 수학적 수식을 표현식으로 사용할 수 있어 매우 표현력이 높음  
- **PlusCal 알고리듬은 TLA+ 모델로 변환되며, TLA+ 도구로 검증 가능**  
- 프로그래밍 언어처럼 보이므로 배우기 쉬우나, **복잡한 모델 구조화에는 TLA+가 더 적합**  
  
### 모델이란 무엇인가  
- 컴퓨터와 네트워크는 연속적인 물리 법칙을 따르지만, 이들의 동작은 이산적 사건의 집합으로 모델링하는 것이 자연스러움  
- 실제 시스템을 완벽히 묘사하는 모델은 없으며, 모델은 특정 목적을 위한 시스템의 일부 측면을 묘사함  
- TLA+는 **상태 기반 모델링 언어**로, **시스템의 실행을 상태들의 순서로 표현**함  
- 사건은 연속된 두 상태 쌍으로 표현되며 이를 '단계(step)'라 부름  
- 시스템은 가능한 모든 실행을 설명하는 행동들의 집합으로 모델링됨  
  
### 코드 수준 이상의 모델링  
- TLA+는 코드 수준 이상의 시스템 모델링에 사용됨  
- 예를 들어, 유클리드 알고리듬은 코드가 아닌 절차로서 최대공약수(GCD)를 계산하는 방식으로 설명 가능함  
  - 변수 x를 M, y를 N으로 설정함  
  - x와 y 중 **작은 값을 큰 값에서 반복적으로 뺌**  
  - x와 y가 **같아질 때까지 반복**하고, 그 값이 GCD임  
- 이러한 설명은 변수 타입이나 예외 처리 등의 세부사항을 생략하며, 본질적인 알고리듬 개념만 표현함  
- 코딩에만 집중할 경우 좋은 알고리듬을 찾기 어려움 → 추상적 사고가 필요함  
- 대부분의 프로그래머는 고수준 모델 없이 코딩을 시작하며, 이로 인해 설계 오류가 발생함  
- TLA+는 **코드의 동작과 방법을 명확하게 기술**할 수 있는 고수준 모델 언어임  
- 복잡한 시스템일수록 단순화가 중요하며, 이는 코드 기술이 아니라 고차원 사고를 통해 달성됨  
- 한 산업 프로젝트에서, TLA+ 모델링으로 실시간 운영체제의 코드 크기를 10분의 1로 줄인 사례가 있음  
- **모델링은 설계 오류를 사전에 찾는 데 효과적**이며, 테스트나 코드 수정보다 신뢰성 높음  
  
### 병렬 시스템 모델링  
- 병렬 시스템은 동시에 작동하는 여러 컴포넌트(프로세스)로 구성됨  
- 분산 시스템은 공간적으로 분리된 프로세스들이 메시지를 통해 통신함  
- TLA+는 **전체 시스템 상태를 전역 상태로 모델링**함  
- 40년 이상의 경험에 따르면, **분산 시스템을 전역 상태 기반으로 모델링하는 것이 가장 일반적으로 유용함**  
  
### 상태 기계(State Machine)  
- TLA+는 다음 두 요소로 행동 집합을 정의함:  
  - 초기 조건: 가능한 시작 상태 지정  
  - 다음 상태 관계: 가능한 단계(연속된 상태 쌍) 지정  
- 이 두 조건을 만족하는 행동들의 집합이 모델임  
- 이러한 모델은 상태 기계(state machine)라 불림  
- 유한 상태 기계(finite-state machine)는 상태 수가 유한한 상태 기계임  
- 튜링 기계는 상태 기계의 예로, 결정적 튜링 기계는 상태마다 다음 상태가 최대 하나임  
- 프로그래밍 언어의 의미를 정확히 설명하는 실용적인 방법은 상태 기계로 변환하는 운영 의미론임  
- 다음 상태 동작은 발생 가능한 단계만 지정하며, 반드시 발생해야 한다는 것을 의미하지 않음  
- 단계의 필수 발생을 명시하려면 공정성 조건(fairness property)을 추가해야 함  
- 공정성 없이도 오류(commission)를 찾는 데 충분하지만, 누락 오류(omission)는 검출되지 않음  
- 대부분의 경우 오류는 commission이 많으며, 초보자는 초기 조건과 다음 상태 관계 작성부터 시작해야 함  
  
### 속성 검증  
- 시스템이 원하는 대로 동작하는지를 확인하기 위해 모델을 작성함  
- 모델이 모든 가능한 행동에 대해 특정 속성을 만족하는지 TLA+ 도구로 검증 가능함  
- 예: 99%의 초기 상태에서 동작이 정상 종료되더라도, 모든 행동이 정상 종료되어야 함을 검증함  
- 가장 일반적인 속성은 불변 속성(invariance property)으로, 모든 상태에서 항상 참이어야 함  
- 공정성 조건이 있는 모델은 생존 속성(liveness property)도 검증해야 함 → 예: 실행이 반드시 종료됨  
- 더 복잡한 속성은 상태 기계로 표현 가능하며, 다른 상태 기계가 이를 구현하는지를 검증 가능함  
- TLA+에서는 상태 기계와 속성의 형식적 구분 없이 수학식으로 동일하게 표현됨  
- 한 상태 기계가 다른 상태 기계를 구현한다는 것은 해당 수식이 논리적으로 포함됨을 의미함  
- 실제로는 대부분 불변성과 간단한 생존 속성만 검사하지만, 더 복잡한 개념을 이해하는 것도 코드 오류 방지에 도움됨  
  
### TLA+ 언어 자체  
- TLA+는 **수학 기반 언어**이며 프로그래밍 언어처럼 보이지 않음  
- 프로그래머는 수학 표현보다는 프로그래밍 언어에 익숙하기 때문에 처음에 어렵게 느낄 수 있음  
- 하지만 실제로는 수학이 프로그래밍 언어보다 더 표현력이 뛰어남  
- 예: GCD를 두 수를 나누는 최대의 양의 정수라고 정의할 수 있음 (계산 방법 생략 가능)  
- 수학적 정의는 **목적에 필요한 핵심만 남기고, 불필요한 구현 세부사항을 추상화**할 수 있음  
- 절차화는 추상화를 제공하지 않으며, 단지 다른 위치에 코드를 숨길 뿐임  
- PlusCal은 TLA+ 입문에 적합하며, 숙련자도 간단한 모델에는 PlusCal을 선호함  
- 하지만 수학적으로 사고하고 고수준 모델링을 하려면 TLA+ 자체를 익히는 것이 중요함

## Comments



### Comment 36377

- Author: gera1d
- Created: 2025-03-26T15:47:29+09:00
- Points: 1

https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/ aws에서 잘 쓰고 있죠.

### Comment 36368

- Author: xguru
- Created: 2025-03-26T12:44:13+09:00
- Points: 1

[코딩은 프로그래밍이 아니에요](https://news.hada.io/topic?id=19969)  
이 글에서 언급되길래 찾아봤습니다.

### Comment 36372

- Author: ryj0902
- Created: 2025-03-26T13:20:31+09:00
- Points: 1
- Parent comment: 36368
- Depth: 1

저도 이 글에서 처음 봐서 찾아보고 있었네요