Automated Analysis of Reo Circuits using Symbolic Execution

https://doi.org/10.1016/j.entcs.2009.10.029Get rights and content
Under a Creative Commons license
open access

Abstract

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.

Keywords

Symbolic Execution
Reo
Constraint Automata
Coordination Languages
Program Verification

Cited by (0)