Project Number: 13859 (62001895)
Project Manager: Prof. dr. Jaco C. van der Pol
Faculty of Electrical Engineering, Mathematics and Computer Science
Systematic testing plays an important role in the quest for improved software quality and reliability, but it is currently error-prone, expensive, and time-consuming. Model-based testing (MBT) is the next step in test automation that addresses these issues. MBT uses an abstract model of the behaviour of the system under test (SUT), from which tests are algorithmically generated. MBT has been successfully applied for testing small systems, but not yet for large, complex, high-tech embedded control software, with millions of lines of code, distribution, concurrency, nondeterminism, and complex interfaces.
The goal of SUMBAT is to advance MBT in those areas that currently prohibit the widespread application of MBT to large and complex embedded software systems. First, the development of a complete and sufficiently detailed model of a large system is often not (economically) feasible. Consequently, MBT must cope with partial models. SUMBAT aims at providing a framework and methods in which model-based testing with partial models, and active automata learning to extend partial models with new information, will be integrated. This will include the possibility to compose and (quantitatively) compare partial models, and to slice and focus models for fault localisation. Second, complex systems combine complex state-behaviour (control-flow) with complex data structures on their inputs and outputs. SUMBAT aims at providing symbolic algorithms for the generation of test cases from models that combine millions of states and transitions with complex and large, MByte-size data instances. Third, it is a major challenge to select from the astronomical number of potential test cases those that have the highest chance of catching most, and most important failures. SUMBAT will integrate statistical test selection based on customers' usage profiles into MBT so that test cases are generated that reflect the real usage of the SUT. Moreover, this enables statistical reasoning over test results providing metrics, such as statistical coverage, reliability, and residual risk.
The central theme of SUMBAT is the combination and integration of different existing but isolated test generation methods. Building on the ioco-testing approach developed by the applicants, various methods such as automata learning, complex test-data generation, symbolic testing, and statistical testing will be integrated to provide a powerful MBT approach that combines the strengths of the individual methods. The central challenge is the well-defined, sound, and scalable combination of the different methods, while coping with distribution, concurrency, and nondeterminism. The latter are ubiquitous in the domain of large and complex systems and they are first-class principles in ioco-testing, but they have hardly been considered in the other methods. The central result will be an integrated prototype MBT tool set that combines the MBT techniques, and that will be applied to case studies of ASML, Océ, and PANalytical.
Project duration: 1-8-2015 /1-8-2019
Project budget: 770 k-€ funding
Number of person/months: 168 person months
Project Coordinator: Radboud University
Participants: Radboud University, UT, TNO-ESI, ASML, Océ, PANalytical
Project budget CTIT: 220.4 k-€ funding
Number of person months CTIT: 48 person months
Involved groups: Formal Methods and Tools group
CTIT Research Centre: Centre for Safety and Security in Smart Societies (CS.4)