Protocol verification with reactive PROMELA/RSPIN
Elie Najm, Frank Olsen · DIMACS series in discrete mathematics and theoretical computer science · 1997
Reactive Promela/RSPIN is an extension to the protocol validator Promela/SPIN. It enhances thesimulation and verification capabilities of SPIN by allowing modular specifications to be analysed while alleviating the state-space explosion problem. Reactive Promela is a simple reactive language. Thetool RSPIN is a preprocessor for SPIN which translates a Reactive specification into a corresponding specification. The main function performed by RSPIN is to combine configurations of Reactive Promela automata into Promela proctypes.