Vous êtes ici

Optimal test-case generation with game theory

Equipe et encadrants
Département / Equipe: 
Site Web Equipe: 
Directeur de thèse
Nicolas Markey
Co-directeur(s), co-encadrant(s)
Sujet de thèse

Computer systems play an ever-growing role in our lives, from widespread leisure applications to safety-critical medical appliances or industrial plants. Testing is the most-used verification technique to ensure correct behaviour of such systems. But it remains costly and error-prone, thus its automatization using formal methods is welcome.

Testing reactive systems consists in sending well-chosen inputs to the system under test (SUT) and observing outputs, with the aim of finding situations where the SUT would not fulfill its specification[1]. It can
conveniently be phrased as a game [2,3] between the tester, trying to evidence non-conformance along behaviours targeted by test purposes, and the s.u.t., trying to follow the specification.

The aim of this thesis is to deeper explore and strengthen this correspondance in the context of automatic test generation using formal methods, in particular in the following directions:
- when no winning strategy exist, it is sometimes advised to "reformulate the test purpose" [4]. This is very unsatisfactory, and we would better look for other notions of winning conditions, such as winning against fair strategies [5]. Test cases corresponding to dominant or admissible strategies would also be worth investigating.
- most computer systems are subject to real-time constraints. Generating test-cases for such systems raises new challenges [6], including determinization questions for timed automata, of the development of efficient algorithms for generating test cases. Computing permissive strategies [7] and considering imprecision
issues are also of particular interest in this setting.
- besides time, other quantities can be taken into account, against which test cases can be optimized. This may include the cost (or energy) consumed for applying a test case, its efficiency (e.g. in terms of duration), or the coverage of the SUT by the test suite.


[1] J. Tretmans. Test Generation with Inputs, Outputs and Repetitive Quiescence. SCT 17(3), 1996.
[2] A. Blass et al. Play to test. FATES 2005.
[3] M. Yannakakis. Testing, optimization, and games. ICALP 2004.
[4] A. David et al. Testing real-time systems under uncertainty. FMCO 2010.
[5] S. Ramangalahy. Strategies for conformance testing. 1998.
[6] K.G. Larsen et al. Online testing of real-time systems using UPPAAL. FATES 2004.
[7] P. Bouyer et al. Permissive strategies in timed automata and games. AVOCS 2015.

Début des travaux: 
Mots clés: 
Formal methods, model-based testing, quantitative verification
IRISA - Campus universitaire de Beaulieu, Rennes