A denotational semantics for PROMELA addressing arbitrary jumps

TL;DR

This paper introduces a formal denotational semantics for PROMELA, capturing its complex features like arbitrary jumps and process interactions, to facilitate formal analysis and verification of distributed system models.

Contribution

It presents the first bottom-up, fixpoint semantics for PROMELA, enabling future abstract interpretation and formal verification techniques.

Findings

Provides a formal semantics capturing PROMELA's features

Lays groundwork for analysis and verification methods

First semantics to handle arbitrary jumps in PROMELA

Abstract

PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes. In this paper, we introduce a bottom-up, fixpoint semantics that aims to model the behavior of PROMELA programs. This work is the first step towards a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.