Concrete Delays for Symbolic Traces
Translated title
Konkrete Tidsværdier for Symbolske Eksekveringer
Authors
Poulsen, Danny Bøgsted ; van Vliet, Jonas
Term
2. term
Education
Publication year
2010
Submitted on
2010-06-02
Pages
87
Abstract
Målet med model checking er at sikre, at et system følger sin specifikation. Værktøjet UPPAAL verificerer timede automater og giver diagnostiske spor, der hjælper brugeren med at se, hvordan en overtrædelse opstår. På grund af de tidsabstraktioner, der bruges i beregningerne, mangler disse spor ofte konkrete forsinkelser, hvilket gør dem svære at forstå. I dette speciale beskriver vi flere metoder til at tilføje konkrete forsinkelser til diagnostiske spor. To af metoderne er rettet mod spor, der krænker sikkerhedsegenskaber (ting der aldrig må ske), og én metode er rettet mod spor, der krænker liveness-egenskaber (ting der til sidst skal ske). Vi beviser korrektheden af alle metoder, tester de to sikkerhedsmetoder op mod hinanden og vurderer liveness-metodens anvendelighed.
Model checking aims to verify that a system behaves according to its specification. The UPPAAL tool checks Timed Automata and provides diagnostic traces that show how a violation occurs. Due to time abstractions used in the computations, these traces often lack concrete delays, which makes them hard to interpret. This thesis presents several methods for adding concrete delays to diagnostic traces. Two methods address traces that violate safety properties (things that must never happen), and one method addresses traces that violate liveness properties (things that must eventually happen). We prove the correctness of all methods, compare the two safety methods against each other, and assess the viability of the liveness method.
[This abstract was generated with the help of AI]
Keywords
Documents