@incollection{formats2015,
year = {2015},
isbn = {978-3-319-22974-4},
booktitle = {Formal Modeling and Analysis of Timed Systems},
volume = {9268},
series = {Lecture Notes in Computer Science},
editor = {Sankaranarayanan, Sriram and Vicario, Enrico},
doi = {10.1007/978-3-319-22975-1_19},
title = {{{Bounded Determinization of Timed Automata with Silent Transitions}}},
publisher = {Springer},
author = {Lorber, Florian and Rosenmann, Amnon and Ni\v{c}kovi\'{c}, Dejan and Aichernig, Bernhard K.},
pages = {288--304},
originalfile = {/formal_methods/formal_methods.bib}
}
@inproceedings{icst2015doclorber,
author = {Florian Lorber},
title = {{{Model-Based Mutation Testing of Synchronous and Asynchronous Real-Time Systems}}},
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.7102615},
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{icst2015amost,
author = {Bernhard K. Aichernig and Florian Lorber},
title = {{{Towards Generation of Adaptive Test Cases from Partial Models of Determinized Timed Automata}}},
booktitle = {Proceedings of the 11th Workshop on Advances in Model Based Testing, A-MOST 2015, co-located with ICST 2015},
year = {2015},
publisher = {IEEE Computer Society},
url = {http://msdl.cs.mcgill.ca/conferences/amost/files/A-MOST_2015_submission_9.pdf},
abstract = {The well-defined timed semantics of timed automata as specification models provide huge advantages for the verification
and validation of real-time systems. Thus, timed automata have already been applied in many different areas, including
model-based testing. Unfortunately, there is one drawback in using timed automata for test-case generation: if they contain
non-determinism or silent transitions, the problem of language inclusion between timed automata becomes undecidable. In recent
work, we developed and implemented a technique to determinize timed automata up to a certain depth k. The resulting timed
automata are unfolded to directed acyclic graphs (DAGs) up to depth k. The unfolding caused an exponential state-space
explosion. Consequently, our model-based test-case generation algorithm for deterministic timed automata, which uses language
inclusion, did not scale anymore.
Within this paper we investigate how to split the determinized
DAGs into partial models, to overcome the problems caused by the increased state space and find effective ways to use the
deterministic DAGs for model-based test case generation.},
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}
}
@inproceedings{safecomp2014,
author = {Bernhard K. Aichernig and Klaus H{\"o}rmaier and Florian Lorber},
title = {{{Debugging with Timed Automata Mutations}}},
year = {2014},
isbn = {978-3-319-10505-5},
booktitle = {Computer Safety, Reliability, and Security},
volume = {8666},
series = {Lecture Notes in Computer Science},
editor = {Bondavalli, Andrea and Di Giandomenico, Felicita},
doi = {10.1007/978-3-319-10506-2_4},
publisher = {Springer International Publishing},
keywords = {Timed automata; debugging; model-based mutation debugging; mutation testing; model-based testing; language inclusion; mutation operators},
pages = {49--64},
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}
}
@incollection{Aichernig2013b,
year = {2013},
isbn = {978-3-642-38915-3},
booktitle = {Tests and Proofs},
volume = {7942},
series = {Lecture Notes in Computer Science},
editor = {Veanes, Margus and Vigan{\`o}, Luca},
doi = {10.1007/978-3-642-38916-0_2},
title = {{{Time for Mutants - Model-Based Mutation Testing with Timed Automata}}},
publisher = {Springer Berlin Heidelberg},
author = {Aichernig, Bernhard K. and Lorber, Florian and Ni\v{c}kovi\'{c}, Dejan},
pages = {20--38},
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}
}
This file was generated by bibtex2html 1.98.