Stefan Tiran

This is a research summary of my upcoming PhD thesis.
Slides for the associated talk are available at: https://online.tugraz.at/tug_online/voe_main2.getVollText?pDocumentNr=1084742&pCurrPk=84662 (PDF) https://github.com/StefanTiran/doctoral_symposium (LaTeX Source)

Abstract: Model-based mutation testing is a promising approach to automate the generation of test cases. However, application is still limited to small models because of the computational complexity. In the proposed thesis… Mehr anzeigen

This is a research summary of my upcoming PhD thesis.
Slides for the associated talk are available at: https://online.tugraz.at/tug_online/voe_main2.getVollText?pDocumentNr=1084742&pCurrPk=84662 (PDF) https://github.com/StefanTiran/doctoral_symposium (LaTeX Source)

Abstract: Model-based mutation testing is a promising approach to automate the generation of test cases. However, application is still limited to small models because of the computational complexity. In the proposed thesis it is investigated, how the knowledge of the internal structure of the test model can help to push the limits of the model size, which is necessary eg. for interlocking systems. A recently invented incremental language inclusion check for timed automata shall form the basis of an incremental test-case generation method based on partial test models. The approach will be applied to both synchronous and asynchronous test models. The thesis will also include hints on how to model the system-under-test in order to facilitate the proposed incremental test-case generation technique. Weniger anzeigen

Abstract: Model-based mutation testing (MBMT) is a promising testing methodology that relies on a model of the system under test (SUT) to create test cases. Hence, MBMT is a so-called black-box testing approach. It also is fault based, as it creates test cases that are guaranteed to reveal certain faults: after inserting a fault into the model of the SUT, it looks for a test case revealing this fault. This turns MBMT into one of the most powerful and versatile test case generation approaches… Mehr anzeigen

Abstract: Model-based mutation testing (MBMT) is a promising testing methodology that relies on a model of the system under test (SUT) to create test cases. Hence, MBMT is a so-called black-box testing approach. It also is fault based, as it creates test cases that are guaranteed to reveal certain faults: after inserting a fault into the model of the SUT, it looks for a test case revealing this fault. This turns MBMT into one of the most powerful and versatile test case generation approaches available as its tests are able to demonstrate the absence of certain faults, can achieve both, control-flow and data-flow coverage of model elements, and also may include information about the behaviour in the failure case. The latter becomes handy whenever the test execution framework is bound in the number of observations it can make and - as a consequence - has to restrict them. However, this versatility comes at a price: MBMT is computationally expensive. The tool MoMuT::UML (https://www.momut.org) is the result of a multi-year research effort to bring MBMT from the academic drawing board to industrial use. In this paper we present the current stable version, share the lessons learnt when applying two generations of MoMuT::UML in an industrial setting, and give an outlook on the upcoming, third,generation. Weniger anzeigen

This article presents the techniques and results of a novel model-based test case generation approach that automatically derives test cases from UML state machines. The main contribution of this article is the fully automated fault-based test case generation technique together with two empirical case studies derived from industrial use cases. Also, an in-depth evaluation of different fault-based test case generation strategies on each of the case studies is given and a comparison with plain… Mehr anzeigen

This article presents the techniques and results of a novel model-based test case generation approach that automatically derives test cases from UML state machines. The main contribution of this article is the fully automated fault-based test case generation technique together with two empirical case studies derived from industrial use cases. Also, an in-depth evaluation of different fault-based test case generation strategies on each of the case studies is given and a comparison with plain random testing is conducted. The test case generation methodology supports a wide range of UML constructs and is grounded on the formal semantics of Back's action systems and the well-known input–output conformance relation. Mutation operators are employed on the level of the specification to insert faults and generate test cases that will reveal the faults inserted. The effectiveness of this approach is shown and it is discussed how to gain a more expressive test suite by combining cheap but undirected random test case generation with the more expensive but directed mutation-based technique. Finally, an extensive and critical discussion of the lessons learnt is given as well as a future outlook on the general usefulness and practicability of mutation-based test case generation. Weniger anzeigen

In this paper we propose the combination of several techniques into an agile formal development process: model-based testing, formal models, refinement of models, model checking, and test-driven development. The motivation is a smooth integration of formal techniques into an existing development cycle. Formal models are used to generate abstract test cases. These abstract tests are verified against requirement properties by means of model checking. The motivation for verifying the tests and not… Mehr anzeigen

In this paper we propose the combination of several techniques into an agile formal development process: model-based testing, formal models, refinement of models, model checking, and test-driven development. The motivation is a smooth integration of formal techniques into an existing development cycle. Formal models are used to generate abstract test cases. These abstract tests are verified against requirement properties by means of model checking. The motivation for verifying the tests and not the model is two-fold: (1) in a typical safety-certification process the test cases are essential, not the models, (2) many common modelling tools do not provide a model checker. We refine the models, check refinement, and generate additional test cases capturing the newly added details. The final refinement step from a model to code is done with classical test-driven development. Hence, a developer implements one generated and formally verified test case after another, until all tests pass. The process is scalable to actual needs. Emphasis can be shifted between formal refinement of models and test-driven development. A car alarm system serves as a demonstrating case-study. We use Back’s Action Systems as modelling language and mutation analysis for test case generation. We define refinement as input-output conformance (ioco). Model checking is done with the CADP toolbox. Weniger anzeigen

We present a requirement-centered analysis and testing framework that integrates methods and tools for capturing and formalizing textual customer requirements, analyzing requirements consistency, generating test cases from formalized requirements and executing them on the implementation model. The framework preserves a fine grained traceability of informal
and formal requirements, test cases and implementation models throughout every step of the workflow.
We instantiate the framework with… Mehr anzeigen

We present a requirement-centered analysis and testing framework that integrates methods and tools for capturing and formalizing textual customer requirements, analyzing requirements consistency, generating test cases from formalized requirements and executing them on the implementation model. The framework preserves a fine grained traceability of informal
and formal requirements, test cases and implementation models throughout every step of the workflow.
We instantiate the framework with concrete tools that we integrate via a file repository and Open Services for Lifecycle Collaboration (OSLC). The standardized integration ensures that
the framework remains generic – any specific tool used in our instantiation can be replaced by another one with compatible functionality.
We apply our framework on an industrial airbag control chip case study that we use to illustrate step-by-step our requirements driven analysis and test methodology. Weniger anzeigen

In model-based mutation testing, a test model is mutated for test case generation. The resulting test cases are able to detect whether the faults in the mutated models have been implemented in the system under test. For this purpose, a conformance check between the original and the mutated model is required. The generated counterexamples serve as basis for the test cases. Unfortunately, conformance checking is a hard problem and requires sophisticated verification techniques. Previous attempts… Mehr anzeigen

In model-based mutation testing, a test model is mutated for test case generation. The resulting test cases are able to detect whether the faults in the mutated models have been implemented in the system under test. For this purpose, a conformance check between the original and the mutated model is required. The generated counterexamples serve as basis for the test cases. Unfortunately, conformance checking is a hard problem and requires sophisticated verification techniques. Previous attempts using an explicit conformance checker suffered state space explosion. In this paper, we present several optimisations of a symbolic conformance checker using constraint solving techniques. The tool efficiently checks the refinement between non-deterministic test models. Compared to previous implementations, we could reduce our runtimes by 97%. In a new industrial case study, our optimisations can reduce the runtime from over 6 hours to less than 3 minutes. Weniger anzeigen

Europe's industry in embedded system design is currently aiming for a better integration of tools that support their development, validation and verification processes. The idea is to combine model-driven development with model-based testing and model-based analysis. The interoperability of tools shall be achieved with the help of meta-models that facilitate the mapping between different modelling notations. However, the syntactic and semantic integration of tools is a complex and costly task… Mehr anzeigen

Europe's industry in embedded system design is currently aiming for a better integration of tools that support their development, validation and verification processes. The idea is to combine model-driven development with model-based testing and model-based analysis. The interoperability of tools shall be achieved with the help of meta-models that facilitate the mapping between different modelling notations. However, the syntactic and semantic integration of tools is a complex and costly task. A common problem is that different tools support different subsets of a language. Furthermore, semantic differences are a major obstacle to sound integration efforts. In this paper we advocate an alternative, more pragmatic approach. We propose the exchange of test cases generated from the models instead of exchanging the models themselves. The advantage is that test cases have a much simpler syntax and semantics, and hence, the mapping between different tools is easier to implement and to maintain. With a formal testing approach with adequate testing criteria a set of test cases can be viewed as partial models that can be formally analysed. We demonstrate an integration of our test case generator Ulysses with the CADP toolbox by means of test case exchange. We generate test cases in Ulysses and verify properties in CADP. We also generate test cases in CADP and perform a mutation analysis in Ulysses. Weniger anzeigen

Abstract. We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems
from informal requirements. Multiple views of a system, modeled as requirement interfaces, are naturally combined by conjunction. We develop an incremental test generation procedure with several advantages. The test… Mehr anzeigen

Abstract. We propose a framework for requirement-driven test generation that combines contract-based interface theories with model-based testing. We design a specification language, requirement interfaces, for formalizing different views (aspects) of synchronous data-flow systems
from informal requirements. Multiple views of a system, modeled as requirement interfaces, are naturally combined by conjunction. We develop an incremental test generation procedure with several advantages. The test generation is driven by a single requirement interface
at a time. It follows that each test assesses a specific aspect or feature of the system, specified by its associated requirement interface. Since we do not explicitly compute the conjunction of all requirement interfaces of the system, we avoid state space explosion while generating tests. However, we incrementally complete a test for a specific feature with the constraints defined by other requirement interfaces. This allows catching violations of any other requirement during test execution, and not only of the one used to generate the test. Finally, this framework defines
a natural association between informal requirements, their formal specifications and the generated tests, thus facilitating traceability. We implemented a prototype test generation tool and we demonstrate its applicability on an industrial use case. Weniger anzeigen