Motivé par le besoin de la « Conception par Réutilisation », les modèles de processus configurables ont été proposés pour représenter de manière générique des modèles de processus similaires. Ils doivent être configurés en fonction des besoins d’une organisation en sélectionnant des options. Comme les modèles de processus configurables peuvent être larges et complexes, leur configuration sans assistance est sans doute une tâche difficile, longue et source d'erreurs.De plus, les organisations adoptent de plus en plus des environnements Cloud pour déployer et exécuter leurs processus afin de bénéficier de ressources dynamiques à la demande. Néanmoins, en l'absence d'une description explicite et formelle de la perspective de ressources dans les processus métier existants, la correction de la gestion des ressources du Cloud ne peut pas être vérifiée.Dans cette thèse, nous visons à (i) fournir de l’assistance et de l’aide à la configuration aux analystes avec des options correctes, et (ii) améliorer le support de la spécification et de la vérification des ressources Cloud dans les processus métier. Pour ce faire, nous proposons une approche formelle pour aider à la configuration étape par étape en considérant des contraintes structurelles et métier. Nous proposons ensuite une approche comportementale pour la vérification de la configuration tout en réduisant le problème bien connu de l'explosion d'espace d'état. Ce travail permet d'extraire les options de configuration sans blocage d’un seul coup. Enfin, nous proposons une spécification formelle pour le comportement d'allocation des ressources Cloud dans les modèles de processus métier. Cette spécification est utilisée pour valider et vérifier la cohérence de l'allocation des ressources Cloud en fonction des besoins des utilisateurs et des capacités des ressources / Motivated by the need for the “Design by Reuse”, Configurable process models are proposed to represent in a generic manner similar process models. They need to be configured according to an organization needs by selecting design options. As the configurable process models may be large and complex, their configuration with no assistance is undoubtedly a difficult, time-consuming and error-prone task.Moreover, organizations are increasingly adopting cloud environments for deploying and executing their processes to benefit from dynamically scalable resources on demand. Nevertheless, due to the lack of an explicit and formal description of the resource perspective in the existing business processes, the correctness of Cloud resources management cannot be verified.In this thesis, we target to (i) provide guidance and assistance to the analysts in process model configuration with correct options, and to (ii) improve the support of Cloud resource specification and verification in business processes. To do so, we propose a formal approach for assisting the configuration step-by-step with respect to structural and business domain constraints. We thereafter propose a behavioral approach for configuration verification while reducing the well-known state space explosion problem. This work allows to extract configuration choices that satisfy the deadlock-freeness property at one time. Finally, we propose a formal specification for Cloud resource allocation behavior in business process models. This specification is used to formally validate and check the consistency of the Cloud resource allocation in process models according to user requirements and resource capabilities

Depuis plusieurs années, la mondialisation du marché, l'augmentation des exigences des clients, et la recherche permanente d'une baisse des coûts induisent un accroissement fort de la complexité du monde industriel. Ainsi, la collaboration inter-organisationnelle devient essentielle pour maintenir et renforcer la compétitivité des entreprises. Dans cette optique, le système d'information peut, selon sa flexibilité et sa robustesse, freiner ou faciliter cette collaboration. Cette problématique est le point de départ du projet MISE (Mediation Information System Engineering) qui propose une solution pour la conception et la réalisation d'un système d'information collaboratif. Cette solution se base sur une démarche d'ingénierie dirigée par les modèles, couplée à une approche Business Process Management (BPM) et reposant sur les Architectures Orientées Services (SOA). Cette démarche se déroule en deux étapes : (i) la génération d'une cartographie de processus répondant à une situation collaborative (niveau métier), et (ii) sa transformation en un système exécutable (niveau technique). Les travaux présentés dans ce manuscrit s'inscrivent dans cette démarche. Ils s'intéressent en particulier au passage du niveau métier vers le niveau technique en se focalisant sur les aspects non-fonctionnels. Nous présentons une approche permettant (i) d'annoter les activités métier à l'aide d'exigences non-fonctionnelles lors de la modélisation des processus collaboratifs, (ii) de rationaliser la gestion des services et leurs propriétés non-fonctionnelles au moyen de la Gouvernance SOA, et enfin (iii) de faire une réconciliation non-fonctionnelle entre les activités et les services. Nous avons validé les concepts de notre approche au travers de deux prototypes : Petals BPM-NFR pour la modélisation et l'annotation non-fonctionnelle des processus métier, et EasierGov-NFR pour la gouvernance des services et leurs propriétés non-fonctionnelles ainsi que la réconciliation non-fonctionnelle. Un cas d'étude illustre notre approche pour prouver son applicabilité. Ces travaux s'inscrivent au sein du projet européen FP7 CHOReOS. / Over the last years, the globalization, the increase of customers requirements, and the constant search for lower costs, have induced a steep complexity of organization's management. Therefore, inter-organizational collaboration becomes essential to maintain and enhance the competitiveness of enterprises. In this context, the information system may, depending on its flexibility and its robustness, hamper or facilitate this collaboration. One approach to resolve this problem has been taken by the MISE (Mediation Information System Engineering) project. It aims to provide an effective implementation of a collaborative information system, based on Model-Driven Engineering, coupled with a Business Process Management approach (BPM) and supported by Service-Oriented Architecture (SOA). This solution consists in two steps: (i) the generation of a business processes map from the description of a collaborative situation (business level), and (ii) the transformation of these process models into an executable system (technical level). The works detailed in this PhD take roots in this solution and improve it by adding non-functional aspects management during the transition from the business level to the technical level. We present an approach that: first (i) annotates the business activities with Non-Functional Requirements (NFR) in the processes modelling stage, second (ii) rationalizes the management of services and their non-functional properties through SOA Governance, and third (iii) makes a non-functional reconciliation between activities and services. We validate our approach through two prototypes: Petals BPM-NFR for modelling and non-functional annotation of business process, and EasierGov-NFR for the governance of services and their non- functional properties, and the non-functional reconciliation. A case study illustrates our approach to demonstrate its applicability. This work is supported by the FP7 European project CHOReOS.