A logical framework to reason about Reo circuits

Reo is a graphic-based coordination modelling language which aims to cap-ture 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 at-tention 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. © 2022, College Publications. All rights reserved.