An incremental formal semantics for PROMELA
Carsten Weise · 2002
An approach to a formal semantics for PROMELA is presented. The approach uses SOS rules to define a labeled transition system model for a PROMELA program. The approach is a bottom-up, incremental approach with three basic steps (declarations, single processes, parallel processes). PROMELA before version 2.0 is treated nearly entirely. Especially assertions, never claims and correctness conditions are discussed.