모델 확인 Paxos

Question

나는 합의 알고리즘 (Paxos 기반)을 구현했습니다. 몇 가지 임의의 테스트 케이스를 추가했으며 괜찮습니다. 하지만 모델 검사를 통해 테스트하고 싶습니까? 올바른 기사를 찾을 수 없습니다. Paxos에서 모델 확인에 대한

감사

Answer 1

당신은 시스템의 추상적 인 설명을 확인하기 위해 Spin Model checker를 사용할 수있는 작업을 수행하는 방법을 공유하시기 바랍니다.

Java 기반 구현의 경우 Java Path Finder을 사용할 수 있습니다.

mace도 있습니다. 여기서 Paxos와 같은 분산 시스템을 구현하고 테스트 할 수 있으며 C 코드를 포함하도록 지원합니다.

감사합니다, 기독교