Model-Based Test Case Generation in Ecdar: Offline Conformance Testing Using Refinement in Ecdar
Authors
Perruchon, Yann Bernard Bastrup ; Bach, Esben Rask
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-06
Pages
43
Abstract
Dette projekt præsenterer en offline, modelbaseret tilgang til test af realtidssystemer ved hjælp af værktøjet Ecdar. Målet er at generere en testpakke, der kan køres lokalt på systemet uden løbende kontakt med modellen. Tilgangen bygger på tidsbestemte input-output-automater, som vi udvider med testkode i både tilstande (lokationer) og overgange (kanter). En central udfordring var at håndtere ure (clocks) i testkoden. Dette blev løst ved at bruge zoner (sæt af mulige klokværdier) og ved at tjekke, at de symbolske tidsværdier i testkoden er gyldige. Hver test sag er konstrueret ved at stille reachability-forespørgsler til hver overgang (kan den nås?), og derefter forlænge sporet frem til den næste output-overgang for at få en kørbar test. Tilgangen blev afprøvet i tre forskellige casestudier og evalueret med PIT mutation testing, hvor små ændringer (mutanter) indføres i systemet for at se, om testene afslører dem. Resultaterne viste, at tilgangen fandt alle refinement-brud (afvigelser fra den forventede adfærd) introduceret af mutanterne i det testede system.
This project presents an offline, model-based approach to testing real-time systems using the Ecdar tool. The goal is to generate a test suite that can be run locally on the system without ongoing interaction with the model. The approach extends timed input–output automata by embedding test code in both states (locations) and transitions (edges). A key challenge was handling clocks in the test code. This was addressed by using zones (sets of possible clock values) and by asserting that the symbolic time values used in the test code are valid. Each test case is built by issuing reachability queries to each transition (can it be reached?) and then extending the trace to the next output transition to produce an executable test. The approach was applied in three case studies and evaluated with PIT mutation testing, which introduces small changes (mutants) into the system to check whether the tests detect them. The results show that the approach detected all refinement violations introduced by the mutants in the system under test.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Documents