Reo is a graphical channel-based coordination language that enables the modeling of complex behavioral protocols using a small set of channel types with well-defined behavior. Reo has been developed for the coordination of standalone components and services, which makes it suitable for the modeling of service-based business processes. The formal semantic models for Reo lay the grounds for computer-aided analysis of different aspects of Reo diagrams, including their animation, simulation and verification of control flow and data flow by means of model checking techniques. In this paper, we discuss the verification of data aware Reo process models using the mCRL2 model checking toolset including time analysis. We also show how behavior abstraction can be used to minimize Reo process models and generate smaller mCRL2 specifications. A detailed auction example illustrates our approach to timeaware modeling and verification of data-centric service models.
Additional Metadata
ACM SOFTWARE ENGINEERING (acm D.2)
THEME Software (theme 1)
Publisher Springer
Persistent URL dx.doi.org/10.1109/SEFM.2010.26
Series Lecture Notes in Computer Science
Project Compliance-driven Models, Languages and Architectures for Services
Conference IEEE International Conference on Software Engineering and Formal Methods
Citation
Kokash, N, C. (born Köhler, , C.) Krause, ,, & de Vink, E.P. (2010). Time and Data Aware Analysis of Graphical Service Models in Reo. In Proceedings of the IEEE International Conference on Software Engineering and Formal Methods (SEFM). Springer. doi:10.1109/SEFM.2010.26