Compiling protocols to Promela and verifying their LTL properties

Component-based systems can be modeled as black-box, standalone components, coordinated by an interaction protocol. In this paper we focus on developing reliable protocols, specified in a coordination language where their design, implementation, and property verification rely on the exact same model. In this context, to construct complex protocols compositionally, we use Reo, a powerful channel-based coordination language with well-defined semantics. We extend the current set of back-end languages supported by Reo's compiler with Promela, the specification language of the model checker SPIN. The automatic generation of Promela code from Reo specification enables system simulation and verification of LTL properties of Reo models using SPIN.