[Model Checking] Designing Reliable Distributed Systems

TODO

Ch. 2 : 자연수, 정수, list, binary tree, multiset 등 data type 정의

Ch. 3 : equational specification이 만족하는지 확인

Ch. 8 : rewrite logic을 사용해서 concurrent behavior 작성 방법을 설명

Ch. 9 : rewriting logic을 사용해서 system의 동작 하나를 분석하는 방법

 

FREE

Ch. 10 : concurrent

Ch. 11 : communication

Ch. 12 : TCP와 같은 transport protocol 모델링

Ch. 13 : distributed DB 모델링

 

 

 

Ch. 2 Data Types

Module

fmod MODULE_NAME is
    MODULE_BODY
endfm

 

op : 연산자 정의

• protecting은 다른 module 가져오는 것
• sort는 새로운 data type 정의

ctor : 생성자

var : 변수 선언

eq : 등식

 

1. data type import (sort)
2. op 정의하기 : 생성자와 해당 연산
3. var 정의하기 : 변수 정의하기
4. eq 정의하기 : 어떤 연산의 결과가 어떤 것인지 정의하기

 

 

 

Ch. 3 Equational Specification

 equational specificaion은 specification이 실행될 수 있는 방법을 설명한다.

 

 

 

Ch. 8 Modeling Distributed System in Rewriting Logic

 state가 바뀌는, dynamic system을 modeling하고 analysis하는 방법을 살핀다.

 한 예시로, 변화는 잘 안바뀐다!

 

 distributed system은 shared variable에 읽고 쓰거나, 서로 messaage를 주고받는 등 여러 개의 component로 이루어져 있다.

 

 distributed system은 대부분 non-deterministic하다! 

 

Interleaving

 interleaving system은 한 번에 하나의 component만 실행할 수 있는 system에 적합하다.

 

Rewriting Logic

 state t에서 t'로 0번 이상의 rewriting logic을 사용해 t'로 변경할 수 있다. 이것들은 nondeterministic하게 이뤄진다!

 

crl : 조건이 있는 rewriting logic

rl : 조건 없는 rewriting logic

 

Concurrency

 rl로 적으면 된다.

 

 

 

Ch. 9 Executing Rewriting Logic Specifications in Maude

 equational specification은 더 이상 적용할 수 없을 때까지 해당 specification을 실행한다.

 반면 rewriting logic은 dynamic system의 모든 가능한 behavior를 정의하며, 종료되지 않을 수 있다. 

 

 rewriting logic과 equational이 같은 변수에 의해 적용될 경우, equational을 먼저 rewriting logiㅊ 형태로 바꾼다. 이를 위해서는 rewriting logic의 좌항에는 생성자가 와야 한다.

 

set trace on .

 으로 규칙 적용과 rewriting 과정을 기록한다.

 

rew, frew

 rew나 frew를 사용해 rewriting을 할 수 있다. rew는 leftmost에만 적용, frew는 가능한 것들에 적용.

 

search

search t arrow pattern .
search t arraw pattern such that cond .

 search 명령어를 사용해 모델 검증을 할 수 있다. 그 결과로 특정 속성을 만족하는지, 다음 state를 검증할 때 쓸 수 있다.

• =>1 : t에서 한 step으로 도달할 수 있는 state
• =>* : t에서 0개 이상의 step으로 도달할 수 있는 state
• =>+ : t에서 1개 이상의 step으로 도달할 수 있는 state
• =>! : 더 이상 rewrite될 수 없는 state

 

show path

 특정 state의 path를 출력한다. 만약 =>!가 무한루프라면 상한을 걸어서 둘 수 있다.

 

 

 

Ch. 10 Concurrent Objects in Maude

 distributed system의 각 component를 object로 모델링하고, 각  component는 message를 주고받아서 communicate할 수 있다. 여기서는 rewriting logic을 사용해 concurrent logic을 모델링하는 방법을 살펴본다.

 

 

 

Ch. 11 Modeling Comunications in Maude

 ch. 10에서는 concurrent system이 concurrent object들의 multiset으로 표현하는 방법을 살펴봤었다. 이를 위해서는 model을 abstraction해야 한다.

 communication은 sync일 수도 이쏙, async일 수도 있다.

 rewriting은 communication primitive에 대한 뭔가를 제공하지 않기 때문에 통신 그 자체를 rewriting logic을 사용해 모델링해야만 한다.

 

 일단 비동기식을 쓸 때는, 메시지를 보내고, 받은 사람이 해당 메시지를 받지 않고 자신의 action을 취한 이후 받은 메시지를 처리하는 경우에, 문제가 발생하기 때문에 이 경우를 처리할 수 있는 로직을 작성해야 한다.

 

 

 

Ch. 13 Distributed Algorithm

 ch. 12는 생략했다. TCP를 굳이 쓸 필요는 없을 것 같아서.

 2-phase commit, mutual exclusion, leader election, concencus algorithm을 살핀다. 

 

 

 

 

 이제 직접 해 보자!