↓Skip to main content

Towards Timed Requirement Verification for Service Choreographies

Verification Fiacre
Table of Contents

Silvano Dal Zilio, Nawal Guermouche
In CollaborateCom 2012 — 8th IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing, oct 2012.

conference paper

 PDF  DOI〈10.4108/icst.collaboratecom.2012.250441〉  HAL-00578436

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.

Citation
#


@InProceedings{DalzilioS:timedreqtchoreographies,
   author    = {{Dal Zilio}, Silvano and Guermouche, Nawal},
   title     = {{Towards Timed Requirement Verification for Service Choreographies}},
   booktitle = {CollaborateCom 2012 -- 8th IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing},
   publisher = {IEEE Computer Society},
   doi = {10.4108/icst.collaboratecom.2012.250441},
   month     = oct, 
   year      = 2012
}