Search

Current softwares are built using "agile" development methods, to better consider the need to adapt to new user requirements. Developers and designers are getting closer to future software users by making short iterative cycles, where the future user gives a fast feedback on the increment made to the software and emits new user requirement to be fulfilled in future increments. These iterations can be seen as evolutions, as an answer to the definition of a new user requirement, or due to a change in the execution environment or in the architecture of the software. In the Service-Oriented Architecture (SOA) world, the design of software is composed of service choreography, or service orchestration using business processes. The design of these applications is equivalent to connecting the services control flow and data flow. As a result, the evolution step becomes a complex step, where a simple modification on a sub-part of a business process can have consequences on the entire system, causing for example its slowing down at runtime. From the Quality of Service (QoS) point of view, ensuring the fiability of the evolution process to maintain software QoS is critical. As a result, it is necessary to propose agile, reliable evolution mecanisms ensuring QoS preservation during the evolution of software made of business processes. In other words, we need to control that an evolution does not violate any QoS contract initially set up. Depending of the contract, this garanty must be established either at design time or at runtime. In the latter case, the verification process must be minimal and local, in order to not degrade the software performance. To achieve this goal, we propose to realise an agile development cycle, centered on the QoS preservation during the evolution. It is necessary to care about the evolutive concern of a system from the initial design step, by identifying required information to determine if the QoS continues to be correct and not violated by an evolution. Considering that this information is known by many stakeholders, it is also necessary to set up interaction points during the development cycle, during which information is shared in order to keep building a syntactically and semantically coherent software and to minimally (re)check QoS contracts. The contributions of this thesis are applied in Blink, a development cycle for evolution, and Smile, a framework to maintain QoS during the evolution of a service-oriented software made of business processes. While Blink is intended to identify the different actors and to make their interactions explicit, Smile proposes the realisation of an evolution loop. This loop enables the design, analysis and application of an evolution, by detecting the potential QoS contract violation. The evolution analysis determines its effect on the software QoS, by defining causal relations among variables, operations, services and other parts of the system. In this way, by identifying elements that are causally affected by the evolution, and by avoiding the elements that are not, our approach enables the limitation of the number of elements to (re)check in order to assure a reliable evolution step, with a minimal (re)check step. We show on the concrete case of a crisis management system, composed of eleven bu- siness processes and ten scenarios, that the combined use of Blink and Smile enables for each evolution the identification of its effect on the system, and the QoS preservation of the system.; Les logiciels actuels adoptent une méthodologie de développement dite "agile" pour mieux prendre en compte la nécessité de s'adapter constamment aux nouveaux besoins des utilisateurs. Les concepteurs et développeurs se rapprochent alors des futurs utilisateurs du logiciel en proposant des cycles courts d'itération, où le futur utilisateur fait un retour rapide sur l'incrément apporté au logiciel, et fait part de nouveaux besoins à prendre en compte dans les incréments à venir. Ces itérations peuvent être vues comme des évolutions, faisant suite à la définition d'un nouveau besoin de l'utilisateur, à un changement de l'en- vironnement d'exécution, ou encore à une remise en question de l'architecture du logiciel. Dans l'écosystème des architectures orientées services, la conception d'applications passe par la chorégraphie ou l'orchestration de services par des processus métiers. Concevoir ces applications consiste alors à mettre en relation les flots de contrôle et de données de ces services. La phase d'évolution devient une phase complexe, où une simple modification lo- calisée à une sous-partie d'un processus métier peut avoir des conséquences sur l'ensemble du système logiciel, causant par exemple son ralentissement lors de l'exécution. Du point de vue de la qualité de service (QoS), la maîtrise de la fiabilité du processus d'évolution pour maintenir la qualité de service d'un logiciel est alors critique. Il est donc nécessaire de pouvoir proposer des mécanismes d'évolution agiles et fiables permettant le maintien de la QoS lors de l'évolution d'applications à base de processus métiers. En d'autres termes, il s'agit de s'assurer qu'une évolution ne viole pas les contrats de QoS définis initialement. Cette garantie doit être établie en fonction du contrat soit lors de la conception soit lors de l'exécution. Dans ce dernier cas, le processus de vérification doit être minimal et localisé, afin de ne pas dégrader les performances du système logiciel. Pour cela, nous proposons de mettre en œuvre un cycle de développement agile, centré sur le maintien de la QoS lors de l'évolution. Il s'agit de prendre l'aspect évolutif du système, ceci dès l'étape de conception initiale, en identifiant les informations requises pour déter- miner si la QoS est correcte et si elle est non violée par une évolution. Ces informations étant détenues par plusieurs intervenants, il est également nécessaire d'établir les points d'interaction au cours du cycle de développement, au cours desquels les informations seront partagées de façon à ce que le logiciel qui en est issu reste syntaxiquement et sémantique- ment cohérent et que les contrats de QoS soient (re)vérifiés a minima. Les contributions de cette thèse sont donc mises en œuvre dans Blink, un cycle de développement pour l'évolu- tion, et Smile, un canevas de développement pour le maintien de la qualité de service lors de l'évolution d'applications orientées service définies à base de processus métiers. Tandis que le cycle de développement Blink vise à identifier les différents rôles présents dans l'équipe de développement et à expliciter leurs interactions, le canevas Smile propose la réalisation d'une boucle d'évolution. Cette boucle permet de concevoir, d'analyser et d'appliquer une évolution, en détectant les potentielles violations de contrat de QoS. Pour cela, l'analyse de l'évolution détermine son effet sur la QoS du logiciel, en établissant des relations de causalité entre les différentes variables, opérations, services et autres parties du système. Ainsi, en identifiant les éléments causalement affectés par l'évolution et en écartant ceux qui ne le sont pas, notre approche permet de limiter le nombre d'éléments à (re)vérifier, garantissant ainsi une étape d'évolution fiable, avec une étape de (re)vérification minimale. Nous montrons sur un cas concret de système de gestion de crises, constitué de onze processus métiers et de dix scénarios, que l'utilisation conjointe de Blink et de Smile permet d'identifier, pour chaque évolution, quel sera son effet sur le reste du système, et si la qualité de service sera maintenue ou non.

Current softwares are built using "agile" development methods, to better consider the need to adapt to new user requirements. Developers and designers are getting closer to future software users by making short iterative cycles, where the future user gives a fast feedback on the increment made to the software and emits new user requirement to be fulfilled in future increments. These iterations can be seen as evolutions, as an answer to the definition of a new user requirement, or due to a change in the execution environment or in the architecture of the software. In the Service-Oriented Architecture (SOA) world, the design of software is composed of service choreography, or service orchestration using business processes. The design of these applications is equivalent to connecting the services control flow and data flow. As a result, the evolution step becomes a complex step, where a simple modification on a sub-part of a business process can have consequences on the entire system, causing for example its slowing down at runtime. From the Quality of Service (QoS) point of view, ensuring the fiability of the evolution process to maintain software QoS is critical. As a result, it is necessary to propose agile, reliable evolution mecanisms ensuring QoS preservation during the evolution of software made of business processes. In other words, we need to control that an evolution does not violate any QoS contract initially set up. Depending of the contract, this garanty must be established either at design time or at runtime. In the latter case, the verification process must be minimal and local, in order to not degrade the software performance. To achieve this goal, we propose to realise an agile development cycle, centered on the QoS preservation during the evolution. It is necessary to care about the evolutive concern of a system from the initial design step, by identifying required information to determine if the QoS continues to be correct and not violated by an evolution. Considering that this information is known by many stakeholders, it is also necessary to set up interaction points during the development cycle, during which information is shared in order to keep building a syntactically and semantically coherent software and to minimally (re)check QoS contracts. The contributions of this thesis are applied in Blink, a development cycle for evolution, and Smile, a framework to maintain QoS during the evolution of a service-oriented software made of business processes. While Blink is intended to identify the different actors and to make their interactions explicit, Smile proposes the realisation of an evolution loop. This loop enables the design, analysis and application of an evolution, by detecting the potential QoS contract violation. The evolution analysis determines its effect on the software QoS, by defining causal relations among variables, operations, services and other parts of the system. In this way, by identifying elements that are causally affected by the evolution, and by avoiding the elements that are not, our approach enables the limitation of the number of elements to (re)check in order to assure a reliable evolution step, with a minimal (re)check step. We show on the concrete case of a crisis management system, composed of eleven bu- siness processes and ten scenarios, that the combined use of Blink and Smile enables for each evolution the identification of its effect on the system, and the QoS preservation of the system.; Les logiciels actuels adoptent une méthodologie de développement dite "agile" pour mieux prendre en compte la nécessité de s'adapter constamment aux nouveaux besoins des utilisateurs. Les concepteurs et développeurs se rapprochent alors des futurs utilisateurs du logiciel en proposant des cycles courts d'itération, où le futur utilisateur fait un retour rapide sur l'incrément apporté au logiciel, et fait part de nouveaux besoins à prendre en compte dans les incréments à venir. Ces itérations peuvent être vues comme des évolutions, faisant suite à la définition d'un nouveau besoin de l'utilisateur, à un changement de l'en- vironnement d'exécution, ou encore à une remise en question de l'architecture du logiciel. Dans l'écosystème des architectures orientées services, la conception d'applications passe par la chorégraphie ou l'orchestration de services par des processus métiers. Concevoir ces applications consiste alors à mettre en relation les flots de contrôle et de données de ces services. La phase d'évolution devient une phase complexe, où une simple modification lo- calisée à une sous-partie d'un processus métier peut avoir des conséquences sur l'ensemble du système logiciel, causant par exemple son ralentissement lors de l'exécution. Du point de vue de la qualité de service (QoS), la maîtrise de la fiabilité du processus d'évolution pour maintenir la qualité de service d'un logiciel est alors critique. Il est donc nécessaire de pouvoir proposer des mécanismes d'évolution agiles et fiables permettant le maintien de la QoS lors de l'évolution d'applications à base de processus métiers. En d'autres termes, il s'agit de s'assurer qu'une évolution ne viole pas les contrats de QoS définis initialement. Cette garantie doit être établie en fonction du contrat soit lors de la conception soit lors de l'exécution. Dans ce dernier cas, le processus de vérification doit être minimal et localisé, afin de ne pas dégrader les performances du système logiciel. Pour cela, nous proposons de mettre en œuvre un cycle de développement agile, centré sur le maintien de la QoS lors de l'évolution. Il s'agit de prendre l'aspect évolutif du système, ceci dès l'étape de conception initiale, en identifiant les informations requises pour déter- miner si la QoS est correcte et si elle est non violée par une évolution. Ces informations étant détenues par plusieurs intervenants, il est également nécessaire d'établir les points d'interaction au cours du cycle de développement, au cours desquels les informations seront partagées de façon à ce que le logiciel qui en est issu reste syntaxiquement et sémantique- ment cohérent et que les contrats de QoS soient (re)vérifiés a minima. Les contributions de cette thèse sont donc mises en œuvre dans Blink, un cycle de développement pour l'évolu- tion, et Smile, un canevas de développement pour le maintien de la qualité de service lors de l'évolution d'applications orientées service définies à base de processus métiers. Tandis que le cycle de développement Blink vise à identifier les différents rôles présents dans l'équipe de développement et à expliciter leurs interactions, le canevas Smile propose la réalisation d'une boucle d'évolution. Cette boucle permet de concevoir, d'analyser et d'appliquer une évolution, en détectant les potentielles violations de contrat de QoS. Pour cela, l'analyse de l'évolution détermine son effet sur la QoS du logiciel, en établissant des relations de causalité entre les différentes variables, opérations, services et autres parties du système. Ainsi, en identifiant les éléments causalement affectés par l'évolution et en écartant ceux qui ne le sont pas, notre approche permet de limiter le nombre d'éléments à (re)vérifier, garantissant ainsi une étape d'évolution fiable, avec une étape de (re)vérification minimale. Nous montrons sur un cas concret de système de gestion de crises, constitué de onze processus métiers et de dix scénarios, que l'utilisation conjointe de Blink et de Smile permet d'identifier, pour chaque évolution, quel sera son effet sur le reste du système, et si la qualité de service sera maintenue ou non.

In past years, formal verification techniques and tools were widely developed and used by the research community. However, the use of formal verification at industrial scale remains difficult, expensive and requires lot of time. This is due to the size and the complexity of manipulated models, but also, to the important gap between requirement models manipulated by different stackholders and formal models required by existing verification tools. This dissertation aims therefore to develop a methodology that define activities that fill this gap by generating formal artifacts from textual requirements and existing design models. Our approach is based on previous work on the exploitation of contexts for formal verification, particularly, CDL language. We extended UML use cases with the ability to precisely describe interaction scenarios between the system under validation and its context. We also defined a requirement specification language based on the processing of natural language to formalize textual requirements. This formalization is performed thanks to model transformations that generate CDL properties from textual requirements and CDL context models form extended use cases scenarios. The proposed methodology is instantiated on a reel industrial case study provided by our industrial partner., En dépit de l'efficacité des méthodes formelles, en particulier les techniques d'analyse de modèles (model checking), à identifier les violations des exigences dans les modèles de conception, leur utilisation au sein des processus de développement industriel demeure limitée. Ceci est dû principalement à la complexité des modèles manipulés au cours de ces processus (explosion combinatoire) et à la difficulté de produire des représentations formelles afin d'exploiter les outils de vérification existants. Fort de ce constat, mes travaux de thèse contribuent au développement d'un volet méthodologique définissant les activités conduisant à l'obtention des artefacts formels. Ceux-ci sont générés directement à partir des exigences et des modèles de conception manipulés par les ingénieurs dans leurs activités de modélisation. Nos propositions s'appuient sur les travaux d'exploitation des contextes pour réduire la complexité de la vérification formelle, en particulier le langage CDL. Pour cela, nous avons proposé une extension des cas d'utilisation, afin de permettre la description des scénarios d'interaction entre le système et son environnement directement dans le corps des cas d'utilisation. Aussi, nous avons proposé un langage de spécification des exigences basé sur le langage naturel contrôlé pour la formalisation des exigences. Cette formalisation est opérée par transformations de modèle générant des propriétés CDL formalisées directement des exigences textuelles des cahiers des charges ainsi que les contextes CDL à partir des cas d'utilisations étendus. L'approche proposée a été instanciée sur un cas d'étude industriel de taille et de complexité réelles développées par notre partenaire industriel.

National audience; De nombreux secteurs utilisent des systèmes et des logiciels critiques, dont les défaillances pourraient entraîner des pertes de vies humaines. Cet article s’intéresse au développement et à la certification des logiciels critiques, avec une illustration dans le domaine de l’aéronautique. Il souligne les difficultés rencontrées en entreprise et l’état des pratiques pour mettre en perspective quelques pistes d’améliorations possibles de celles-ci. Il démontre notamment l’intérêt d’intégrer plus étroitement et de façon continue les contraintes de la certification au processus de développement des logiciels. Notre proposition est de nous inspirer des valeurs agiles pour répondre le plus tôt possible aux exigences de certification applicables au développement des logiciels. C’est ce que nous appelons la certification continue.