Model-Based Mutation Testing of Real-Time Systems via Model Checking

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)

Resumé

Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach
OriginalsprogEngelsk
Titel2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)
ForlagIEEE
Publikationsdatoapr. 2018
Sider59-68
ISBN (Trykt)978-1-5386-6353-0
ISBN (Elektronisk)978-1-5386-6352-3
DOI
StatusUdgivet - apr. 2018
Begivenhed2018 IEEE International Conference on Software Testing, Verification and Validation Workshops - Vasteras, Sverige
Varighed: 9 apr. 201813 apr. 2018

Konference

Konference2018 IEEE International Conference on Software Testing, Verification and Validation Workshops
LandSverige
ByVasteras
Periode09/04/201813/04/2018

Fingerprint

Model checking
Real time systems
Testing
Specifications
Gears
Controllers

Citer dette

Lorber, F., Larsen, K. G., & Nielsen, B. (2018). Model-Based Mutation Testing of Real-Time Systems via Model Checking. I 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW) (s. 59-68). IEEE. https://doi.org/10.1109/ICSTW.2018.00029
Lorber, Florian ; Larsen, Kim Guldstrand ; Nielsen, Brian. / Model-Based Mutation Testing of Real-Time Systems via Model Checking. 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE, 2018. s. 59-68
@inproceedings{280c5d0595664553a02c2b3abb3820b8,
title = "Model-Based Mutation Testing of Real-Time Systems via Model Checking",
abstract = "Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach.",
author = "Florian Lorber and Larsen, {Kim Guldstrand} and Brian Nielsen",
year = "2018",
month = "4",
doi = "10.1109/ICSTW.2018.00029",
language = "English",
isbn = "978-1-5386-6353-0",
pages = "59--68",
booktitle = "2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)",
publisher = "IEEE",
address = "United States",

}

Lorber, F, Larsen, KG & Nielsen, B 2018, Model-Based Mutation Testing of Real-Time Systems via Model Checking. i 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE, s. 59-68, 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops , Vasteras, Sverige, 09/04/2018. https://doi.org/10.1109/ICSTW.2018.00029

Model-Based Mutation Testing of Real-Time Systems via Model Checking. / Lorber, Florian; Larsen, Kim Guldstrand; Nielsen, Brian.

2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE, 2018. s. 59-68.

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Model-Based Mutation Testing of Real-Time Systems via Model Checking

AU - Lorber, Florian

AU - Larsen, Kim Guldstrand

AU - Nielsen, Brian

PY - 2018/4

Y1 - 2018/4

N2 - Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach.

AB - Model-based mutation testing is a fault-based technique for generating effective test suites. Given a formal model of a system and a set of slightly altered variants of the model (mutants), the approach generates a test suite that is able to distinguish the original model from all (non-equivalent) mutants. Generally, this is done via conformance checks between the mutants and the correct specification where witness traces of non-conformance are transformed into test cases. While this procedure generates high-quality test suites, the conformance checks are computationally expensive, resulting in a high test-case generation time. To ensure that the specification is correct, many safety-critical systems are additionally specified via properties, e.g., timed computation tree logic (TCTL) properties. These can be used to verify the specification model via model checking. After this check, the properties are often not used any further. In this paper, we propose to reuse the properties in a combination of model-based mutation testing and the model-checking of properties for real-time systems. That is, we generate a set of mutated models, and check whether they still satisfy the specified properties. In case of a violation, we receive a trace to this violation, which can be transformed into a test case in the same way as in the traditional approach. The advantages of the approach are manifold: the checking of individual small properties is often more efficient than a full conformance check; the resulting test suite is smaller in size and mainly focuses on the safety-critical parts that were specified by the properties; the distribution of the generated test cases gives a very good indication on the quality of the properties; the technique can also be applied to certain kinds of non-functional properties. We apply the technique to an industrial case study of an automated gear controller. It is modeled as a network of timed automata and specified via 46 TCTL properties. We use the tool UPPAAL and its model-checking capabilities to demonstrate the approach.

U2 - 10.1109/ICSTW.2018.00029

DO - 10.1109/ICSTW.2018.00029

M3 - Article in proceeding

SN - 978-1-5386-6353-0

SP - 59

EP - 68

BT - 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW)

PB - IEEE

ER -

Lorber F, Larsen KG, Nielsen B. Model-Based Mutation Testing of Real-Time Systems via Model Checking. I 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). IEEE. 2018. s. 59-68 https://doi.org/10.1109/ICSTW.2018.00029