@inproceedings{tap2015,
series = {Lecture Notes in Computer Science},
pages = {1--18},
volume = {9154},
publisher = {Springer},
booktitle = {TAP'15},
title = {{"Scalable Incremental Test-case Generation from Large Behavior Models"}},
author = {Bernhard K. Aichernig and Dejan Ni\v{c}kovi\'{c} and Stefan Tiran},
note = {In press.},
year = {2015},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{icst2015doctiran,
author = {Stefan Tiran},
title = {{{Incremental Model-Based Mutation Testing}}},
booktitle = {IEEE 8\textsuperscript{th} Int. Conf. on Software Testing, Verification and Validation, ICST 2015},
year = {2015},
publisher = {IEEE Computer Society},
doi = {10.1109/ICST.2015.7102614},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{fmics,
series = {Lecture Notes in Computer Science},
pages = {113--127},
volume = {9128},
publisher = {Springer},
booktitle = {FMICS'15},
title = {{"Require, Test and Trace IT"}},
author = {Bernhard K. Aichernig and Klaus H{\"o}rmaier and Florian Lorber and Dejan Ni\v{c}kovi\'{c} and Stefan Tiran},
note = {In press.},
year = {2015},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{icst2015tool,
author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J{\"o}bstl and Willibald Krenn and Rupert Schlick and Stefan Tiran},
title = {{{MoMuT::UML - model-based mutation testing for UML}}},
booktitle = {IEEE 8\textsuperscript{th} Int. Conf. on Software Testing, Verification and Validation, ICST 2015},
year = {2015},
doi = {10.1109/ICST.2015.7102627},
publisher = {IEEE Computer Society},
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::UML1 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.},
url = {http://www.ist.tugraz.at/aichernig/publications/papers/icst15-tools.pdf},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{qsic2014oslc,
author = {Bernhard K. Aichernig and Klaus H{\"o}rmaier and Florian Lorber and Dejan Ni\v{c}kovi\'{c} and Rupert Schlick and Didier Simoneau and Stefan Tiran},
title = {{{Integration of Requirements Engineering and Test-Case Generation via {OSLC}}}},
booktitle = {QSIC '14: Proceedings of the 2014 14\textsuperscript{th} International Conference on Quality Software},
year = {2014},
pages = {117--126},
address = {Dallas, USA},
publisher = {IEEE Computer Society},
doi = {10.1109/QSIC.2014.13},
abstract = {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.},
originalfile = {/formal_methods/formal_methods.bib}
}
@article{Aichernig2015,
author = {Bernhard K. Aichernig and Elisabeth J{\"o}bstl and Stefan Tiran},
title = {{{Model-based mutation testing via symbolic refinement checking}}},
journal = {Science of Computer Programming},
volume = {97, Part 4},
number = {0},
pages = {383--404},
year = {2015},
note = {Special Issue: Selected Papers from the 12th International Conference on Quality Software (QSIC 2012)},
issn = {0167-6423},
doi = {10.1016/j.scico.2014.05.004},
publisher = {Elsevier},
abstract = {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},
originalfile = {/formal_methods/formal_methods.bib}
}
@techreport{IST-MBT-2014-03,
author = {Bernhard K. Aichernig and Florian Lorber and Dejan Ni\v{c}kovi\'{c}
and Stefan Tiran},
title = {{{Require, Test and Trace IT}}},
institution = {Institute for Software Technology (IST), Graz University of Technology},
year = {2014},
abstract = {We present a framework for requirement-driven test-case generation
from specifications of synchronous reactive systems. We propose requirement
interfaces as the formal specification model. Contract specifications
of individual requirements are naturally combined by the conjunction
operation. The conjunction of two requirement interfaces has the
property that it subsumes all behaviors of the individual interfaces.
We exploit this property to generate test cases incrementally. We
use a small set of related requirements to drive test-case generation,
thus
avoiding the explosion of the state space to explore. In addition
to test-case generation, we also provide a procedure for incremental
consistency checking of the requirements. Our requirement-driven
approach has several advantages: (1) both consistency checking and
test case generation are incremental and thus more efficient; (2)
test cases are naturally related to requirements, hence enabling
easier traceability; and (3) fail verdicts in a test case can be
mapped to violated requirements. We implemented a prototype using
the SMT-solver Z3.},
url = {https://online.tugraz.at/tug_online/voe_main2.getVollText?pDocumentNr=637834&pCurrPk=77579},
originalfile = {/formal_methods/formal_methods.bib}
}
@techreport{Aichernig2012,
author = {Bernhard Aichernig and Florian Lorber and Stefan Tiran},
title = {{{Formal Test-Driven Development with Verified Test Cases}}},
institution = {Institute for Software Technology (IST), Graz University of Technology},
year = {2012},
timestamp = {2014.02.24},
url = {https://online.tugraz.at/tug_online/voe_main2.getVollText?pDocumentNr=275810&pCurrPk=67400},
urldate = {2013-05-06},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{Aichernig2014a,
author = {Bernhard Aichernig and Florian Lukas Lorber and Stefan Tiran},
title = {{{Formal Test-Driven Development with Verified Test Cases}}},
booktitle = {Proceedings of the 2\textsuperscript{nd} International Conference
on Model-Driven Engineering and Software Development},
year = {2014},
editor = {Luis Ferreira Pires, Slimane Hammoudi, Joaquim Filipe and Rui C{\'e}sar
das Neves},
pages = {626--635},
address = {Lisbon},
month = jan,
publisher = {SCITEPRESS - Science and Technology Publications},
doi = {10.5220/0004874406260635},
isbn = {978-989-758-007-9},
language = {EN},
location = {Lisbon},
timestamp = {2014.02.24},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{Aichernig2012a,
author = {Bernhard Aichernig and Florian Lukas Lorber and Stefan Tiran},
title = {{{Integrating model-based testing and analysis tools via test case
exchange}}},
booktitle = {Proceedings of the 2012 Sixth International Symposium on Theoretical
Aspects of Software Engineering},
year = {2012},
editor = {IEEE Computer Society},
pages = {119--126},
month = jul,
publisher = {IEEE Computer Society},
abstract = {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.},
doi = {10.1109/TASE.2012.20},
isbn = {978-1-4673-2353-6},
language = {EN},
location = {Beijing},
timestamp = {2014.02.24},
originalfile = {/formal_methods/formal_methods.bib}
}
@article{Aichernig2014,
author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J{\"o}bstl
and Willibald Krenn and Rupert Schlick and Stefan Tiran},
title = {{{Killing strategies for model-based mutation testing}}},
journal = {Software Testing, Verification and Reliability},
year = {2015},
pages = {716--748},
volume = {25},
number = {8},
abstract = {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. Copyright (c) 2014 John Wiley
& Sons, Ltd.},
doi = {10.1002/stvr.1522},
issn = {1099-1689},
keywords = {test case generation, model-based testing, mutation testing, random
testing, ioco, action systems, Unified Modeling Language, UML},
timestamp = {2014.02.24},
originalfile = {/formal_methods/formal_methods.bib}
}
@mastersthesis{Tiran2013,
author = {Stefan Tiran},
title = {{{On the Effects of {UML} Modeling Styles in Model-based Mutation Testing}}},
school = {Graz, University of Technology},
year = {2013},
type = {Master Thesis},
abstract = {This thesis deals with the application of model-based mutation testing
in software-development processes. In recent research projects the
Austrian Institute of Technology and the Institute for Software Technology
have developed a prototype toolchain, which can automatically derive
test cases out of UML diagrams. In order to support modern software-development
methods like test-driven development and enabling regression testing,
the idea is used, to decompose test models into their functional
components and gain partial test models. In later development phases,
these partial models can be combined, which can be seen as refinement
of the underlying partial models. In two case-studies this thesis
shows, how partial models can be built. The first case-study deals
with a car alarm system. A given test model is decomposed into two
partial models and alternative modeling styles are presented. The
second case study deals with the bucket control of an agricultural
vehicle. Here, a given test model is optimized and a second partial
model is introduced in order to cope with the complexity of the test
case generation, so that it becomes computational feasible. Additionally,
a comparison among different test case extraction strategies is conducted.},
timestamp = {2014.02.24},
url = {https://online.tugraz.at/tug_online/voe_main2.getvolltext?pCurrPk=71474},
originalfile = {/formal_methods/formal_methods.bib}
}
@techreport{Tiran2012,
author = {Stefan Tiran},
title = {{{The Argos Manual}}},
institution = {Institute for Software Technology (IST), Graz University of Technology},
year = {2012},
timestamp = {2014.02.24},
url = {https://online.tugraz.at/tug_online/voe_main2.getVollText?pDocumentNr=275803&pCurrPk=67399},
urldate = {2013-05-06},
originalfile = {/formal_methods/formal_methods.bib}
}
This file was generated by bibtex2html 1.98.