Journée “méthodes formelles et processus métier”

Une journée sur le thème “méthodes formelles et processus métier” (workflow, services Web, contrats QoS, …) se tiendra le 16 octobre 2014 à Paris.
Organisée avec le soutien du GDR GPL.

Lieu : LIP6, Paris 6 (Jussieu) - salle 203-205 bâtiment 41 .

Programme de 6 exposés d’environ 1h (incluant les questions) :

• Yoann LAURENT (LIP6) Alloy4SPV: a Formal Framework for Software Process Verification. 


In this work we present a framework for software process verification called Alloy4SPV which uses a subset of UML2 Activity Diagrams as a process modeling language. In order to achieve software process verification, we i) define a formal model of our process modeling language using first-order logic, ii) we give it a formal semantics based on the fUML standard, and iii) we implement this formalization using the Alloy language. In order to ease its adoption by process modelers, our framework comes with a graphical tool and a ready to use and customizable set of software process properties. We categorize these properties into two categories, syntactical and behavioral. We extend the set of behavioral properties we identified from the literature with two new categories that we defined, namely, organizational properties which relate to resource management and planning during process execution and business properties which are project/process specific properties.

• Tarek MELLITI (IBISC) Formal Modelling and Evaluation of Service-based Business Process Elasticity in the Cloud. 


One of the expected features of Cloud environments is elasticity at different levels in order to guarantee provisioning of necessary resources that ensure a smooth functioning of cloud services despite changes in solicitations. Nevertheless, the provisioning of elastic infrastructures and/or platforms is not sufficient to provide users with elasticity at the level of Service-based Business Processes (SBPs). Therefore, there is a need to provide SBPs with mechanisms to scale their resource requirements up and down to ensure their adaptation to the workload changes. This can be achieved using mechanisms for duplicating and consolidating business services that compose the SBP. In this talk, we present a formal unified model (Timed Petri-nets) for SBPs elasticity. We show that our model preserves the semantics of SBPs when services are duplicated or consolidated. Based on this model, we propose a framework that defines and evaluates (by Simulation and Verification) elasticity strategies (defined as colored Petri nets). Our elasticity strategies could be a formal start to Services Level Agreement languages. The complete approach is experimented in a real Cloud environment.

• Kais KLAI (LIPN) Abstraction and Modular Verification of Inter-Enterprise Business Processes. 


Business process composition and cooperation are two important research fields in the business process domain. The questions, what properties of a process have to be public so that potential partners can collaborate with the process without risking to have an ill-designed composed process, and what is the minimal information necessary to be published, is a hot topic in the literature since many years. Also, one has to make sure that the composition of processes has the desired behaviour. The importance of dealing with such inter-enterprise business processes (IEBP for short) on one hand and business process composition on the other hand is reflected in the literature by numerous publications. In general, an IEBP can be considered as the cooperation of several local processes designed separately. The activities of each process are formally of two kinds: internal activities and cooperative activities (interface activities). IEBP are often too large for formal analysis, and the details of the components are hidden to the public so that no party knows the entire process definition. Therefore, we defend the idea that the analysis should be on the local business process and, if necessary, on an abstraction of the pertness models or of the IEBP.
In this talk, we will present our contributions on abstraction and verification of IEBP. These contribution are mainly based on the Event-based Symbolic Observation Graph approach. Tow kinds of properties will be considered: generic properties (deadlock freeness, different variants of the soundness property) and specific properties (expressed by LTL logic).

• Laurence DUCHIEN (LIFL) Une approche formelle pour la préservation de contrats de qualité de service lors de reconfiguration dynamique.

L’omniprésence de services informatiques dans la vie quotidienne, combinée à la nature dynamique de leurs contextes d’exécution, constitue un défi majeur pour garantir la qualité attendue de ces services à l’exécution. Des contrats de Qualité de service (QoS) ont été proposés pour spécifier les niveaux de QoS attendus sur les différentes conditions de contexte, à l’aide de différents mécanismes. Dans cet exposé, nous présentons une définition des contrats de qualité de service en tant que politique de haut niveau pour régir le comportement des logiciels qui s’adaptent automatiquement à l’exécution, en réponse aux changements de contexte. Pour réaliser ce contrat, nous spécifions sa sémantique formelle et nous la mettons en œuvre dans un cadre logiciel capable d’exécuter et de reconfigurer des services, en vue de maintenir les contrats de qualité de service associés. Dans un premier temps, nous étendons les systèmes de transformation des graphes typés attribués et des machines à états finis, et nous les utilisons comme dénotations pour spécifier la sémantique des contrats de qualité de service. Deuxièmement, cette sémantique permet d’exploiter systématiquement des patrons de conception à l’exécution pour leur déploiement dynamique dans le logiciel. Troisièmement, notre sémantique garantit des propriétés d’auto-adaptation telles que la fiabilité et la robustesse dans la satisfaction de contrat. Enfin, nous évaluons l’applicabilité de notre mise en œuvre en l’intégrant et en l’exécutant dans Frascati, un middleware à base de composants multi-échelle, dans une étude de cas.

• Nikolaos GEORGANTAS (INRIA) Service Choreographies: The Case for Interaction Paradigm Interoperability.


With an increasing number of services and devices interacting in a decentralized manner, choreographies are an active area of investigation. The heterogeneous nature of interacting systems leads to choreographies that may not only include conventional services but also sensor-actuator networks, shared data spaces and event-based systems. Their middleware behavior within choreographies can be captured through abstract interaction paradigms, such as client-service, publish-subscribe and tuple space. This raises the essential issue of distributed system interoperability within heterogeneous choreographies. Open system integration paradigms, such as service oriented architecture (SOA) and enterprise service bus (ESB), have provided answers to the interoperability requirement. However, when it comes to integrating systems featuring heterogeneous interaction paradigms, existing solutions are typically ad hoc and partial, applying to specific interaction protocol technologies. In this talk, we introduce an interoperability solution based on abstraction and merging of the common high-level semantics of interaction paradigms, which is sufficiently general and extensible to accommodate many different protocol technologies. We apply this solution to revisit the SOA- and ESB-based integration of heterogeneous distributed systems.

• Pascal POIZAT (LIP6) Développement Formel de Processus Métier Chorégraphiques


Les processus métier collaboratifs peuvent être vus selon deux perspectives complémentaires.
Dans la première il s’agit d’inter-connecter les modèles des pairs participant à la collaboration.
C’est une approche qui convient bien à un développement « bottom-up », par réutilisation et assemblage de pairs.
Dans la seconde, les interactions entre pairs sont des entités de premier ordre, et il est possible de décrire les processus métiers collaboratifs d’un point de vue global, aussi appelé chorégraphique.
Cela convient bien à un développement « top-down », par spécification et génération d’obligations locales (ou squelettes de pairs).
Deux problèmes importants lors de la conception de processus métiers chorégraphiques (BPC) sont d’un côté la conformité entre une spécification et un ensemble de modèles de pairs
et d’un autre côté la réalisabilité d’une spécification, c’est-à-dire la possibilité d’obtenir des modèles conformes de pairs à partir de la spécification.
Ces problèmes ont été étudiés principalement pour des modèles interconnectés et plus récemment des modèles d’interactions.
Par ailleurs, la prise en compte des données échangées entre les partenaires d’un processus métier collaboratif nécessite habituellement une sur-approximation ou un bornage du domaine des données.
Dans cet exposé je présenterai des résultats récents quant à la vérification de BPC décrits dans le standard BPMN 2.0 ainsi qu’une approche symbolique basée sur l’utilisation d’un solveur SMT pour la prise en compte des données dans cette vérification.