Effortless Fault Localisation: Conformance Testing of Real-Time Systems in Ecdar

Gundersen, Tobias Rosenkrantz ; Ovesen, Christian

4. term

Software, Master

2018

2018-06-15

14

Model checking er en automatisk metode til at verificere, at et system opfører sig som beskrevet i dets formelle model. For realtidssystemer—hvor timingen af handlinger er afgørende—bruger værktøjet Ecdar tidsbestemte I/O-automater, en matematisk model af komponenter med input, output og klokker, til at understøtte kompositionel verifikation (at tjekke dele hver for sig og samlet). For at gøre denne tilgang mere anvendelig i industriel udvikling udvider vi Ecdar med overensstemmelsestest og samler det i et nyt integreret udviklingsmiljø (IDE), der rummer modellering, verifikation og test. Værktøjet anvender modelbaseret mutationstestning: det ændrer systematisk modellen for at indføre små fejl (mutationer) og bruger dem til at konstruere tests, som kun kræver modellen og det testede system (SUT). Det hjælper med at finde fejl og, for visse fejlkategorier, at vise at de ikke forekommer. Test kan køres i virkelig tid eller i simuleret tid. Generering og afvikling af testtilfælde kører parallelt for at øge hastigheden. Vi introducerer også nye mutationsoperatorer, der forbedrer evnen til at finde og lokalisere fejl. I et casestudie med 140 fejlfyldte systemer fandt Ecdar alle fejl.

Model checking is an automated way to verify that a system behaves as its formal model specifies. For real-time systems—where the timing of actions matters—the tool Ecdar uses timed I/O automata, a mathematical model of components with inputs, outputs, and clocks, to support compositional verification (checking parts separately and together). To make this approach more useful in industrial development, we extend Ecdar with conformance testing and package it in a new integrated development environment (IDE) that supports modeling, verification, and testing in one place. The tool applies model-based mutation testing: it systematically modifies the model to create small faults (mutations) and uses these to design tests that require only the model and the system under test. This helps locate faults and, for certain fault categories, show that they are absent. Testing can run in real time or in simulated time. Test-case generation and execution are parallelized to speed up the process. We also introduce new mutation operators that improve fault detection and localization. In a case study with 140 faulty systems, Ecdar detected all faults.

[This abstract was generated with the help of AI]

Integration ; Model-Based Mutation Testing ; Conformance Testing ; Testing ; Ecdar ; Model Checking ; Safety-Critical Systems ; Real-Time Systems ; Compositional Systems ; Fault Localisation ; Fault Localization ; Adaptive Test-Cases ; Adaptiveness ; Mutation Testing ; PIT ; Timed Automata ; Timed I/O Automata ; Refinement ; Input-Enabledness ; Mutation Operators ; Determinism ; Test-Case Generation ; Test Execution ; Test Verdicts ; Primary Fails

Download
View record in AAU Student Projects