Automated Analysis of Reo Circuits using Symbolic Execution

Reo is a coordination language that can be used to model different systems. We propose a technique for symbolic execution of Reo circuits using Constraint Automata and more specifically exploiting their data constraints. This technique enables us to obtain the relations among the data passing through different nodes in a circuit and also infer coordination patterns. As an alternative to constructing the symbolic execution tree, we propose an algorithm similar to the algorithms used for converting deterministic finite automata to regular expressions. Our technique can be used for analyzing data-dominated systems whereas the model checking approach is best suited for the study of control-dominated applications. Deadlocks, which may involve data values, can also be checked. We illustrate the technique on a set of data dominated circuits as well as a non-trivial critical section problem. A tool is implemented to automate the proposed technique.