Reo Tool for Model-Checking Dataflow in Service Compositions

Organisation:	CWI Amsterdam (THE NETHERLANDS) Eindhoven University of Technology (THE NETHERLANDS) Hasso Plattner Institute, Potsdam (GERMANY)
Functionality:	Verification of service compositions.
Tools used:	ECT (Extensible Coordination Tools) mCRL2 CADP (Construction and Analysis of Distributed Processes)
Period:	2012
Description:	The paradigm of service-oriented computing revolutionized the field of software engineering. According to this paradigm, new systems are composed of existing stand-alone services to support complex cross-organizational business processes. Correct communication of these services is not possible without a proper coordination mechanism. The Reo coordination language is a channel-based modeling language that introduces various types of channels and their composition rules. By composing Reo channels, one can specify Reo connectors that realize arbitrary complex behavioral protocols. Several formalisms have been introduced to give semantics to Reo. In their most basic form, they reflect service synchronization and dataflow constraints imposed by connectors. To ensure that the composed system behaves as intended, a wide range of automated verification tools is needed to assist service composition designers. This work proposes a new framework for the verification of Reo using formal languages and tools from the concurrency domain, namely the mCRL2 and CADP tool sets. Several semantic models for Reo (constraint automata, timed constraint automata, coloring semantics, and action constraint automata) are mapped to the process algebraic specification language of mCRL2. The conversion from Reo to mCRL2 was implemented as an extension to the Extensible Coordination Tools (ECT), which is a framework for modeling, verification, and execution of component-based and service-oriented systems. ECT consists of a set of integrated tools for the Eclipse platform, providing functionalities for converting high-level modeling languages (e.g., UML, BPMN, and BPEL) to Reo, for editing and animation of Reo models, generation of automata-based semantical models from Reo, modeling and verification of QoS properties and tight integrations with external model checking tools such as Vereofy or PRISM. The conversion tool takes as input a Reo circuit and generates automatically a corresponding mCRL2 specification. The tool also provides an integration with CADP by generating labeled transition systems, converting them in the BCG format, and invoking the EVALUATOR model checker from ECT. In [Kokash-Krause-deVink-12] it is reported that: The main advantage of using model checking tools from the CADP suite is the ability to extract counterexamples which is currently only indirectly supported for the lps2pbes model checker from the mCRL2 toolbox. The formal modeling and analysis approach for Reo in the setting of service-based processes is illustrated by means of an Access Control System used to restrict the opening of a door to a group of trusted people which have to authenticate themselves with an identity card and a personal identification number.
Conclusions:	The newly added plug-in, together with other tools from ECT, provides a user-friendly environment for graphical modeling of component/service-based systems and business processes. Since Reo has an intuitive graphical notation, workflow models designed with ECT look similar to UML activity diagrams. This facilitates the use of the framework by any workflow designer. As regards future work, an interesting direction is to extend the framework with performance analysis using appropriate tools from CADP.
Publications:	[Kokash-Krause-deVink-12] Natallia Kokash, Christian Krause, and Erik de Vink. "Reo+mCRL2: A Framework for Model-Checking Dataflow in Service Compositions". Formal Aspects of Computing 24(2):187-216, March 2012. Available on-line at: http://homepages.cwi.nl/~kokash/documents/FACJ11.pdf or from the CADP Web site in PDF or PostScript
Contact:	Erik de Vink Department of Mathematics and Computer Science Technische Universiteit Eindhoven Den Dolech 2 Eindhoven The Netherlands Tel: +31-40-2473146 Fax: +31-40-2476685 Email: evink@win.tue.nl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page