×

Symbolic execution of Reo circuits using constraint automata. (English) Zbl 1242.68073

Summary: 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.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arbab, F.: Reo: a channel-based coordination model for component composition, Mathematical structures in computer science 14, No. 3, 329-366 (2004) · Zbl 1085.68552 · doi:10.1017/S0960129504004153
[2] Arbab, F.; Baier, C.; Rutten, J. J.; Sirjani, M.: Modeling component connectors in reo by constraint automata (extended abstract), Electronic notes in theoretical computer science  97, 25-46 (2004) · Zbl 1105.68058
[3] Baier, C.; Sirjani, M.; Arbab, F.; Rutten, J. J.: Modeling component connectors in reo by constraint automata, Science of computer programming 61, 75-113 (2006) · Zbl 1105.68058 · doi:10.1016/j.scico.2005.10.008
[4] Koehler, C.; Lazovik, A.; Arbab, F.: Reoservice: coordination modeling tool, Lecture notes in computer science 4749, 625-626 (2007)
[5] Lazovik, A.; Arbab, F.: Using reo for service coordination, Lecture notes in computer science 4749, 398-403 (2007)
[6] Meng, S.; Arbab, F.: Web services choreography and orchestration in reo and constraint automata, , 346-353 (2007)
[7] Tasharofi, S.; Vakilian, M.; Ziloochian, R.; Sirjani, M.: Modeling web services using coordination language reo, Lecture notes in computer science 4937, 108-123 (2007)
[8] Tasharofi, S.; Sirjani, M.: Formal modeling and conformance validation for WS-CDL using reo and CASM, Electronic notes in theoretical computer science 159, 99-115 (2008) · Zbl 1347.68240
[9] Mahdikhani, F.; Hashemi, M. R.; Sirjani, M.: QoS aspects in web services compositions, , 239-244 (2008)
[10] N. Kokash, F. Arbab, Applying Reo to service coordination in long-running business transactions, in: Proceedings of the 24st Annual ACM Symposium on Applied Computing, SAC’09, 2009, pp. 1381–1382.
[11] F. Arbab, N. Kokash, S. Meng, Towards using Reo for compliance-aware business process modeling, in: Margaria and Steffen [74], pp. 108–123.
[12] Razavi, N.; Sirjani, M.: Using reo for formal specification and verification of system designs, , 113-122 (2006)
[13] Razavi, N.; Sirjani, M.: Compositional semantics of system-level designs written in systemc, Lecture notes in computer science, 113-128 (2007) · Zbl 1141.68485 · doi:10.1007/978-3-540-75698-9_8
[14] Arbab, F.; Astefanoaei, L.; De Boer, F. S.; Dastani, M.; Meyer, J. -J.C.; Tinnemeier, N. A. M.: Reo connectors as coordination artifacts in 2APL systems, Lecture notes in computer science, 42-53 (2008)
[15] D. Clarke, D. Costa, F. Arbab, Modelling coordination in biological systems, in: Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods, ISoLA’04, 2004, pp. 9–25.
[16] F. Arbab, N. Medvidovic, N. Mehta, M. Sirjani, Modeling behavior in compositions of software architectural primitives, in: Proceedings of the 19th IEEE International Conference on Automated Software Engineering, ASE’04, 2004, pp. 371–374.
[17] Eclipse coordination tools home page, http://reo.project.cwi.nl/cgi-bin/trac.cgi/reo/wiki/Tools.
[18] Klüppelholz, S.; Baier, C.: Symbolic model checking for channel-based component connectors, Electronic notes in theoretical computer science (2006) · Zbl 1167.68035
[19] Baier, C.; Blechmann, T.; Klein, J.; Kluppelholz, S.: A uniform framework for modeling and verifying components and connectors, Lecture notes in computer science 5521, 268-287 (2009)
[20] Groote, J. F.; Mathijssen, A.; Reniers, M.; Usenko, Y.; Weerdenburg, M. V.: The formal specification language mcrl2, (2007) · Zbl 1171.68400
[21] mCRL2, http://www.mcrl2.org. · Zbl 1171.68400
[22] Kokash, N.; Krause, C.; De Vink, E.: Data-aware design and verification of service composition with reo and mcrl2, , 2406-2413 (2010)
[23] Kokash, N.; Krause, C.; De Vink, E.: Time and data aware analysis of graphical service models in reo, (2010) · Zbl 1312.68073
[24] King, J. C.: Symbolic execution and program testing, Communications of the ACM 19, No. 7, 385-394 (1976) · Zbl 0329.68018 · doi:10.1145/360248.360252
[25] Khurshid, S.; Pasareanu, C. S.; Visser, W.: Generalized symbolic execution for model checking and testing, Lecture notes in computer science, 553-568 (2003) · Zbl 1031.68519
[26] Brzozowski, J. A.: Derivatives of regular expressions, Journal of ACM 11, No. 4, 481-494 (1964) · Zbl 0225.94044 · doi:10.1145/321239.321249
[27] C. Gaston, P.L. Gall, N. Rapin, A. Touil, Symbolic execution techniques for test purpose definition, in: Proceedings of the 18th International Conference on Testing Communicating Systems, TestCom’06, 2006, pp. 1–18. · Zbl 1185.68413 · doi:10.1007/11754008_1
[28] C.S. Pasareanu, W. Visser, Verification of java programs using symbolic execution and invariant generation, in: Proceedings of the 11th International SPIN Workshop on Model Checking of Software, SPIN’04, 2004, pp. 164–181. · Zbl 1125.68367 · doi:10.1007/b96721
[29] Anand, S.; Pasareanu, C. S.; Visser, W.: Symbolic execution with abstraction, International journal on software tools for technology transfer (STTT) 11, No. 1, 53-67 (2009)
[30] Kokash, N.; Krause, C.; De Vink, E.: Verification of context-dependent channel-based service models, Lecture notes in computer science (2010) · Zbl 1312.68073
[31] Mousavi, M. R.; Sirjani, M.; Arbab, F.: Formal semantics and analysis of component connectors in reo, Electronic notes in theoretical computer science 154, 83-99 (2006)
[32] Pourvatan, B.; Sirjani, M.; Hojjat, H.; Arbab, F.: Automated analysis of reo circuits using symbolic execution, Electronic notes in theoretical computer science 255, 137-158 (2009) · Zbl 1364.68142
[33] Arbab, F.: Composition of interacting computations, Interactive computation, 277-321 (2006) · Zbl 1266.68089
[34] Papadopoulos, G. A.; Arbab, F.: Coordination models and languages, Advances in computers 46, 330-401 (1998)
[35] Gelernter, D.: Generative communication in linda, ACM transactions on programming languages and systems, No. 1, 80-112 (1985) · Zbl 0559.68030 · doi:10.1145/2363.2433
[36] Colman, A. W.; Han, J.: Coordination systems in role-based adaptive software, Lecture notes in computer science 3454, 63-78 (2005)
[37] Arbab, F.: The IWIM model for coordination of concurrent activities, Lecture notes in computer science 1061, 34-56 (1996)
[38] Cruz, J. C.; Ducasse, S.: A group based approach for coordinating active objects, Lecture notes in computer science 1594, 355-370 (1999)
[39] A. Omicini, F. Zambonelli, Tuple centres for the coordination of Internet agents, in: Proceedings of the ACM Symposium on Applied Computing, 1999, pp. 183–190.
[40] Omicini, A.; Denti, E.: Formal respect, Electronic notes in theoretical computer science  48, 179-196 (2001) · Zbl 1263.68033
[41] Omicini, A.: Formal respect in the A&A perspective, Electronic notes in theoretical computer science 175, 97-117 (2007)
[42] Talcott, C.; Sirjani, M.; Ren, S.: Comparing three coordination models: reo, ARC, and RRD, Electronic notes in theoretical computer science 194, 39-55 (2008) · Zbl 1277.68208
[43] C. Talcott, M. Sirjani, S. Ren, Comparing three coordination models: Reo, ARC, and RRD, Science of Computer Programming, Special issue of FOCLASA’07. · Zbl 1277.68208
[44] Ren, S.; Yu, Y.; Chen, N.; Marth, K.; Poirot, P. -E.; Shen, L.: Actors, roles and coordinators: a coordination model for open distributed and embedded systems, Lecture notes in computer science 4038, 247-265 (2006)
[45] Meseguer, J.; Talcott, C. L.: Semantic models for distributed object reflection, Lecture notes in computer science 2374, 1-36 (2002) · Zbl 1049.68815
[46] Agha, G.: Actors: A model of concurrent computation in distributed systems, (1990)
[47] Sirjani, M.; Jaghoori, M. -M.; Baier, C.; Arbab, F.: Compositional semantics of an actor-based language using constraint automata, Lecture notes in computer science 4038, 281-297 (2006)
[48] D. Jordan, J. Evdemon, Web Services Business Process Execution Language Version 2.0, August 2006.
[49] Web services choreography description language version 1.0, W3C Candidate Recommendation, http://www.w3.org/TR/ws-cdl-10/, November 2005.
[50] Arbab, F.; Rutten, J.: A coinductive calculus of component connectors, Lecture notes in computer science 2755, 34-55 (2002) · Zbl 1278.68200
[51] F. Arbab, CASM: constraint automata with state memory, unpublished notes.
[52] Clarke, L. A.: A system to generate test data and symbolically execute programs, IEEE transactions on software engineering 2, No. 3, 215-222 (1976)
[53] Boyer, R. S.; Elspas, B.; Levitt, K. N.: Select–a formal system for testing and debugging programs by symbolic execution, SIGPLAN notices 10, No. 6, 234-245 (1975)
[54] Zhang, J.; Xu, C.; Wang, X.: Path-oriented test data generation using symbolic execution and constraint solving techniques, , 242-250 (2004)
[55] Zhang, J.: Constraint solving and symbolic execution, Lecture notes in computer science 4171, 539-544 (2008)
[56] Bradley, A. R.; Manna, Z.: The calculus of computation: decision procedures with applications to verification, (2007) · Zbl 1126.03001
[57] Kain, R. Y.: Automata theory: machines and languages, (1981) · Zbl 0504.68045
[58] C. Neumann, Converting deterministic finite automata to regular expressions, 2005.
[59] Arden, D. N.: Delayed-logic and finite-state machines, Theory of computing machine design, 1-35 (1960)
[60] Manna, Z.; Pnueli, A.: Temporal verification of reactive systems (Safety), (1995) · Zbl 0844.68079
[61] Clarke, E. M.; Grumberg, O.; Peled, D. A.: Model checking, (1999) · Zbl 0847.68063
[62] Emerson, E. A.: Temporal and modal logic, Handbook of theoretical computer science, vol. b, 996-1072 (1990) · Zbl 0900.03030
[63] Mcmillan, K.: Symbolic model checking, (1993) · Zbl 0784.68004
[64] Baier, C.; Katoen, J. -P.: Principles of model checking, (2008) · Zbl 1179.68076
[65] Pasareanu, C. S.; Mehlitz, P.; Bushnell, D.; Gundy-Burlet, K.; Lowry, M.; Person, S.; Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software, , 15-26 (2008)
[66] Pandey, M.; Raimi, R.; Bryant, R. E.; Abadir, M. S.: Formal verification of content addressable memories using symbolic trajectory evaluation, , 167-172 (1997)
[67] Bryant, R. E.; Beatty, D. L.; Seger, C. -J.H.: Formal hardware verification by symbolic ternary trajectory evaluation, , 397-402 (1991)
[68] Seger, C. -J.H.; Jones, R. B.; O’leary, J. W.; Melham, T. F.; Aagaard, M.; Barrett, C.; Syme, D.: An industrially effective environment for formal hardware verification, IEEE transactions on CAD of integrated circuits and systems 24, No. 9, 1381-1405 (2005)
[69] Morasca, S.; Pezzè, M.: Validation of concurrent ADA programs using symbolic execution, , 469-486 (1989) · Zbl 0689.68008
[70] Siegel, S. F.; Mironova, A.; Avrunin, G. S.; Clarke, L. A.: Combining symbolic execution with model checking to verify parallel numerical programs, ACM transactions on software engineering and methodology 17, No. 2, 1-34 (2008)
[71] Lynch, N.; Tuttle, M.: An introduction to input/output automata, CWI quarterly 2, No. 3, 219-246 (1989) · Zbl 0677.68067
[72] Arbab, F.; Meng, S.: Synthesis of connectors from scenario-based interaction specifications, Lecture notes in computer science 5282, 114-129 (2008)
[73] F. Arbab, N. Kokash, S. Meng, Towards using reo for compliance-aware business process modeling, in: Margaria and Steffen [74], pp. 108–123.
[74] , Communications in computer and information science 17 (2008)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.