Time and data-aware analysis of graphical service models in Reo

N. Kokash, C. Krause, E.P. Vink, de

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

25 Citations (Scopus)
82 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010, Pisa, Italy, September 13-18, 2010)
Place of PublicationLos Alamitos CA
PublisherIEEE Computer Society
Pages125-134
ISBN (Print)978-1-4244-8289-4
DOIs
Publication statusPublished - 2010

Fingerprint Dive into the research topics of 'Time and data-aware analysis of graphical service models in Reo'. Together they form a unique fingerprint.

Cite this