Slicing for UPPAAL
Authors
Sørensen, Uffe ; Thrane, Claus Rørbæk
Term
4. term
Education
Publication year
2007
Abstract
Denne afhandling introducerer slicing til Uppaal, et softwareværktøj til at opbygge og kontrollere modeller. Slicing er en teknik inden for statisk analyse, der fjerner dele af en model, som er irrelevante for en given verifikationsopgave, så modellen bliver mindre, mens svaret for netop den opgave bevares. Vi viser, hvordan slicing kan give reachability-bevarende reduktioner af Uppaal-modeller (det vil sige, at det bevarer, om bestemte tilstande kan nås), så værktøjet kan køre hurtigere. At automatisere slicing i Uppaal mindsker behovet for, at brugere manuelt finjusterer modeller for at verificere en bestemt egenskab. Det hjælper også mindre erfarne brugere, som kan komme til at medtage unødvendige mængder data i deres modeller, og gør det muligt at verificere egenskaber, som Uppaal ellers ikke ville kunne tjekke.
This thesis introduces slicing to Uppaal, a software tool for building and checking models. Slicing is a static analysis technique that removes parts of a model that are irrelevant to a given verification task, reducing its size while keeping the answers the same for that task. We show how slicing can produce reachability-preserving reductions of Uppaal models (that is, it keeps whether certain states can be reached), so the tool may run faster. Automating slicing in Uppaal reduces the need for users to hand-tune models to verify particular properties. It also helps less experienced users who might include unnecessary data in their models, enabling verification of properties that Uppaal might otherwise be unable to check.
[This abstract was generated with the help of AI]
Documents