Formal Test-Driven Development with Verified Test Cases

Bernhard K. Aichernig, Florian Lorber, Stefan Tiran

2014

Abstract

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.

Paper Citation

in Harvard Style

Aichernig B., Lorber F. and Tiran S. (2014). Formal Test-Driven Development with Verified Test Cases . In Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014) ISBN 978-989-758-007-9, pages 626-635. DOI: 10.5220/0004874406260635

in Bibtex Style

@conference{mbat14,
author={Bernhard K. Aichernig and Florian Lorber and Stefan Tiran},
title={Formal Test-Driven Development with Verified Test Cases},
booktitle={Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014)},
year={2014},
pages={626-635},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004874406260635},
isbn={978-989-758-007-9},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 2nd International Conference on Model-Driven Engineering and Software Development - Volume 1: MBAT, (MODELSWARD 2014)
TI - Formal Test-Driven Development with Verified Test Cases
SN - 978-989-758-007-9
AU - Aichernig B.
AU - Lorber F.
AU - Tiran S.
PY - 2014
SP - 626
EP - 635
DO - 10.5220/0004874406260635