Information Technology Reference
In-Depth Information
9 Conclusions
In this paper, we presented an extended approach for mapping Reo connectors
to the process algebra
mCRL2
. More specifically, we proved the correctness of the
mapping, extended the conversion tool with the ability to deal with context-
sensitive Reo, and evaluated the tool performance in the presence of optimiza-
tion techniques. Together with other tools from ECT, our plug-in provides a
user-friendly environment for graphical modeling of component/service-based
systems and business processes. On the one hand, this releases developers from
the need to encode the behavior of their systems in the specification language
mCRL2
directly. On the other hand, the
mCRL2
toolset supports full-featured model
checking for Reo.
Future work includes the application of our approach to larger examples to
assess its practicality and scalability. Also, we plan to extend our approach by
incorporating timer channels [16] according to their semantics in terms of TCA.
This will enable the analysis of timed properties for channel-based service mod-
els. Another direction of our research is an extension of Reo semantics with
various actions observable on channel ports. In particular, this will allow us to
model data flow within synchronous regions of a connector and, given time de-
lays for each channel, estimate total delays of the circuits. Finally, as mentioned
before, we will integrate CADP support to our tools.
Acknowledgment.
We are indebted to the reviewers for their detailed feedback
and constructive comment.
References
1. Arbab, F.: The IWIM model for coordination of concurrent activities. In: Hankin,
C., Ciancarini, P. (eds.) COORDINATION 1996. LNCS, vol. 1061, pp. 34-56.
Springer, Heidelberg (1996)
2. Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in
Reo by constraint automata. Science of Computer Programming 61, 75-113 (2006)
3. Clarke, D., Costa, D., Arbab, F.: Connector coloring I: Synchronization and context
dependency. Science of Computer Programming 66(3), 205-225 (2007)
4. Arbab, F., Koehler, C., Maraikar, Z., Moon, Y., Proenca, J.: Modeling, testing
and executing Reo connectors with the Eclipse Coordination Tools. In: Tool demo
session at FACS 2008 (2008)
5. Baier, C., Blechmann, T., Klein, J., Kluppelholz, S.: A uniform framework for
modeling and verifying components and connectors. In: Field, J., Vasconcelos, V.T.
(eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 268-287. Springer, Heidelberg
(2009)
6. Kokash, N., Krause, C., de Vink, E.: Data-aware design and verification of service
composition with Reo and mCRL2. In: Shin, S.Y., et al. (eds.) Proc. SAC 2010,
pp. 2406-2413. ACM, New York (2010)
7. Groote, J., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.: The
formal specification language mCRL2. In: Brinksma, E., Harel, D., Mader, A.,
Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software Systems. IBFI,
Schloss Dagstuhl (2007)
