DissProve: Affine Communication을 이용한 분산 프로토콜의 자동 검증

우리는 분산 프로토콜 (distributed protocols)의 안전성 속성 (safety properties)을 자동으로 증명하는 문제를 고려합니다. 분산 프로토콜은 비동기적 (asynchronous)이고 매개변수적 (parametric)인 특성 때문에 자동 검증 (automated verification) 측면에서 특히 까다로웠습니다. 동기식 시스템 (synchronous systems)과 비교했을 때, 비동기 통신 (asynchronous communication)은 메시지 핸들러 (message handlers)의 가능한 실행 이력 (execution histories)의 조합 폭발 (combinatorial explosion)을 초래합니다. 또한 분산 프로토콜은 일반적으로 액터 (actor)의 수에 대해 매개변수적으로 정의되기 때문에, 이러한 정의는 무한한 길이의 무한한 실행 이력을 생성합니다. 이러한 분산 프로토콜에 대한 기존 검증 기술은 일반적으로 전체 액터 시스템에 대한 전역 불변량 (global invariants)을 요구하며, 이는 단순한 프로토콜에 대해서도 복잡합니다. 본 논문에서는 액터 시스템의 에러 상태 (error states)로부터 역방향으로 도달 불가능성 (unreachability)을 증명하는 것에 기반한 자동 검증 기술을 제시합니다. 하나의 핵심적인 통찰은 매개변수성 (parametricity)으로 인한 무한성이 extit{어파인 (affine)} 프로토콜과 비-어파인 (non-affine) 프로토콜로 더 분류될 수 있다는 점이며, 어파인 프로토콜은 유한한 수의 통신 라운드 (communication rounds) 내에서 무한한 길이의 실행 이력을 가집니다. 우리는 목표 지향적인 새로운 구체화 (materialization), 인과 관계 (causality), 그리고 요약 (summarization) 개념을 사용하여 무한한 수의 액터를 가진 어파인 프로토콜의 안전성 속성을 자동화된 방식으로 검증하는 방법을 보여줍니다. 우리의 프로토타입 검증 도구인 DissProve를 사용하여, 우리는 어파인 통신을 가진 비동기 매개변수 시스템 (asynchronous parametrized systems)의 자동 안전성 검증이 가능하다는 증거를 제공합니다.