[연구의 필요성]

PROMELA는 분산/동시성 시스템을 기술하기 위한 대표적인 모델링 언어로, 암호 프로토콜/항공 소프트웨어/운영체제 등 다양한 시스템의 신뢰성 향상에 핵심적 역할을 해왔다. 그러나 PROMELA 언어의 의미구조는 SPIN 검증기의 구현체에 의존하여, 언어 차원의 정확한 의미 이해나 도구 독립적인 분석 확장이 어려웠다. 이에 따라 PROMELA 프로그램에 대해 SPIN 검증기가 제공하는 모델체킹 외의 분석 기법(예를 들어, 코드 수준의 연역적 검증 등)을 적용하는 데 근본적인 제약이 존재하였다.

[포스텍이 가진 고유의 기술]

본 연구는 PROMELA 언어의 실행가능한 의미구조의 수학적 정의 및 그의 기계적 구현을 제공하여 모델체킹뿐 아니라 PROMELA 코드 기반의 연역적 검증의 토대를 마련한다. 특히, PROMELA 언어의 비결정성(nondeterminism), 원자성(atomicity), 발동가능성(enabledness) 등 고수준 선언적 언어의 특성을 저수준 실행가능한 의미구조로 해석하기 위한 의미구조 디자인 패턴 Load-and-Fire를 제안하였다. 이는 PROMELA 프로그램을 실행시키는 과정에서 먼저 복잡한 비결정적 계산구조를 트리로 분해(Load)하여 국소적으로 비결정성을 없앤 후, 트리의 개별 분기에 대해 부수효과를 국소적으로 발동(Fire)하도록 강제하는 패턴이다. 이를 통해 PROMELA 언어의 실행가능한 의미구조를 마치 비결정성이 존재하지 않는 순차적 프로그래밍 언어와 같이 정의할 수 있게 된다.

[연구의 의미]

본 연구는 특정 도구(SPIN)에 종속되어 있던 PROMELA 언어의 기존 한계를 극복하고, 다양한 분석기술을 적용할 수 있는 범용 검증 프레임워크를 제공했다는 점에서 중요한 의의를 가진다. 이러한 분석기술의 확장성은 Load-and-Fire 패턴에 따라 기술된 PRPOMELA 의미구조의 실행가능성에 기반한다. 특히, PROMELA의 실행가능한 의미구조를 기계적으로 구현 및 코드기반 연역적 검증 기능을 도구화하여, 기존의 검증 기술(SPIN)로는 불가능한 PROMELA 모델의 무한 상태공간 안전성 검증이 가능함을 사례연구를 통해 실증하였다. 제안한 Load-and-Fire 패턴은 PROMELA에 국한되지 않고, 향후 다른 동시성 언어의 의미구조 설계에도 활용될 수 있는 일반적인 방법론을 제공한다.

[연구결과의 진행 상태 및 향후 계획]

본 연구는 정형검증 분야 우수 국제학술대회 VMCAI 2026에 발표되었으며, 그 우수성을 입증받아 Distinguished Paper Award를 수상하였다. 향후에는 PROMELA의 코드기반 연역적 검증 기능을 확장하여 더 복잡한 모델(매개화된 동시성 시스템)에 대한 더 복잡한 성질(시제논리성질)의 검증에 적용할 예정이다.

[성과와 관련된 실적]

Byoungho Son and Kyungmin Bae. A Formal Executable Semantics of PROMELA. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2026.

[성과와 관련된 이미지]

그림1.  다양한 분석을 제공하는 PROMELA 언어의 실행가능한 의미구조 개념도