Nous proposons dans cette thèse les approches de test pour la composition de services web. Nous nous intéressons aux test unitaire et d’intégration d’une orchestration de services web. L’aspect de vérification d’exécution en-ligne est aussi consideré. Nous définissons une plateforme de test unitaire pour l’orchestration de services web qui compose une architecture de test, une relation de conformité et deux approches de test basés sur le modèle de machine à l’états finis étendues temporisés: l’approche offline où les activités de test comme la génération de cas de test temporisé, l’exécution de test et l’assignement de verdict sont appliquées en séquentielle tandis que ces activités sont appliquées en parallèle dans l’approche online. Pour le test d’intégration d’une orchestration, nous combinons deux approches: active et passive.Au debut, l’approche active est utilisée pour activer une nouvelle session d’orchestration par l’envoi d’un message de requête SOAP. Après, tous les messages d’entré et de sortie de l’orchestration sont collectés et analysés par l’approche passive.Pour l’aspect de vérification d’exécution en-ligne, nous nous intéressons à la vérification d’une trace qui respecte un ensemble des constraintes, noté règles, ou pas. Nous avons proposé extendre le langage Nomad en définissant des constraintes sur chaque action atomique et un ensemble de corrélation de données entre les actions pour définir des règles pour le service web. Ce langage nous permet de définir des règles avec le temps futur et passé, et d’utiliser des opérations NOT, AND, OR pour combiner quelque conditions dans le contexte de la règle. Ensuite, nous proposons un algorithme pour vérifier l’exactitude d’une séquence des messages en parallèle avec le moteur de collecte de trace. / In this thesis, we propose the testing approaches for web service composition. We focus on unit, integrated testing of an orchestration of web services and also the runtime verification aspect. We defined an unit testing framework for an orchestration that is composed of a test architecture, a conformance relation and two proposed testing approaches based on Timed Extended Finite State Machine (TEFSM) model: offline which test activities as timed test case generation, test execution and verdict assignment are applied in sequential, and online which test activities are applied in parallel. For integrated testing of an orchestration, we combines of two approaches: active and passive. Firstly, active approach is used to start a new session of the orchestration by sending a SOAP request. Then all communicating messages among services are collected and analyzed by a passive approach. On the runtime verification aspect, we are interested in the correctness of an execution trace with a set of defined constraints, called rules. We have proposed to extend the Nomad language, by defining the constraints on each atomic action (fixed conditions) and a set of data correlations between the actions to define the rules for web services. This language allows us to define a rule with future and past time, and to use the operations: NOT, AND, OR to combines some conditions into a context of the rule. Afterwards, we proposed an algorithm to check correctness of a message sequence in parallel with the trace collection engine. Specifically, this algorithm verifies message by message without storing them.

A Arquitetura Orientada a Serviços (SOA) é um estilo arquitetural formado por um conjunto de restrições que visa promover a escalabilidade e a flexibilidade de um sistema, provendo suas funcionalidades como serviços. Nos últimos anos, um estilo alternativo foi proposto e amplamente adotado, que projeta as funcionalidades de um sistema como recursos. Este estilo arquitetural orientado a recursos é chamado de REST. O teste de serviços web em geral apresenta vários desafios devido a sua natureza distribuída, canal de comunicação pouco confiável, baixo acoplamento e a falta de uma interface de usuário. O teste de serviços RESTful (serviços que utilizam o REST) compartilham estes mesmos desafios e ainda necessitam que suas restrições sejam obedecidas. Estes desafios demandam testes mais sistemáticos e formais. Neste contexto, o teste baseado em modelos (TBM) se apresenta como um processo viável para abordar essas necessidades. O modelo que representa o sistema deve ser simples e ao mesmo tempo preciso para que sejam gerados casos de teste com qualidade. Com base nesse contexto, este projeto de mestrado propõe uma abordagem baseada em modelos para testar serviços RESTful. O modelo comportamental adotado foi a máquina de estados de protocolos UML, capaz de formalizar a interface do serviço enquanto esconde o seu funcionamento interno. Uma ferramenta foi desenvolvida para gerar automaticamente os casos de teste usando critérios de cobertura de estados e transições para percorrer o modelo / Service Oriented Architecture (SOA) is an architectural style consisting of a set of restrictions aimed at promoting the scalability and flexibility of a system, providing its functionalities as services. In recent years, an alternative style was proposed and widely adopted, which designs the system\'s functionalities as resources. This resource oriented architectural style is called REST. In general, the test of web services has several challenges due to its distributed nature, unreliable communication channel, low coupling and the lack of a user interface. Testing RESTful web services (services that use REST) share these same challenges and also need to obey the REST constraints. These challenges require a more systematic and formal testing approach. In this context, model based testing presents itself as a viable process for addressing those needs. The model that represents the system should be simple and precise enough to generate quality test cases. Based on this context, this work proposes a model based approach to test RESTful web services. The behavioral model used was the UML protocol state machine, which is capable to provide a formalization of the service interface, while hiding its internal behaviour. A tool was developed to automatically generate test cases using the state and transition coverage criteria to traverse the model

O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans. / Model-Based Testing (MBT) has emerged as a promising strategy for the minimization of problems related to time and resource limitations in software testing and aims at checking whether the implementation under test is in compliance with its specification. Test cases are automatically generated from behavioral models produced during the software development life cycle. Among the existing modeling techniques, Input/Output Transition Systems (IOTSs) have been widely used in MBT because they are more expressive than Finite State Machines (FSMs). Despite the existence of test generation methods for IOTSs, the problem of selection of test cases is an important and difficult topic. The current methods for IOTSs are non-deterministic, in contrast to the existing theory for FSMs that provides complete fault coverage guarantee based on a fault model. This manuscript addresses the application of fault models to deterministic test generation methods from IOTSs. A method for the test suite generation based on W method for FSMs is proposed for IOTSs. It generates test suites in a deterministic way and also satisfies sufficient conditions of specification coverage and all faults in a given fault domain. Empirical studies evaluated its applicability and effectiveness. Experimental results for the analyses of the cost of test suite generation by random IOTSs and a case study with specifications from the industry show the effectiveness of the test suites generated in relation to the traditional method of Tretmans.

The importance and requirements of certifying safety critical software is today more apparent than ever. This study focuses on the standards and practices used within the avionics, automotive and medical domain when it comes to safety critical software. We identify critical problems and trends when certifying safety critical software and propose a proof-of-concept using static analysis, model checking and incremental SAT solving as a contribution towards solving the identified problems. We present quantitative execution times and code coverage results of our proposed solution. The proposed solution is developed under the assumptions of safety critical software standards and compared to other studies proposing similar methods. Lastly, we conclude the issues and advantages of our proof-of-concept in perspective of the software developer community

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.

A Arquitetura Orientada a Serviços (SOA) é um estilo arquitetural formado por um conjunto de restrições que visa promover a escalabilidade e a flexibilidade de um sistema, provendo suas funcionalidades como serviços. Nos últimos anos, um estilo alternativo foi proposto e amplamente adotado, que projeta as funcionalidades de um sistema como recursos. Este estilo arquitetural orientado a recursos é chamado de REST. O teste de serviços web em geral apresenta vários desafios devido a sua natureza distribuída, canal de comunicação pouco confiável, baixo acoplamento e a falta de uma interface de usuário. O teste de serviços RESTful (serviços que utilizam o REST) compartilham estes mesmos desafios e ainda necessitam que suas restrições sejam obedecidas. Estes desafios demandam testes mais sistemáticos e formais. Neste contexto, o teste baseado em modelos (TBM) se apresenta como um processo viável para abordar essas necessidades. O modelo que representa o sistema deve ser simples e ao mesmo tempo preciso para que sejam gerados casos de teste com qualidade. Com base nesse contexto, este projeto de mestrado propõe uma abordagem baseada em modelos para testar serviços RESTful. O modelo comportamental adotado foi a máquina de estados de protocolos UML, capaz de formalizar a interface do serviço enquanto esconde o seu funcionamento interno. Uma ferramenta foi desenvolvida para gerar automaticamente os casos de teste usando critérios de cobertura de estados e transições para percorrer o modelo / Service Oriented Architecture (SOA) is an architectural style consisting of a set of restrictions aimed at promoting the scalability and flexibility of a system, providing its functionalities as services. In recent years, an alternative style was proposed and widely adopted, which designs the system\'s functionalities as resources. This resource oriented architectural style is called REST. In general, the test of web services has several challenges due to its distributed nature, unreliable communication channel, low coupling and the lack of a user interface. Testing RESTful web services (services that use REST) share these same challenges and also need to obey the REST constraints. These challenges require a more systematic and formal testing approach. In this context, model based testing presents itself as a viable process for addressing those needs. The model that represents the system should be simple and precise enough to generate quality test cases. Based on this context, this work proposes a model based approach to test RESTful web services. The behavioral model used was the UML protocol state machine, which is capable to provide a formalization of the service interface, while hiding its internal behaviour. A tool was developed to automatically generate test cases using the state and transition coverage criteria to traverse the model

L’acceptation et l’utilisation des services Web en industrie se développent de par leursupport au développement d’application distribuées comme compositions d’entitéslogicielles plus simples appelées services. En complément à la vérification, le testpermet de vérifier la correction d’une implémentation binaire (code source nondisponible) par rapport à une spécification. Dans cette thèse, nous proposons uneapproche boîte-noire du test de conformité de compositions de services centralisées(orchestrations). Par rapport à l’état de l’art, nous développons une approchesymbolique de façon à éviter des problèmes d’explosion d’espace d’état dus à la largeutilisation de données XML dans les services Web. Cette approche est basée sur desmodèles symboliques (STS), l’exécution symbolique de ces modèles et l’utilisationd’un solveur SMT. De plus, nous proposons une approche de bout en bout, quiva de la spécification à l’aide d’un langage normalisé d’orchestration (ABPEL) etde la possible description d’objectifs de tests à la concrétisation et l’exécution enligne de cas de tests symboliques. Un point important est notre transformation demodèle entre ABPEL et les STS qui prend en compte les spécifications sémantiquesd’ABPEL. L’automatisation de notre approche est supportée par un ensemble d’outilsque nous avons développés. / Web services are gaining industry-wide acceptance and usage by fostering the developmentof distributed applications out of the composition of simpler entities calledservices. In complement to verification, testing allows one to check for the correctnessof a binary (no source code) service implementation with reference to a specification.In this thesis, we propose black box conformance testing approach for centralizedservice compositions (orchestrations). With reference to the state of the art, wedevelop a symbolic approach in order to avoid state space explosion issues due to theXML data being largely used in Web services. This approach is based on symbolicmodels (STS), symbolic execution, and the use of a satisfiability modulo theory(SMT) solver. Further, we propose a comprehensive end-to-end approach that goesfrom specification using a standard orchestration language (ABPEL), and the possibledescription of test purposes, to the online realization and execution of symbolic testcases against an implementation. A crucial point is a model transformation fromABPEL to STS that we have defined and that takes into account the peculiarities ofABPEL semantics. The automation of our approach is supported by a tool-chainthat we have developed.

O Teste Baseado em Modelos (TBM) emergiu como uma estratégia promissora para minimizar problemas relacionados à falta de tempo e recursos em teste de software e visa verificar se a implementação sob teste está em conformidade com sua especificação. Casos de teste são gerados automaticamente a partir de modelos comportamentais produzidos durante o ciclo de desenvolvimento de software. Entre as técnicas de modelagem existentes, Sistemas de Transição com Entrada/Saída (do inglês, Input/Output Transition Systems - IOTSs), são modelos amplamente utilizados no TBM por serem mais expressivos do que Máquinas de Estado Finito (MEFs). Apesar dos métodos existentes para geração de testes a partir de IOTSs, o problema da seleção de casos de testes é um tópico difícil e importante. Os métodos existentes para IOTS são não-determinísticos, ao contrário da teoria existente para MEFs, que fornece garantia de cobertura completa com base em um modelo de defeitos. Esta tese investiga a aplicação de modelos de defeitos em métodos determinísticos de geração de testes a partir de IOTSs. Foi proposto um método para geração de conjuntos de teste com base no método W para MEFs. O método gera conjuntos de teste de forma determinística além de satisfazer condições de suficiência de cobertura da especificação e de todos os defeitos do domínio de defeitos definido. Estudos empíricos avaliaram a aplicabilidade e eficácia do método proposto: resultados experimentais para analisar o custo de geração de conjuntos de teste utilizando IOTSs gerados aleatoriamente e um estudo de caso com especificações da indústria mostram a efetividade dos conjuntos gerados em relação ao método tradicional de Tretmans. / Model-Based Testing (MBT) has emerged as a promising strategy for the minimization of problems related to time and resource limitations in software testing and aims at checking whether the implementation under test is in compliance with its specification. Test cases are automatically generated from behavioral models produced during the software development life cycle. Among the existing modeling techniques, Input/Output Transition Systems (IOTSs) have been widely used in MBT because they are more expressive than Finite State Machines (FSMs). Despite the existence of test generation methods for IOTSs, the problem of selection of test cases is an important and difficult topic. The current methods for IOTSs are non-deterministic, in contrast to the existing theory for FSMs that provides complete fault coverage guarantee based on a fault model. This manuscript addresses the application of fault models to deterministic test generation methods from IOTSs. A method for the test suite generation based on W method for FSMs is proposed for IOTSs. It generates test suites in a deterministic way and also satisfies sufficient conditions of specification coverage and all faults in a given fault domain. Empirical studies evaluated its applicability and effectiveness. Experimental results for the analyses of the cost of test suite generation by random IOTSs and a case study with specifications from the industry show the effectiveness of the test suites generated in relation to the traditional method of Tretmans.

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.

A modern truck contains a large number of functionalities implemented in its electronics system. Thus, testing all of these functions employs a considerable effort. The execution of tests against the system has been automated for a long time. Unfortunately, most of the test is still designed manually these days. This manual test design is sometimes not comprehensive enough to cover all possible scenarios within a complex system. At the moment, there is also a growing trend in the development process based on the model. Furthermore, model-based software can handle events and signal behaviour more robustly[1]. This thesis investigates the technique in model-based testing. The study evaluates the requirement modelling and automated abstract test generation of model-based testing over the existing testing method. A cause-effect graph is utilized for the modelling in Matlab Simulink tool with DesignVerifier feature. The case study is the truck dosing system in Scania. The results are the following. The temporal and static requirements modelling are capable of being modelled using the cause-effect graph in Matlab Simulink. Compared to the traditional method, the MBT method can achieve higher requirement coverage and more rigorous test with optimized test case generation. The MBT method also has a rapid test case generation time suitable for quick design iteration. However, the total test development time (including test case generation time) of using MBT is 12.5% higher than the manual method. Using a model-based platform like Matlab Simulink is recommended to assist the manual testing, not to replace the test flow entirely with the current research state. / En modern truck innehåller ett stort antal funktioner implementerade i dess elektroniksystem. Att testa alla dessa funktioner kräver därför en avsevärd ansträngning. Utförandet av tester mot systemet har varit automatiserat under lång tid. Tyvärr är det mesta av testet fortfarande utformat manuellt nu för tiden. Denna manuella testdesign är ibland inte tillräckligt omfattande för att täcka alla möjliga scenarier inom ett komplext system. För tillfället finns det också en växande trend i utvecklingsprocessen utifrån modellen. Dessutom kan modellbaserad programvara hantera händelser och signalbeteende mer robust[1]. Detta examensarbete undersöker tekniken i modellbaserad testning. Studien utvärderar kravmodellering och automatiserad abstrakt testgenerering av modellbaserad testning över den befintliga testmetoden. En cause-effect graph används för modelleringen i Matlab Simulink-verktyget med Design Verifier-funktionen. Fallstudien är lastbilens doseringssystem i Scania. Resultaten är följande. Den tidsmässiga och statiska kravmodelleringen kan modelleras med hjälp av cause-effect graph i Matlab Simulink. Jämfört med den traditionella metoden kan MBT-metoden uppnå högre kravtäckning och mer rigorösa test med optimerad testfallsgenerering. MBT-metoden har också en snabb genereringstid för testfall som är lämplig för snabb designiteration. Den totala testutvecklingstiden (inklusive genereringstid för testfall) för att använda MBT är 12,5% högre än den manuella metoden. Att använda en modellbaserad plattform som Matlab Simulink rekommenderas för att underlätta den manuella testningen, inte för att ersätta testflödet helt med det aktuella forskningsläget.