Integrating tools to reason about Reo circuits
Mariana Ferreira, Bruno Lopes · 2022
Critical systems are present in many applications and require high reliability. However, there are still challenges for the verification and certification of these systems. The graphical language Reo is based on coordination and model the communication of software components. A set of existing tools offers compilers and reasoners based on proof assistants and model checkers for Reo-specified systems. This paper proposes the integration of these compilers through an interface that allows building Reo circuits, converting the model to the compilers' input language, simplifying the use of logic tools and allowing the creation of new channels in addition to the canonical ones. The theory used, integrated tools, features of interface and some examples are presented.