[Model Checking] 과제연구 주제 정리

 지도교수님과 여러 가지 이야기를 나눴고, [특정 모델 체킹 언어를 사용해, 특정 시스템의 모델 체킹을 해 보기]를 주제로 과제연구를 진행하기로 했다. 대충 flow는 아래와 같다.

 

1. 특정한 model checking 언어를 공부한다. 
2. 어떤 system을 체킹할 지 확인하기
   • distributed key-value store (cloud DB)
   • RAFT consensus algorithm
   • 위 2개를 추천받았는데, 모델링하기 위해서는 해당 system의 동작 방식을 알아야 한다. 일단 백엔드로 갈 거니까 분산 DB를 공부하는 게 좋아보인다.
3. safety, fairness 등 어떤 property를 모델링할지 결정하기

 

Model Checking 언어 공부

 model checking tool은 몇 가지가 있는데, SV 랩에서 현재 사용하고 있는 maude를 공부하기로 했다.

 Maude의 사용 방법은 Designing Reliable Distributed Systems를 추천받았고, 해당 글을 읽고 정리할 예정이다.

• 2장, 3장, 8장, 9장을 일단 보면 된다.
• 4장, 5장, 6장, 7장은 skip할 예정이다.
• 이후 concurrent를 다루는 10장, communication을 다루는 11장, transport protocol(통신)을 다루는 12장, distributed algorithm을 다루는 13장 중 원하는 system에 해당하는 것을 보면 된다.

 

 

 

어떤 system을 체킹할 지 결정하기

 구글에 `model checking distributed key value store`나 `model checking consensus algorithm`

 

 

 

어떤 property를 모델링할지 결정하기

 이건 system을 결정하면 따라오는 것이다.

 

 

 

참고

https://www.youtube.com/watch?v=nH4qjmP2KEE