Automated Analysis of Reo Circuits using Symbolic Execution
Electronic Notes in Theoretical Computer Science , Volume 255 - Issue 10 p. 137- 158
Presented at the International Workshop on the Foundations of Coordination Languages and Software Architecture, Rhodes, Greece
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|
|THEME||Software (theme 1)|
|Journal||Electronic Notes in Theoretical Computer Science|
|Conference||International Workshop on the Foundations of Coordination Languages and Software Architecture|
Pourvatan, B, Sirjani, M, Hojjat, H, & Arbab, F. (2009). Automated Analysis of Reo Circuits using Symbolic Execution. In Electronic Notes in Theoretical Computer Science (Vol. 255, pp. 137–158). Elsevier.