2021/08/27 by Marco Comini, Comini, Marco, María del Mar Gallardo +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Petri Nets in System Modeling #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2108.12348
openalex publication_date 2021/08/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.