Laboratoire d’Analyse et d’Architecture des Systèmes
N.GUERMOUCHE, S.DAL ZILIO
SARA, VERTICS
Manifestation avec acte : IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing ( COLLABORATECOM ) 2012 du 14 octobre au 17 octobre 2012, Pittsburgh (USA), Octobre 2012, 10p. , N° 12495
Diffusable
Plus d'informations
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.
S.REBAI, H.HADJ KACEM, A.HADJ KACEM, N.GUERMOUCHE
ReDCAD Laboratory, SARA
Rapport LAAS N°12496, Septembre 2012, 16p.
Lien : http://hal.archives-ouvertes.fr/hal-00733861
Diffusable
Plus d'informations
This paper introduces an approach addressing the transition from choreography to orchestration. As far as validation method is achieved through the use of model-checker. We are interested in various levels of transformations. Initially, the process of transformation is based on a set of heterogeneous business protocols. This unit will consequently provide a choreography as result, which unifies them. Then, this choreography will be transformed into an orchestration. Thus, coherence between choreography and orchestration must be checked while showing the relation of conformity between these two different composition models. Indeed, this passage is accompanied by a verification phase. A set of properties will be preserved, the ones, which refer to the choreography and others, which are relative to those checked by the orchestration. Towards the end of this process, and in order to validate the transformation, we must check the maintained properties. This checking will be illustrated by the use of the model-checker, which depends on the properties.
I.GUIDARA, N.GUERMOUCHE, T.CHAARI, S.TAZI
SARA
Manifestation avec acte : Interoperability for Enterprise Systems and Applications (I-ESA 2012). Workshop: Factories of the future (FoF), Valence (Espagne), 20-23 Mars 2012, pp.267-274 , N° 12170
Lien : http://hal.archives-ouvertes.fr/hal-00676200
Diffusable
Plus d'informations
SLA (Service Level Agreement) is a contract between a service consumer and a service provider. It aims at specifying conditions of services delivery and guarantees to ensure required quality of service (QoS). Nowadays, to satisfy complex client needs, inter-enterprises collaboration must take place to provide new value added services and form inter-organizational extended enterprises. In this context, SLAs composition primitives are needed to define complex dependencies and agreements between services composition. In this paper, we are interested in the problem of SLAs composition where consumer-to-provider and provider-to-provider relationships can hold in cross-organizational enterprise. The aim is to define a framework to assist business decision makers to automatically generate and manage a composition of SLAs to fulfill end-to-end functional and non functional requirements.