Project/Model Checking

[RAFT] RAFT consensus algorithm specification

중간고사가 끝난 이후부터는 RAFT 알고리즘을 maude를 사용해 formal modeling을 진행할 것입니다. 그에 앞서 어떠한 specification을 모델링할지 결정해야 합니다. 따라서, 이 글에서는 RAFT consensus algorithm에 대해 간단히 소개하고 modeling하고자 하는 specification을 작성하고자 합니다. RAFT consensus algorithm RAFT consensus algorithm은 모든 node가 동일한 상태를 유지하며, tolerance를 보장하기 위해 고안된 알고리즘이다. 때문에 일부 node에 문제가 생겨도 전체 system이 잘 동작해야만 한다. 구성 모든 node는 아래 3가지 상태 중 한 가지를 가진다. cluster란 여러 subsys..

[Maude] Token Ring 검증

이 글에서는 Designing Reliables Distributes Systems, 225p에 있는 Token Ring을 maude를 사용해 formal modeling하고 원하는 검증을 진행합니다. 원 프로젝트는 RAFT consensus algorithm을 모델링하는 것이지만, 그 전에 손풀기 느낌으로 좀 더 쉬운 token ring을 모델링합니다. Token Ring In the “token ring” mutual exclusion algorithm, the nodes logically form a “ring” structure, as shown in Figure 13.1 where a node only knows the next node in this ring. The algorithm work..

[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 o..

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

지도교수님과 여러 가지 이야기를 나눴고, [특정 모델 체킹 언어를 사용해, 특정 시스템의 모델 체킹을 해 보기]를 주제로 과제연구를 진행하기로 했다. 대충 flow는 아래와 같다. 특정한 model checking 언어를 공부한다. 어떤 system을 체킹할 지 확인하기 distributed key-value store (cloud DB) RAFT consensus algorithm 위 2개를 추천받았는데, 모델링하기 위해서는 해당 system의 동작 방식을 알아야 한다. 일단 백엔드로 갈 거니까 분산 DB를 공부하는 게 좋아보인다. safety, fairness 등 어떤 property를 모델링할지 결정하기 Model Checking 언어 공부 model checking tool은 몇 가지가 있는데, ..

[Model Checking] Linear Time Properties

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. model checking의 주된 알고리즘은 transition system과 requirement를 model checker에 넣어, 해당 transition system이 requirement를 만족하는지 여부를 확인하는 방법이다. 그래서 지금까지 transition system을 모델링하는 방법을 살펴봤었고, 지금부터는 requirement를 모델링하는 방법을 살펴볼 것이다. 이 포스트에서는 크게 4가지를 살핀다. state-based and linear t..

[Model Checking] Modeling Concurrent System

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 지난 글에서는 Transition System과 Program Graph, 그리고 Program Graph를 Transition System으로 변환하는 방법을 살펴 봤다. 여기서 살폈었던 것들은 닫힌 계로써, 단 하나의 프로그램만 모델링하는 방법이었다. 이제 총 n개의 parallel system P$_1$, P$_2$, ... P$_n$ 이 있을 때를 모델링하고자 한다. 이 때 각 thread의 행동은 아래 3가지 중 하나이다. no communication ..

[Model Checking] Transition System과 Program Graph

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 이 글에서는 model checking에서 사용하는 transition system이 대체 뭔지, 그리고 우리가 사용하는 일반적인 프로그램을 transition system으로 바꾸는 방법을 살펴본다. Transition System transition system은 directed graph로 나타낸다. 이 때 graph의 node는 state를, edge는 transition을 의미한다. Definition. Transition System transition..