Advances in constraint solving and increases in processing power have enabled new approaches for automating specification-based testing. However, writing specifications and scaling techniques that utilize them remain challenging. We introduce Milao -- a novel framework for mixed imperative and declarative formulation and solving of structural constraints -- which addresses both these challenges. One, Milao introduces a mixed style for writing specifications using a combination of declarative and imperative styles, which provides flexibility in specification formulation and reduces its burden on the user. Two, it introduces a mixed technique for solving constraints using a combination of solvers in synergy. As enabling technologies, the Alloy tool-set and the Java PathFinder model checker are used. Initial experiments witness the benefits of our framework. / text

No description available.

This thesis describes the development and evaluation of a manual black-box testing method inspired by Zweben's test adequacy criteria, which apply white-box analogues of all-DU-pairs and all-nodes to a flow graph generated from the black-box specification. The approach described herein generates tests from a matrix representation of a class interface based on the flow graph concept. In this process, separate matrices for all-DU-pairs and all-nodes guide the generation of the required tests. The primary goal of the research is not to optimize the number of tests generated but to describe the process in a user-friendly manner so that practitioners can utilize it directly, quickly, and efficiently for real-world testing purposes. The approach has been evaluated to assess its effectiveness at detecting bugs. Both strategies - all-DU-pairs and all-nodes - were compared against three other testing methods: the commercial white-box testing tool Jtest, Orthogonal Array Testing Strategy (OATS), and test cases generated at random. The five approaches were applied across a sample of eleven java classes selected from java.util.*. Experimental results indicate that the two versions resulting from this research performed on par with or better than their respective equivalent approaches. The all-DU-pairs method performed better than all other approaches except for the random approach, with which it compared equally. Experimental evaluation results thus indicate that an automated approach based on the manual method is worth exploring. / Master of Science

In this thesis we investigate the feasibility of learning-based testing (LBT) as a viable testing methodology for reactive systems. In LBT, a large number of test cases are automatically generated from black-box requirements for the system under test (SUT) by combining an incremental learning algorithm with a model checking algorithm. The integration of the SUT with these algorithms in a feedback loop optimizes test generation using the results from previous outcomes. The verdict for each test case is also created automatically in LBT. To realize LBT practically, existing algorithms in the literature both for complete and incremental learning of finite automata were studied. However, limitations in these algorithms led us to design, verify and implement new incremental learning algorithms for DFA and Kripke structures. On the basis of these algorithms we implemented an LBT architecture in a practical tool called LBTest which was evaluated on pedagogical and industrial case studies. The results obtained from both types of case studies show that LBT is an effective methodology which discovers errors in reactive SUTs quickly and can be scaled to test industrial applications. We believe that this technology is easily transferrable to industrial users because of its high degree of automation. / <p>QC 20130312</p>

This thesis concerns the design, implementation and evaluation of a specification based testing architecture for reactive systems using the paradigm of learning-based testing. As part of this work we have designed, verified and implemented new incremental learning algorithms for DFA and Kripke structures.These have been integrated with the NuSMV model checker to give a new learning-based testing architecture. We have evaluated our architecture on case studies and shown that the method is effective. / QC 20110822

Automating the generation of test cases for software is an active area of research. Specification based test generation is an approach in which a formal representation of a method is analyzed to generate valid test cases. Constraint solving and state space exploration are important aspects of the specification based test generation. One problem with specification based testing is that the size of the state space explodes when we apply this approach to a code of practical size. Hence finding ways to reduce the number of candidates to explore within the state space is important to make this approach practical in industry. Korat is a tool which generates test cases for Java programs based on predicates that validate the inputs to the method. Various ongoing researches intend to increase the tools effectiveness in handling large state space. Parallelizing Korat and minimizing the exploration of invalid candidates are the active research directions. This report surveys the basic algorithms of Korat, PKorat, and Fast Korat. PKorat is a parallel version of Korat and aims to take advantage of multi-processor and multicore systems available. Fast Korat implements four optimizations which reduce the number of candidate explored to generate validate candidates and reduce the amount of time required to explore each candidate. This report also presents the execution time results for generating test candidates for binary tree, doubly linked list, and sorted singly linked list, from their respective predicates. / text

Naujuose programiniuose produktuose plačiai taikoma mobilioji įranga (mobilieji telefonai, delniniai kompiuteriai). Programinės įrangos kūrimo procese svarbią vietą užima testavimas. Dabartinių mobiliųjų įranginių apribojimai (darbo sparta, atminties kiekis, energija, ekrano dydis, platformų įvairumas) kelia naujas problemas programinės įrangos kūrimo procesui, tame tarpe ir testavimui. Testavimo proceso automatizavimas leidžia sumažinti bandymų trukmę, padidinti testavimo darbų apimtį. Programinės įrangos testavime mobiliems įrenginiams svarbu išskirti grafinės vartotojo sąsajos testavimą. Svarbi testavimo dalis – testavimas pagal specifikaciją. Šiame darbe nagrinėjamas grafinės vartotojo sąsajos automatizuotas testavimas mobiliai įrangai, nustatomi tikslai, galimi keliai jiems pasiekti bei galimas testavimo aplinkos praplėtimas testų generavimui pagal specifikaciją. / Mobile devices such as cell phones and personal digital assistance are widely used in new software products. Testing takes important place in software development process. Constraints of mobile devices (speed, amount of memory, energy, small screen, wide range of platforms) raise new problems for software development process including testing phase. Automated approach of software testing reduces testing time and increases testing range. It is important to distinguish graphic user interface as a special part of testing. The important part of testing is specification based testing. The aim of these master theses is to analyze automated testing of GUI for mobile devices, define testing tasks and enhance mobile device testing framework by providing means for test case generation from specification.