Why is this thesis important?

2020 년 초에 Paul은 Tezos 코드베이스에서 구성 요소의 올바른 구현을 확인하는 과정에서 발생한 문제인 메시지 전달 프로토콜의 올바른 구현을 지정하고 검증하는 방법을 제기했습니다. 호기심에 그는 기존 형식주의에서 몇 가지 해결책을 연구했지만 불만족 스러웠습니다.

Paul이 강조한 문제는 배포 여부에 관계없이 현대 시스템에서 널리 퍼져 있습니다. 소프트웨어 시스템의 각 구성 요소가 로컬 사양을 충족해야하는 것으로는 충분하지 않습니다. 그들은 또한 일부 합의 된 프로토콜에 따라 올바르게 함께 대화해야합니다. 즉, 구성 요소가 상호 작용하는 방식과 이러한 상호 작용이 정확하다는 의미 (버그없는)를 지정하고 추론 할 언어가 필요합니다.

Paul의 논문은 메시지 전달 프로토콜의 실행을 엄격하고 모호하지 않게 설명하는 공식 언어를 소개합니다. 그 설명에서 구조별로 올바른 프로토콜의 각 당사자에 대한 참조 구현을 생성 할 수 있습니다. 구현이 해당 사양에서 공식적으로 구성되면 각 구성 요소가 수신 된 메시지에 올바르게 응답하고 프로토콜에 의해 예측 된 메시지. 멋진 점은이 참조 구현을 프로덕션에 배포 할 수 있고 다른 구현의 유효성을 검사하는 데 사용할 수도 있다는 것입니다. 더 빠르거나 더 나은 메모리 소비를 가진 최적화 된 것.