Orientador: Arnaldo Vieira Moura / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-15T05:28:23Z (GMT). No. of bitstreams: 1 Bonifacio_AdilsonLuiz_D.pdf: 1228504 bytes, checksum: 62db4b0286cfd1c735336e429629b3de (MD5) Previous issue date: 2009 / Resumo: O objetivo deste trabalho é prover métodos eficientes de geração de casos de teste para sistemas reativos críticos. Sistemas dessa natureza compreendem sistemas de tempo real e com transformações de contexto. Uma das técnicas mais usadas na geração de conjuntos de teste tem sido a abordagem baseada em modelos formais. Neste caso, os formalismos fornecem uma base sólida para que a atividade de teste seja efetuada de forma precisa e segura. Este trabalho propõe a construção de modelos formais, métodos e técnicas, bem como estratégias de teste, para dar suporte ao processo de geração automática de conjuntos de teste, aplicáveis a sistemas complexos. Porém, o processo de geração de testes baseado em modelos se torna, muitas vezes, impraticável em aplicações reais, devido ao problema da explosão combinatória de estados. Daí a necessidade de se encontrar modelos adequados que capturem o comportamento desejado dos sistemas a serem testados, bem como a importância de se construir métodos que contornem o problema da explosão do espaço de estado, de maneira razoável, permitindo que a geração de testes seja um processo aplicável a sistemas complexos. Entre os modelos abordados neste trabalho estão: (i) as tradicionais Máquinas de Estados Finito (FSM); (ii) uma extensão das FSMusando variáveis de contexto, as Máquinas de Estados Finito Estendida (EFSM); (iii) a extensão temporizada de EFSM (TEFSM), que possui, não apenas variáveis de contexto, mas também variáveis relógio; (iv) os modelos temporizados com entradas e saídas independentes, conhecidos como Timed I/O Automata (TIOA); e (v) uma extensão proposta para TIOA, denominado Timed I/O Context Automata (TIOCA), para compreender a evolução contínua de tempo e também as transformações de contexto. Com relação a geração de testes baseada em tais modelos, foi proposto, primeiramente, uma técnica de derivação de sequências de confirmação para TEFSM, usando model-checking. Em seguida, foi proposta uma generalização para um método de geração de conjuntos completos de teste usando FSM. Também foi desenvolvido um novo método de discretização do modelo TIOA, provendo a base necessária para a geração de casos de teste usando os conceitos de proposta de teste e produto síncrono. Por fim, foi desenvolvida uma extensão do método de discretização para TIOA também proposto neste trabalho, aplicado ao modelo TIOCA, permitindo a geração de testes em sistemas com evolução contínua de tempo e fluxo de dados, usando os conceitos de proposta de teste e produto de TIOCA / Abstract: This work aims to provide efficient test case generation methods for reactive and critical systems. In general, reactive and critical systems are real-time systems with context transformations. One of the most promising techniques for generating test suites is model-based testing. The formalisms supply the basis to perform a precise and dependable testing activity. In this scenery, our work proposes a construction of formal models, methods and techniques, as well as testing strategies, to support the process of automatically generating test suites for complex systems. However, the test generation process using formal models is usually infeasible in real applications, due to the state space explosion. Therefore, we need to find out suitable models to capture the system behaviors, and also to construct methods that can overcome the explosion problem, in a reasonable way, allowing the generation of test suites for complex systems. In this work we treat the following formal models: the conventional FSM; an extension of FSM using context variables (EFSM); the proposed extension of EFSM (TEFSM) to capture context variables and also clock variables; timed models, with disassociated input and output actions, called TIOA; and the proposed extension for TIOA, so-called TIOCA, to capture continuous time evolution and context transformations. In a first step of this work we proposed a technique to derive confirming sequences for TEFSM, using model-checking. Next, a classical method to generate complete test suites was generalized for FSM.We also proposed a new discretizationmethod for TIOA models, allowing the test case generation using test purpose and the synchronous product. Lastly, we extended the discretization method for TIOA to obtain more compact grid automata for TIOCA models, allowing the test case generation for systems with continuous time evolution and data flow transformations, using the notion of test purpose and the product of TIOCA / Doutorado / Teoria da Computação e Teste de Sistemas / Doutor em Ciência da Computação

Orientador: Eliane Martins / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-24T16:35:59Z (GMT). No. of bitstreams: 1 Letizio_CarolineCastello_M.pdf: 1670478 bytes, checksum: c2f330cd004addd705aef75384effcd2 (MD5) Previous issue date: 2013 / Resumo: Teste baseado em modelo é uma técnica na qual um sistema é modelado e geram-se testes a partir do modelo. Esta técnica apresenta como uma das maiores dificuldades a modelagem do sistema. Alguns dos empecilhos encontrados ao modelar são o que considerar do sistema e como representar essas considerações no modelo, incluindo em aplicações Web. Sendo assim, este trabalho propõe um método para auxiliar na modelagem de aplicações Web. Esta escolha é motivada pelo fato que esse tipo de sistema tem sido cada vez mais utilizado nos últimos anos e, com a sua evolução, sua complexidade tem aumentado consideravelmente, devido à dinamicidade e interatividade que esse tipo de aplicação oferece. A abordagem proposta é baseada em trabalhos correlatos, para se saber o que modelar da aplicação Web e como criar o modelo, descrevendo-se o passo-a-passo para se gerar os testes a partir dos modelos desenvolvidos e aplicá-los no sistema. A abordagem deste trabalho sugere tanto formas manuais como automáticas para os testes baseados em modelos. O método foi proposto para testar uma aplicação real: o ambiente de ensino à distância TelEduc. Os resultados, obtidos a partir da aplicação da proposta deste trabalho por um analista de teste e pela própria equipe do TelEduc, são analisados, a fim de validar a proposta e auxiliar no processo de desenvolvimento e aplicação dos testes de equipes de qualidade de software, principalmente, daquelas que não possuem nenhuma forma de organização de testes / Abstract: Model based testing is a technique in which the system is modeled and, from this model, tests can be generated. The major difficulty about this technique is to generate the model, since it is problematic to define what should be considered from the system and insert these characteristics into the model. This technique is also used in Web applications which presents the same challenges. Therefore, the present work proposes a method to assist in the modeling of Web applications. This sort of system has been increasingly used in recent years, where the system¿s complexity has considerably grown due to the dynamic and interactivity that this kind of application offers. The proposed method is based on related works in order to know what to model from the applications and how to create this model. The method contains the steps to generate tests cases from the created model, and how to execute them in the system. This work also suggests manual and automatic ways to execute the method. The proposal has been applied to test a real application: the e-learning Web environment TelEduc. The results obtained from the method¿s application by a test analyst and by the TelEduc team, are here analyzed to validate the method and to assist in the process development and tests execution by quality teams, especially those teams where there are no means of tests organization. / Mestrado / Ciência da Computação / Mestra em Ciência da Computação

Software testing is considered as one of the key phases in the software-development life cycle (SDLC). The main objective of software testing is to detect the faults either through manual testing or with automated testing approach. The most commonly adopted software testing approach in industries is test case based testing (TCBT) which is usually done manually. TCBT is mainly used by the software testers to formalize and guide their testing activities and set theoretical principals for testing. On the other hand, model based testing (MBT) is widely used automation software testing technique to generate and execute the tests. Both techniques are showing their prominence in real time with some pros and cons. However, there is no formal comparison available between these two techniques. The main objective of this thesis work is to find out the difference in test cases in TCBT and MBT in terms of providing better test coverage ( Statement, Branch and Path), requirement traceability, cost and time. To fulfill the aims of the research we have conducted interviews for static validation, and later we did an experiment for validating those results dynamically. The analysis of experiment results showed that the requirement traceability in MBT generated test cases are very hard to make the test cases traceable to the requirements, particularly with the open-source tool Model J-Unit. However, this can be done by using other commercial tools like Microsoft Spec Explorer or Conformiq Qtronic. Furthermore, we found by conducting experiment, that MBT consumes less time thus it is cost-effective as compared to TCBT and also MBT show better test coverage than TCBT. Moreover, we found that, in our case, requirement traceability is better in traditional TCBT approach as compared to MBT. / +4746851975

Les systèmes multi-agents (SMA) peuvent être utilisé pour modéliser les phénomènes qui peuvent être décomposés en agents qui interagissent et qui existent au sein d'un environnement. Ils peuvent être utilisés pour modéliser les sociétés humaines et animales, aux fins de l'analyse de leurs propriétés par des moyens de calcul. Cette thèse est consacrée à l'analyse automatisée d'un type particulier de ces modèles sociaux, celles qui sont fondées sur les principes comportementalistes, qui contrastent avec les approches cognitives plus dominantes dans la littérature des SMAs. La caractéristique des théories comportementalistes est l'accent mis sur la définition des comportements basée sur l'interaction entre les agents et leur environnement. Non seulement des actions réflexives, mais aussi d'apprentissage, les motivations, et les émotions peuvent être définies. Nous introduisons une architecture formelle d'agent basée sur la théorie d'analyse comportementale de B. F. Skinner, ainsi que une notion appropriée et formelle de l'environnement pour mettre ces agents ensemble dans un SMA. La simulation est souvent utilisée pour analyser les SMAs. Les techniques consistent généralement à simuler le SMA plusieurs fois, soit pour recueillir des statistiques, soit pour voir ce qui se passe à travers l'animation. Toutefois, les simulations peuvent être utilisées d'une manière plus orientée vers la vérification si on considère qu'elles sont en réalité des explorations de grandes espaces d'états. Nous proposons une technique de vérification nouvelle basé sur cette idée, qui consiste à simuler un SMA de manière guidée, afin de vérifier si quelques hypothèses sur lui sont confirmées ou non. À cette fin, nous tirons profit de la position privilégiée que les environnements sont dans les SMAs de cette thèse: la spécification formelle de l'environnement d'un SMA sert à calculer les évolutions possibles du SMA comme un système de transition, établissant ainsi l'espace d'états à vérifier. Dans ce calcul, les agents sont pris en compte en les simulant afin de déterminer, à chaque état de l'environnement, quelles sont leurs actions. Chaque exécution de la simulation est une séquence d'états dans cet espace d'états, qui est calculée à la volée, au fur et à mesure que la simulation progresse. L'hypothèse à étudier, à son tour, est donnée comme un autre système de transition, appelé objectif de simulation, qui définit les simulations désirables et indésirables. Il est alors possible de vérifier si le SMA est conforme à l'objectif de simulation selon un certain nombre de notions de satisfiabilité très précises. Algorithmiquement, cela correspond à la construction d'un produit synchrone de ces deux systèmes de transitions (i.e., celui du SMA et l'objectif de simulation) à la volée et à l'utiliser pour faire fonctionner un simulateur. C'est-à-dire, l'objectif de simulation est utilisé pour guider le simulateur, de sorte que seuls les états concernés sont en réalité simulés. À la fin d'un tel algorithme, il délivre un verdict concluant ou non concluant. Si c'est concluant, il est connu que le SMA est conforme à l'objectif de simulation par rapport aux observations qui ont été faites lors des simulations. Si c'est non-concluant, il est possible d'effectuer quelques ajustements et essayer à nouveau. En résumé, dans cette thèse nous fournissons quatre nouveaux éléments: (i) une architecture d'agent; (ii) une spécification formelle de l'environnement de ces agents, afin qu'ils puissent être composés comme un SMA; (iii) une structure pour décrire les propriétés d'intérêt, que nous avons nommée objectif de simulation, et (iv) une technique pour l'analyse formelle du SMA résultant par rapport à un objectif de simulation. Ces éléments sont mis en œuvre dans un outil, appelé Simulateur Formellement Guidé (FGS, de l'anglais Formally Guided Simulator).Des études de cas exécutables dans FGS sont fournies pour illustrer l'approche. / Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely reflexive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as a MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., "every time the agent does X, it will do Y later"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS's and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose w.r.t. the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again.In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into a MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach.

L'ingénierie des lignes de produits est une approche utilisée pour développer une famille de produits. Ces produits partagent un ensemble de points communs et un ensemble de points de variation. Aujourd'hui, la validation est une activité disjointe du processus de développement des lignes de produits. L'effort et les moyens fournis dans les campagnes de tests de chaque produit peuvent être optimisés dans un contexte plus global au niveau de la ligne de produits. Le model-based testing est une technique de génération automatique des cas de test à partir d'un modèle d'états et de transitions construit à partir des exigences fonctionnelles. Dans cette thèse, nous présentons une approche pour tester une ligne de produits logiciels avec le model-based testing. La première contribution consiste à établir un lien entre le modèle de variabilité et le modèle de test, à l'aide des exigences fonctionnelles. La deuxième contribution est un algorithme qui extrait automatiquement un modèle de test spécifique à un produit membre de la famille de produits sous test. L'approche est illustrée par une famille de produits de tableaux de bord d'automobiles et expérimentée par un industriel du domaine aéronautique dans le cadre du projet Européen MBAT. / Software product line engineering is an approach that supports developing products in family. These products are described by common and variable features. Currently, the validation activity is disjointed from the product lines development process. The effort and resources provided in the test campaigns for each product can be optimized in the context of product lines. Model-based testing is a technique for automatically generating a suite of test cases from requirements. In this thesis report, we present an approach to test a software product line with model-based testing. This technique is based on an algorithm that establishes the relationship between the variability model released with OVM and the test model, using traceability of functional requirements present in both formalisms. Our contribution is an algorithm that automatically extracts a product test model. It is illustrated with a real industrial case of automotive dashboards and experimented by an industrial of aeronautic domain in the MBAT European project context.

Access Control (AC) is a major pillar in software security. In short, AC ensures that only intended users can access resources and only the required access to accomplish some task will be given. In this context, Role Based Access Control (RBAC) has been established as one of the most important paradigms of access control. In an organization, users receive responsibilities and privileges through roles and, in AC systems implementing RBAC, permissions are granted through roles assigned to users. Despite the apparent simplicity, mistakes can occur during the development of RBAC systems and lead to faults or either security breaches. Therefore, a careful verification and validation process becomes necessary. Access control testing aims at showing divergences between the actual and the intended behavior of access control mechanisms. Model Based Testing (MBT) is a variant of testing that relies on explicit models, such as Finite State Machines (FSM), for automatizing test generation. MBT has been successfully used for testing functional requirements; however, there is still lacking investigations on testing non-functional requirements, such as access control, specially in test criteria. In this Master Dissertation, two aspects of MBT of RBAC were investigated: FSM-based testing methods on RBAC; and Test prioritization in the domain of RBAC. At first, one recent (SPY) and two traditional (W and HSI) FSM-based testing methods were compared on RBAC policies specified as FSM models. The characteristics (number of resets, average test case length and test suite length) and the effectiveness of test suites generated from the W, HSI and SPY methods to five different RBAC policies were analyzed at an experiment. Later, three test prioritization methods were compared using the test suites generated in the previous investigation. A prioritization criteria based on RBAC similarity was introduced and compared to random prioritization and simple similarity. The obtained results pointed out that the SPY method outperformed W and HSI methods on RBAC domain. The RBAC similarity also achieved an Average Percentage Faults Detected (APFD) higher than the other approaches. / Controle de Acesso (CA) é um dos principais pilares da segurança da informação. Em resumo, CA permite assegurar que somente usuários habilitados terão acesso aos recursos de um sistema, e somente o acesso necessário para a realização de uma dada tarefa será disponibilizado. Neste contexto, o controle de acesso baseado em papel (do inglês, Role Based Access Control - RBAC) tem se estabelecido como um dos mais importante paradigmas de controle de acesso. Em uma organização, usuários recebem responsabilidades por meio de cargos e papéis que eles exercem e, em sistemas RBAC, permissões são distribuídas por meio de papéis atribuídos aos usuários. Apesar da aparente simplicidade, enganos podem ocorrer no desenvolvimento de sistemas RBAC e gerar falhas ou até mesmo brechas de segurança. Dessa forma, processos de verificação e validação tornam-se necessários. Teste de CA visa identificar divergências entre a especificação e o comportamento apresentado por um mecanismo de CA. Teste Baseado em Modelos (TBM) é uma variante de teste de software que se baseia em modelos explícitos de especificação para automatizar a geração de casos testes. TBM tem sido aplicado com sucesso no teste funcional, entretanto, ainda existem lacunas de pesquisa no TBM de requisitos não funcionais, tais como controle de acesso, especialmente de critérios de teste. Nesta dissertação de mestrado, dois aspectos do TBM de RBAC são investigados: métodos de geração de teste baseados em Máquinas de Estados Finitos (MEF) para RBAC; e priorização de testes para RBAC. Inicialmente, dois métodos tradicionais de geração de teste, W e HSI, foram comparados ao método de teste mais recente, SPY, em um experimento usando políticas RBAC especificadas como MEFs. As características (número de resets, comprimento médio dos casos de teste e comprimento do conjunto de teste) e a efetividade dos conjuntos de teste gerados por cada método para cinco políticas RBAC foram analisadas. Posteriormente, três métodos de priorização de testes foram comparados usando os conjuntos de teste gerados no experimento anterior. Neste caso, um critério baseado em similaridade RBAC foi proposto e comparado com a priorização aleatória e baseada em similaridade simples. Os resultados obtidos mostraram que o método SPY conseguiu superar os métodos W e HSI no teste de sistemas RBAC. A similaridade RBAC também alcançou uma detecção de defeitos superior.

Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they can be used to model human and animal societies, for the purpose of analysing their properties by computational means. This thesis is concerned with the automated analysis of a particular kind of such social models, namely, those based on behaviourist principles, which contrasts with the more dominant cognitive approaches found in the MAS literature. The hallmark of behaviourist theories is the emphasis on the definition of behaviour in terms of the interaction between agents and their environment. In this manner, not merely re exive actions, but also learning, drives, and emotions can be defined. More specifically, in this thesis we introduce a formal agent architecture (specified with the Z Notation) based on the Behaviour Analysis theory of B. F. Skinner, and provide a suitable formal notion of environment (based on the pi-calculus process algebra) to bring such agents together as an MAS. Simulation is often used to analyse MASs. The techniques involved typically consist in implementing and then simulating a MAS several times to either collect statistics or see what happens through animation. However, simulations can be used in a more verification-oriented manner if one considers that they are actually explorations of large state-spaces. In this thesis we propose a novel verification technique based on this insight, which consists in simulating a MAS in a guided way in order to check whether some hypothesis about it holds or not. To this end, we leverage the prominent position that environments have in the MASs of this thesis: the formal specification of the environment of a MAS serves to compute the possible evolutions of the MAS as a transition system, thereby establishing the state-space to be investigated. In this computation, agents are taken into account by being simulated in order to determine, at each environmental state, what their actions are. Each simulation execution is a sequence of states in this state-space, which is computed on-the-fly, as the simulation progresses. The hypothesis to be investigated, in turn, is given as another transition system, called a simulation purpose, which defines the desirable and undesirable simulations (e.g., \"every time the agent does X, it will do Y later\"). It is then possible to check whether the MAS satisfies the simulation purpose according to a number of precisely defined notions of satisfiability. Algorithmically, this corresponds to building a synchronous product of these two transitions systems (i.e., the MAS\'s and the simulation purpose) on-the-fly and using it to operate a simulator. That is to say, the simulation purpose is used to guide the simulator, so that only the relevant states are actually simulated. By the end of such an algorithm, it delivers either a conclusive or an inconclusive verdict. If conclusive, it becomes known whether the MAS satisfies the simulation purpose with respect to the observations made during simulations. If inconclusive, it is possible to perform some adjustments and try again. In summary, then, in this thesis we provide four novel elements: (i) an agent architecture; (ii) a formal specification of the environment of these agents, so that they can be composed into an MAS; (iii) a structure to describe the property of interest, which we named simulation purpose; and (iv) a technique to formally analyse the resulting MAS with respect to a simulation purpose. These elements are implemented in a tool, called Formally Guided Simulator (FGS). Case studies executable in FGS are provided to illustrate the approach. / Sistemas multi-agentes (SMAs) podem ser usados para modelar fenômenos que podem ser decompostos em diversos agentes que interagem entre si dentro de um ambiente. Em particular, eles podem ser usados para modelar sociedades humanas e animais, com a finalidade de se analisar as suas propriedades computacionalmente. Esta tese trata da análise automatizada de um tipo particular de tais modelos sociais, a saber, aqueles baseados em princípios behavioristas, o que contrasta com as abordagens cognitivas mais dominante na literatura de SMAs. A principal característica das teorias behaviorista é a ênfase na descrição do comportamento em termos da interação entre agentes e seu ambiente. Desta forma, não apenas ações refl exivas, mas também de aprendizado, motivações, e as emoções podem ser definidas. Mais especificamente, nesta tese apresentamos uma arquitetura de agentes formal (especificada através da Notação Z) baseada na teoria da Análise do Comportamento de B. F. Skinner, e fornecemos uma noção adequada e formal de ambiente (com base na álgebra de processos pi-calculus) para colocar tais agentes juntos em um SMA. Simulações são freqüentemente utilizadas para se analisar SMAs. As técnicas envolvidas tipicamente consistem em simular um SMA diversas vezes, seja para coletar estatísticas, seja para observar o que acontece através de animações. Contudo, simulações podem ser usadas de forma a pertmitir a realização de verificações automatizadas do SMA caso sejam entendidas como explorações de grandes espaços-de-estados. Nesta tese propomos uma técnica de verificação baseada nessa observação, que consiste em simular um SMA de uma forma guiada, a fim de se determinar se uma dada hipótese sobre ele é verdadeira ou não. Para tal fim, tiramos proveito da importância que os ambientes têm nesta tese: a especificação formal do ambiente de um SMA serve para calcular as evoluções possíveis do SMA como um sistema de transição, estabelecendo assim o espaço-de-estados a ser investigado. Neste cálculo, os agentes são levados em conta simulando-os, a fim de determinar, em cada estado do ambiente, quais são suas ações. Cada execução da simulação é uma seqüência de estados nesse espaço-de-estados, que é calculado em tempo de execução, conforme a simulação progride. A hipótese a ser investigada, por sua vez, é dada como um outro sistema de transição, chamado propósito de simulação, o qual define as simulações desejáveis e indesejáveis (e.g., \"sempre que o agente fizer X, ele fará Y depois\"). Em seguida, é possível verificar se o SMA satisfaz o propósito de simulação de acordo com uma série de relações de satisfatibilidade precisamente definidas. Algoritmicamente, isso corresponde a construir um produto síncrono desses dois sistemas de transições (i.e., o do SMA e o do propósito de simulação) em tempo de execução e usá-lo para operar um simulador. Ou seja, o propósito de simulação é usado para guiar o simulador, de modo que somente os estados relevantes sejam efetivamente simulados. Ao terminar, um tal algoritmo pode fornecer um veredito conclusivo ou inconclusivo. Se conclusivo, descobre-se se o SMA satisfaz ou não o propósito de simulação com relação às observações feitas durante as simulações. Se inconclusivo, é possível realizar alguns ajustes e tentar novamente. em resumo, portanto, nesta tese propomos quatro novos elementos: (i) uma arquitetura de agente, (ii) uma especificação formal do ambiente desses agentes, de modo que possam ser compostos em um SMA, (iii) uma estrutura para descrever a propriedade de interesse, a qual chamamos de propósito de simulação, e (iv) uma técnica para se analisar formalmente o SMA resultante com relação a um propósito de simulação. Esses elementos estão implementados em uma ferramenta, denominada Simulador Formalmente Guiado (FGS, do inglês Formally Guided Simulator). Estudos de caso executáveis no FGS são fornecidos para ilustrar a abordagem.

Les réseaux logiciels (connus sous l'éppellation: Software Defined Networking, SDN), qui s'appuient sur le paradigme de séparation du plan de contrôle et du plan d'acheminement, ont fortement progressé ces dernières années pour permettre la programmabilité des réseaux et faciliter leur gestion. Reconnu aujourd'hui comme des architectures logicielles pilotées par des applications, offrant plus de programmabilité, de flexibilité et de simplification des infrastructures, les réseaux logiciels sont de plus en plus largement adoptés et graduellement déployés par l'ensemble des fournisseurs. Néanmoins, l'émergence de ce type d'architectures pose un ensemble de questions fondamentales sur la manière de garantir leur correct fonctionnement. L'architecture logicielle SDN est elle-même un système complexe à plusieurs composants vulnérable aux erreurs. Il est essentiel d'en assurer le bon fonctionnement avant déploiement et intégration dans les infrastructures.Dans la littérature, la manière de réaliser cette tâche n'a été étudiée de manière approfondie qu'à l'aide de vérification formelle. Les méthodes de tests s'appuyant sur des modèles n'ont guère retenu l'attention de la communauté scientifique bien que leur pertinence et l'efficacité des tests associés ont été largement demontrés dans le domaine du développement logiciel. La création d'approches de test efficaces et réutilisables basées sur des modèles nous semble une approche appropriée avant tout déploiement de réseaux virtuels et de leurs composants. Le problème abordé dans cette thèse concerne l'utilisation de modèles formels pour garantir un comportement fonctionnel correct des architectures SDN ainsi que de leurs composants. Des approches formelles, structurées et efficaces de génération de tests sont les principale contributions de la thèse. En outre, l'automatisation du processus de test est mis en relief car elle peut en réduire considérablement les efforts et le coût.La première contribution consiste en une méthode reposant sur l'énumération de graphes et qui vise le test fonctionnel des architectures SDN. En second lieu, une méthode basée sur un circuit logique est développée pour tester la fonctionnalité de transmission d'un commutateur SDN. Plus loin, cette dernière méthode est étendue pour tester une application d'un contrôleur SDN. De plus, une technique basée sur une machine à états finis étendus est introduite pour tester la communication commutateur-contrôleur.Comme la qualité d'une suite de tests est généralement mesurée par sa couverture de fautes, les méthodes de test proposées introduisent différents modèles de fautes et génèrent des suites de tests avec une couverture de fautes guarantie. / Having gained momentum from its concept of decoupling the traffic control from the underlying traffic transmission, Software Defined Networking (SDN) is a new networking paradigm that is progressing rapidly addressing some of the long-standing challenges in computer networks. Since they are valuable and crucial for networking, SDN architectures are subject to be widely deployed and are expected to have the greatest impact in the near future. The emergence of SDN architectures raises a set of fundamental questions about how to guarantee their correctness. Although their goal is to simplify the management of networks, the challenge is that the SDN software architecture itself is a complex and multi-component system which is failure-prone. Therefore, assuring the correct functional behaviour of such architectures and related SDN components is a task of paramount importance, yet, decidedly challenging.How to achieve this task, however, has only been intensively investigated using formal verification, with little attention paid to model based testing methods. Furthermore, the relevance of models and the efficiency of model based testing have been demonstrated for software engineering and particularly for network protocols. Thus, the creation of efficient and reusable model based testing approaches becomes an important stage before the deployment of virtual networks and related components. The problem addressed in this thesis relates to the use of formal models for guaranteeing the correct functional behaviour of SDN architectures and their corresponding components. Formal, and effective test generation approaches are in the primary focus of the thesis. In addition, automation of the test process is targeted as it can considerably cut the efforts and cost of testing.The main contributions of the thesis relate to model based techniques for deriving high quality test suites. Firstly, a method relying on graph enumeration is proposed for the functional testing of SDN architectures. Secondly, a method based on logic circuit is developed for testing the forwarding functionality of an SDN switch. Further on, the latter method is extended to test an application of an SDN controller. Additionally, a technique based on an extended finite state machine is introduced for testing the switch-to-controller communication. As the quality of a test suite is usually measured by its fault coverage, the proposed testing methods introduce different fault models and seek for test suites with guaranteed fault coverage that can be stated as sufficient conditions for a test suite completeness / exhaustiveness.

Large and complex software that is frequently changed leads to testing challenges. It is well established that the later a fault is detected in software development, the more it costs to fix. This thesis aims to research and develop a method of generating relevant and non-redundant test cases for a regression test suite, to catch bugs as early in the development process as possible. The research was executed at Axis Communications AB with their products and systems in mind. The approach utilizes user data to dynamically generate a Markov chain model and with a Markov chain Monte Carlo method, strengthen that model. The model generates test case proposals, detects test gaps, and identifies redundant test cases based on the user data and data from a test suite. The sampling in the Markov chain Monte Carlo method can be modified to bias the model for test coverage or relevancy. The model is generated generically and can therefore be implemented in other API-driven systems. The model was designed with scalability in mind and further implementations can be made to increase the complexity and further specialize the model for individual needs.

Under två decennier har utvecklare inom mjukvarutestning utvecklat testtekniken Modell-baseradtestning. Tekniken bygger på att man genererar testfall från en modell (tex i UML), istället föratt manuallet skriva testfall. Detta kan göra testprocessen mer effektiv, vilket leder till att merarbeten kan göras på kortare tid. Det kan också ses som en ekonomiskt fördel för företag därtestning är huvudområdet. Modell-baserad testning har goda omdömen och teorin för teknikenär väl dokumenterad i artiklar, arbeten samt böcker. Mycket tyder på att tekniken rent teoretisktär användbar i praktiken dessutom finns det väldigt lite kritik mot tekniken. Men trots alltdetta har Modell-baserad testning inte blomstrat inom IT-industrin.Syftet med detta arbete är att ta reda på vad anledningarna skulle kunna vara till att MBT intelyckats bättre inom industrin. I arbetet används tre olika MBT-verktyg för att testa och sedanjämföra om resultatet i praktiken blir som teorin beskriver tekniken. Studiens resultat pekar påatt tekniken fortfarande är omogen och många brister kring Modell-baserad testning stöts på. / For two decades, software testing developers have developed the Model-based testing technique.The technology is based on generating test cases from a model (e.g. in UML) instead of manuallywriting test cases. This can make the test process more efficient, which leads to more workcan be done in less time. It can also be seen as an economic benefit for companies where testingis the main area. Model-based testing has good reviews and the theory of the technique is welldocumented in articles, works and books. There are many indications that the technology istheoretically useful in practice, with a very few criticisms of the technology. Despite all this,Model-based testing has not expanded in the IT industry.The purpose of this study is to find out what the reasons could be to the fact that MBTdid not succeed better in the industry. In this thesis, three different MBT tools are used totest and then compare whether the result in practice becomes as the theory describes the technique.The result of the study indicates the opposite direction and many shortcomings regardingModel-based testing come across.