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.
|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|
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).