mCRL2에서 공유 공간 협력 모델링: Bach-to-mCRL2 변환 프레임워크

데이터 기반 협력 언어의 이론 및 구현에 상당한 연구가 집중되었지만, 분산 시스템의 신뢰성과 정확성을 보장하는 데 필수적인 모델 검사(model-checking) 기법을 사용한 자동 검증 측면은 여전히 충분히 탐구되지 않은 영역입니다. Anemone과 같은 기존 도구들은 Bach 프로그램의 도달 가능성 기반 검증에 견고한 토대를 제공합니다. 이러한 도구들이 상태 달성 가능성(state attainability) 측면에서 표현된 속성을 효과적으로 분석하지만, 생존성 속성(liveness properties)이나 공유 공간 내용물에 대한 불변 조건(invariants over shared space contents)과 같은 보다 표현력이 풍부한 시간적 명세(temporal specifications)로 지원을 확장하는 것은 여전히 열려 있는 기회입니다. 이러한 확장은 예를 들어, '요청은 항상 응답으로 매칭된다'거나 '메시지가 조용히 손실되지 않는다'와 같이 포괄적인 시스템 동작을 포착하는 데 중요합니다. 이러한 한계점을 해결하기 위해, 우리는 공유 공간을 명시적으로 표현하여 Bach에서 mCRL2로의 자동 변환을 제안하며, 이를 통해 단순 도달 가능성을 넘어선 복잡한 속성 검증에 mCRL2의 mu-calculus 모델 검사기를 사용할 수 있게 합니다. 이 변환을 보완하여, 우리는 mu-calculus를 사용하여 공유 공간 내용물에 대한 속성을 직접 표현함으로써 mCRL2에서 공유 공간을 분석하는 체계적인 방법을 도입하고, 이를 통해 검증을 위한 보다 명확한 프레임워크를 제공합니다. 이 접근 방식은 액션 기반 속성과 공유 공간 내용물에 대한 상태 기반 속성을 결합하는 새로운 검증 프로세스를 가능하게 하는데, 이는 현재 협력 언어 검증 접근법에서 크게 탐구되지 않은 영역이며 분석의 새로운 차원을 제공합니다.