A LOGICAL FRAMEWORK TO REASON ABOUT REO CIRCUITS

Reo is a graphic-based coordination modelling language which aims to capture and model the interaction between pieces of software, using structures known as channels. The fact that Reo has been used to model many real-world situations, from software components to Smart Cities entities, has attracted attention from researchers, resulting in a great effort directed in its formalization in order to verify and certify properties of Reo circuits. This work presents a constructive formalization in Coq of Reo's formal semantics (based on Constraint Automata) and a formalization in the nuXmv model checker, both with a composition operation and with tools to automate the process. We describe the formalizations and present some usage examples with experimental results.