Symbolic execution of Reo circuits using constraint automata

Reo is a coordination language that can be used to model different systems. We propose a technique for symbolic execution of Reo circuits using the symbolic representation of data constraints in Constraint Automata. This technique enables us to obtain the relations among the data that pass through different nodes in a circuit from which we infer the coordination patterns of the circuit. Deadlocks, which may involve data values, can also be checked using reachability analysis. As an alternative to constructing the symbolic execution tree, we use regular expressions and their derivatives which we obtain from our deterministic finite automata. We show that there is an upper bound of one for unfolding the cycles in constraint automata which is enough to reveal the relations between symbolic representations of inputs and outputs. In the presence of feedback in a Reo circuit a number of substitutions are necessary to make the relationship between successive input/output values explicit. The number of these substitutions depends on the number of buffers in the Reo circuit, and can be found by static analysis. We illustrate our technique on a set of Reo circuits to show the extracted relations between inputs and outputs. We have implemented a tool to automate our proposed technique.