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.

Additional Metadata
Keywords Component-based systems, Promela/SPIN, Reo circuits, Verification
Journal Proceedings of 21st MODELS Workshops 2018: Copenhagen, Denmark
Conference 21st MODELS Workshops 2018: Copenhagen, Denmark
Citation
Lion, B, Chouali, S, & Arbab, F. (2018). Compiling protocols to Promela and verifying their LTL properties. In Proceedings of 21st MODELS Workshops 2018: Copenhagen, Denmark (pp. 31–39).