Research Article
Towards Timed Requirement Verification for Service Choreographies
@INPROCEEDINGS{10.4108/icst.collaboratecom.2012.250441, author={Nawal Guermouche and Silvano Dal Zilio}, title={Towards Timed Requirement Verification for Service Choreographies}, proceedings={8th IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing}, publisher={IEEE}, proceedings_a={COLLABORATECOM}, year={2012}, month={12}, keywords={timed bpel processes choreography analysis asynchronous services real-time requirements formal verification}, doi={10.4108/icst.collaboratecom.2012.250441} }- Nawal Guermouche
Silvano Dal Zilio
Year: 2012
Towards Timed Requirement Verification for Service Choreographies
COLLABORATECOM
ICST
DOI: 10.4108/icst.collaboratecom.2012.250441
Abstract
In this paper, we propose an approach for analyzing and validating a composition of services with respect to real time properties. We consider services defined using an extension of the Business Process Execution Language (BPEL) where timing constraints can be associated to the execution of an activity or define delays between events. The goal is to check whether a choreography of timed services satisfies given complex real time requirements. Our approach is based on a formal interpretation of timed choreographies in the Fiacre verification language that defines a precise model for the behavior of services and their timed interactions. We also rely on a logic-based language for property definition to formalize complex real-time requirements and on specific tooling for model-checking Fiacre specifications.