Extending a Real-Time Model-Checker to a Test-Case Generation Tool Using libCoverage

Abstract: UPPAAL is a model-checker developed by the Department of Information Technology at Uppsala University in Sweden together with Aalborg University inDenmark. UPPAAL can be used to model, simulate, and verify timed automata. It has been used in many case studies since the first release in 1995. libCoverage is a library developed at Uppsala University which can be used togenerate test-cases for real-time systems described as networks of timed automata. The test-cases are generated based upon a given coverage criteria, where the coverage criteria is specified by a parameterized observer automaton. The library is designed to extend model-checking tools, such as UPPAAL or SPIN. The aim of this thesis is to extend UPPAAL 4.0 with libCoverage. For this purpose the grammar of the property file was extended to support libCoverage specific queries, and a modified reachability algorithm was presented which supports coverage exploration. We also extended each state with information about its current coverage, and implemented a wrapper which makes it possible for libCoverage to fetch information from UPPAAL about the system of timed automata. In conclusion, we show that UPPAAL 4.0 can be extended with libCoverage tosupport test-case generation.