Formal Requirement Verification for Timed Choreographies
Résumé
Time plays a crucial role when reasoning about the composition of Web Services. Nonetheless, while the addition of temporal aspects in the specification of services improves expressiveness, it also makes reasoning about service composition much harder. In this work, we propose an approach for analyzing and validating a composition of services with respect to time related 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 on the delay between events. The goal is to check whether a choreography obtained from the composition of timed services satisfies given 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 real-time requirements and on specific tooling for model-checking Fiacre specifications.
Origine : Fichiers produits par l'(les) auteur(s)