Beta: uma ferramenta para geração de testes de unidade a partir de especificações B

Formal methods and software testing are tools to obtain and control software quality. When used together, they provide mechanisms for software specification, verification and error detection. Even though formal methods allow software to be mathematically verified, they are not enough to assure that a system is free of faults, thus, software testing techniques are necessary to complement the process of verification and validation of a system. Model Based Testing techniques allow tests to be generated from other software artifacts such as specifications and abstract models. Using formal specifications as basis for test creation, we can generate better quality tests, because these specifications are usually precise and free of ambiguity. Fernanda Souza (2009) proposed a method to define test cases from B Method specifications. This method used information from the machine s invariant and the operation s precondition to define positive and negative test cases for an operation, using equivalent class partitioning and boundary value analysis based techniques. However, the method proposed in 2009 was not automated and had conceptual deficiencies like, for instance, it did not fit in a well defined coverage criteria classification. We started our work with a case study that applied the method in an example of B specification from the industry. Based in this case study we ve obtained subsidies to improve it. In our work we evolved the proposed method, rewriting it and adding characteristics to make it compatible with a test classification used by the community. We also improved the method to support specifications structured in different components, to use information from the operation s behavior on the test case generation process and to use new coverage criterias. Besides, we have implemented a tool to automate the method and we have submitted it to more complex case studies

A holistic approach to model-based testing of Web service compositions

The behavior of composed Web services depends on the results of the invoked services; unexpected behavior of one of the invoked services can threat the correct execution of an entire composition. This paper proposes an event-based approach to black-box testing of Web service compositions based on event sequence graphs, which are extended by facilities to deal not only with service behavior under regular circumstances (i.e., where cooperating services are working as expected) but also with their behavior in undesirable situations (i.e., where cooperating services are not working as expected). Furthermore, the approach can be used independently of artifacts (e.g., Business Process Execution Language) or type of composition (orchestration/choreography). A large case study, based on a commercial Web application, demonstrates the feasibility of the approach and analyzes its characteristics. Test generation and execution are supported by dedicated tools. Especially, the use of an enterprise service bus for test execution is noteworthy and differs from other approaches. The results of the case study encourage to suggest that the new approach has the power to detect faults systematically, performing properly even with complex and large compositions. Copyright © 2012 John Wiley & Sons, Ltd.

Aplicação de modelos de defeitos na geração de conjuntos de teste completos a partir de Sistemas de Transição com Entrada/Saída

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.

Automated Software Debugging Using Hybrid Static/Dynamic Analysis

With the increasing complexity of today's software, the software development process is becoming highly time and resource consuming. The increasing number of software configurations, input parameters, usage scenarios, supporting platforms, external dependencies, and versions plays an important role in expanding the costs of maintaining and repairing unforeseeable software faults. To repair software faults, developers spend considerable time in identifying the scenarios leading to those faults and root-causing the problems. While software debugging remains largely manual, it is not the case with software testing and verification. The goal of this research is to improve the software development process in general, and software debugging process in particular, by devising techniques and methods for automated software debugging, which leverage the advances in automatic test case generation and replay. In this research, novel algorithms are devised to discover faulty execution paths in programs by utilizing already existing software test cases, which can be either automatically or manually generated. The execution traces, or alternatively, the sequence covers of the failing test cases are extracted. Afterwards, commonalities between these test case sequence covers are extracted, processed, analyzed, and then presented to the developers in the form of subsequences that may be causing the fault. The hypothesis is that code sequences that are shared between a number of faulty test cases for the same reason resemble the faulty execution path, and hence, the search space for the faulty execution path can be narrowed down by using a large number of test cases. To achieve this goal, an efficient algorithm is implemented for finding common subsequences among a set of code sequence covers. Optimization techniques are devised to generate shorter and more logical sequence covers, and to select subsequences with high likelihood of containing the root cause among the set of all possible common subsequences. A hybrid static/dynamic analysis approach is designed to trace back the common subsequences from the end to the root cause. A debugging tool is created to enable developers to use the approach, and integrate it with an existing Integrated Development Environment. The tool is also integrated with the environment's program editors so that developers can benefit from both the tool suggestions, and their source code counterparts. Finally, a comparison between the developed approach and the state-of-the-art techniques shows that developers need only to inspect a small number of lines in order to find the root cause of the fault. Furthermore, experimental evaluation shows that the algorithm optimizations lead to better results in terms of both the algorithm running time and the output subsequence length.

Uma abordagem dirigida a modelo para a geração de casos de teste baseada na detecção de cenários implícitos

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2015.

A Functional Verification Methodology Based on Parameter Domains for Efficient Input Stimuli Generation and Coverage Modeling

Modern Integrated Circuit (IC) design is characterized by a strong trend of Intellectual Property (IP) core integration into complex system-on-chip (SOC) architectures. These cores require thorough verification of their functionality to avoid erroneous behavior in the final device. Formal verification methods are capable of detecting any design bug. However, due to state explosion, their use remains limited to small circuits. Alternatively, simulation-based verification can explore hardware descriptions of any size, although the corresponding stimulus generation, as well as functional coverage definition, must be carefully planned to guarantee its efficacy. In general, static input space optimization methodologies have shown better efficiency and results than, for instance, Coverage Directed Verification (CDV) techniques, although they act on different facets of the monitored system and are not exclusive. This work presents a constrained-random simulation-based functional verification methodology where, on the basis of the Parameter Domains (PD) formalism, irrelevant and invalid test case scenarios are removed from the input space. To this purpose, a tool to automatically generate PD-based stimuli sources was developed. Additionally, we have developed a second tool to generate functional coverage models that fit exactly to the PD-based input space. Both the input stimuli and coverage model enhancements, resulted in a notable testbench efficiency increase, if compared to testbenches with traditional stimulation and coverage scenarios: 22% simulation time reduction when generating stimuli with our PD-based stimuli sources (still with a conventional coverage model), and 56% simulation time reduction when combining our stimuli sources with their corresponding, automatically generated, coverage models.

Revising the Emergency Management Requirements for new generation reactors

The paper presents the application of a new risk-informed methodology for the identification of the Emergency Management Requirements (EMR) to a Generation II, Large size Reactor and a Generation III+ Small Modular Reactor. The results obtained in this test case demonstrate that the actual EMR is conservative, as expected, for the GenII reactor, while the new methodology could be applied for the definition of EMRs for the new generation Nuclear Power Plants, with a possible reduction of the emergency area without loss of safety level. By adopting both probabilistic and deterministic approaches, the study addresses possible accidents and corresponding release scenarios for the two types of reactor, calculates the areas where the accidents have an impact on the population and defines the new EMR considering the health effects on the population.

A framework for table driven testing of Java classes

With the advent of object-oriented languages and the portability of Java, the development and use of class libraries has become widespread. Effective class reuse depends on class reliability which in turn depends on thorough testing. This paper describes a class testing approach based on modeling each test case with a tuple and then generating large numbers of tuples to thoroughly cover an input space with many interesting combinations of values. The testing approach is supported by the Roast framework for the testing of Java classes. Roast provides automated tuple generation based on boundary values, unit operations that support driver standardization, and test case templates used for code generation. Roast produces thorough, compact test drivers with low development and maintenance cost. The framework and tool support are illustrated on a number of non-trivial classes, including a graphical user interface policy manager. Quantitative results are presented to substantiate the practicality and effectiveness of the approach. Copyright (C) 2002 John Wiley Sons, Ltd.

Mixed-integer nonlinear approach for the optimal scheduling of a head-dependent hydro chain

This paper is on the problem of short-term hydro scheduling (STHS), particularly concerning a head-dependent hydro chain We propose a novel mixed-integer nonlinear programming (MINLP) approach, considering hydroelectric power generation as a nonlinear function of water discharge and of the head. As a new contribution to eat her studies, we model the on-off behavior of the hydro plants using integer variables, in order to avoid water discharges at forbidden areas Thus, an enhanced STHS is provided due to the more realistic modeling presented in this paper Our approach has been applied successfully to solve a test case based on one of the Portuguese cascaded hydro systems with a negligible computational time requirement.

Scheduling distributed energy resources in an isolated grid - an artificial neural network approach

Power Systems (PS), have been affected by substantial penetration of Distributed Generation (DG) and the operation in competitive environments. The future PS will have to deal with large-scale integration of DG and other distributed energy resources (DER), such as storage means, and provide to market agents the means to ensure a flexible and secure operation. Virtual power players (VPP) can aggregate a diversity of players, namely generators and consumers, and a diversity of energy resources, including electricity generation based on several technologies, storage and demand response. This paper proposes an artificial neural network (ANN) based methodology to support VPP resource schedule. The trained network is able to achieve good schedule results requiring modest computational means. A real data test case is presented.

Optimal dispatch with reactive power compensation by Genetic Algorithm

This paper presents a Unit Commitment model with reactive power compensation that has been solved by Genetic Algorithm (GA) optimization techniques. The GA has been developed a computational tools programmed/coded in MATLAB. The main objective is to find the best generations scheduling whose active power losses are minimal and the reactive power to be compensated, subjected to the power system technical constraints. Those are: full AC power flow equations, active and reactive power generation constraints. All constraints that have been represented in the objective function are weighted with a penalty factors. The IEEE 14-bus system has been used as test case to demonstrate the effectiveness of the proposed algorithm. Results and conclusions are dully drawn.

3G SGSN Toiminnallisuustestauksen Automatisointi

3G SGSN (3rd Generation Serving GPRS Support Node) onUMTS (Universal Mobile Telecommunications System) pakettiverkon verkkoelementti, joka toimii linkkinä ulkoisen verkon(kuten Internet) ja radioverkon välillä. 3G SGSN ylläpitää tilaajan tietoja ja paikannustietoja päätelaitteen liikkuessa verkon sisällä ja välittää myös dataa ulkoisen verkon ja mobiilipäätelaitteen välillä. Tämän diplomityön aiheena on 3G SGSN toiminnallisuus-testauksen automatisointi. Työssä kehitetään 3G SGSN toiminnallisuustestaukseen soveltuva testauksen automatisointijärjestelmä Linux-ympäristössä AuTS (Automated Test Sequences)-automatisointityökalulla. Kehitystyöhön kuuluu järjestelmän suunnittelu ja toteutus. Toteutettu automatisointijärjestelmä suorittaa 3G SGSN toiminnallisuustestauksen istunnon- ja liikkuvuudenhallinnan testitapauksia.Suoritettujen testitapausten tuloksista luodaan HTML (Hypertext Markup Language)-raportti, joka sisältää tiedot ja analyysit suoritetuista testitapauksista sekä linkit testitapausten lokitietoihin. Hyvä automatisointi vaatii suunnittelua, jossa huomioidaan käytettävyys ja ylläpidettävyys. Näihin ominaisuuksiin on toteutuksessa kiinnitetty erityistä huomiota. Lopputuloksena saatiin toimiva automatisointijärjestelmä, joka osoittaa automatisoinnin tuovan huomattavia etuja toiminnallisuustestauksen tehokkuuteen. Työssä käsitelläänmyös ohjelmistotestausta sekä testauksen automatisointia ja niiden periaatteita.

Test automation scheme for LTE core network element

Modern sophisticated telecommunication devices require even more and more comprehensive testing to ensure quality. The test case amount to ensure well enough coverage of testing has increased rapidly and this increased demand cannot be fulfilled anymore only by using manual testing. Also new agile development models require execution of all test cases with every iteration. This has lead manufactures to use test automation more than ever to achieve adequate testing coverage and quality. This thesis is separated into three parts. Evolution of cellular networks is presented at the beginning of the first part. Also software testing, test automation and the influence of development model for testing are examined in the first part. The second part describes a process which was used to implement test automation scheme for functional testing of LTE core network MME element. In implementation of the test automation scheme agile development models and Robot Framework test automation tool were used. In the third part two alternative models are presented for integrating this test automation scheme as part of a continuous integration process. As a result, the test automation scheme for functional testing was implemented. Almost all new functional level testing test cases can now be automated with this scheme. In addition, two models for integrating this scheme to be part of a wider continuous integration pipe were introduced. Also shift from usage of a traditional waterfall model to a new agile development based model in testing stated to be successful.

Alueellinen energiatasemalli

Kiinnostus energia-asioiden käsittelemiseen alueellisesti yksittäisen rakennuksen asioiden käsittelyn sijaan on lisääntynyt voimakkaasti viime vuosina. Keskustelu alueellisesta ener-gia-asioista on kuitenkin vasta alussa ja alueellisiin energiatarkasteluihin tarvitaan työväli-neitä. Tämän työn päätavoitteena oli luoda alueellinen energiatasemalli, jolla voidaan laskea alueen rakennuskannan energiankulutusta ja -tuotantoa sekä energiantuotannon hiilidi-oksidipäästöjä helposti ja nopeasti. Työssä perehdyttiin alueellisten energiatarkasteluiden tämän hetken tasoon, työvälineisiin ja ohjeistukseen. Myös Suomen rakentamismääräyskokoelman rakennusten energiatehok-kuusmääräyksiin tutustuttiin. Alueellisen energiatasemallin perustana käytettiin uusien rakentamismääräysten E-lukulaskennan ohjeistusta. Mallin toimivuutta testattiin Helsingin Salmenkallioon rakennettavaan uudisrakennusalueeseen. Testattaessa mallilla laskettiin kyseisen alueen energiankulutus sekä erilaisia energiantuo-tantovaihtoehtoja ja todettiin, että erityisesti energiankulutuksen laskenta on hyvin helppoa, kun alueen rakennusten kerrosalat ovat tiedossa. Tuotantopuolen uusiutuvan energian laskeminen luotettavasti vaatii hiukan enemmän taustatyötä, mutta varsinainen mallin käyt-täminen on helppoa ja tulokset saadaan suoraan selkeinä kuvaajina. Työssä onnistuttiin luomaan tavoitteiden mukainen malli, jota voidaan soveltaa erilaisissa alueellisissa energiatarkasteluissa. Tarkasteltaessa energia-asioita alueellisesti, saadaan esimerkiksi alueen huipputehon tarvetta pienennettyä ja energiantuotantoa optimoitua. Malli ei kuitenkaan ole vielä valmis laskentatyökalu, vaan vaatii jatkokehitystä, mikäli sitä halutaan hyödyntää laajemmin.

Modelling of hydrogen stratification and gas mixing in containment using the APROS code

Hydrogen stratification and atmosphere mixing is a very important phenomenon in nuclear reactor containments when severe accidents are studied and simulated. Hydrogen generation, distribution and accumulation in certain parts of containment may pose a great risk to pressure increase induced by hydrogen combustion, and thus, challenge the integrity of NPP containment. The accurate prediction of hydrogen distribution is important with respect to the safety design of a NPP. Modelling methods typically used for containment analyses include both lumped parameter and field codes. The lumped parameter method is universally used in the containment codes, because its versatility, flexibility and simplicity. The lumped parameter method allows fast, full-scale simulations, where different containment geometries with relevant engineering safety features can be modelled. Lumped parameter gas stratification and mixing modelling methods are presented and discussed in this master’s thesis. Experimental research is widely used in containment analyses. The HM-2 experiment related to hydrogen stratification and mixing conducted at the THAI facility in Germany is calculated with the APROS lump parameter containment package and the APROS 6-equation thermal hydraulic model. The main purpose was to study, whether the convection term included in the momentum conservation equation of the 6-equation modelling gives some remarkable advantages compared to the simplified lumped parameter approach. Finally, a simple containment test case (high steam release to a narrow steam generator room inside a large dry containment) was calculated with both APROS models. In this case, the aim was to determine the extreme containment conditions, where the effect of convection term was supposed to be possibly high. Calculation results showed that both the APROS containment and the 6-equation model could model the hydrogen stratification in the THAI test well, if the vertical nodalisation was dense enough. However, in more complicated cases, the numerical diffusion may distort the results. Calculation of light gas stratification could be probably improved by applying the second order discretisation scheme for the modelling of gas flows. If the gas flows are relatively high, the convection term of the momentum equation is necessary to model the pressure differences between the adjacent nodes reasonably.