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.

翻译：PROMELA (Process Meta languages) 是设计用于模拟分布式系统互动的一种高规格语言, PROMELA 被用作Spromela SPIN(Spromela Interprepter)模型的输入语言, PROMELA的主要特征是非确定性、通过同步和同步渠道进行过程沟通以及动态创建过程实例的可能性。 在本文中,我们引入了自下而上的固定点语义,旨在模拟 PROMELA 程序的行为。 这项工作是朝着更宏伟的目标迈出的第一步, 即基于抽象解释的分析和核查技术将在这种语义的顶端加以界定。