Compositional Backwards Reachability of Timed Automata
Author
Larsen, Ulrik
Term
4. term
Education
Publication year
2002
Abstract
Denne afhandling udvikler en generel ramme for Compositional Backwards Reachability (CBR), en verificeringsmetode der arbejder baglæns fra et mål for at finde alle systemtilstande, som kan føre til det, og som udnytter systemets opbygning. Metoden opbygges ved gradvist at opdele tilstandsrummet i stadig finere områder. Vi præsenterer to CBR-algoritmer og giver formelle korrekthedsbeviser. Vi beskriver Timed Automata Networks (TAN), som er matematiske modeller for realtidssystemer, samt den symbolske, DBM-baserede analyse af Timed Automata, som bruges i værktøjer som Uppaal. Den anden CBR-algoritme anvendes på TAN. Vi diskuterer flere udvidelser af domænet, udvikler en testimplementering af den grundlæggende metode og præsenterer indledende eksperimentelle resultater. Afslutningsvis skitseres fremtidigt arbejde og gives en konklusion.
This thesis develops a general framework for Compositional Backwards Reachability (CBR), a verification method that works backwards from a goal to find all system states that could lead to it while taking advantage of system structure. The method is built by progressively partitioning the state space into finer regions. We present two CBR algorithms and provide formal proofs of correctness. We describe Timed Automata Networks (TAN), mathematical models of real-time systems, and the symbolic, DBM-based analysis of Timed Automata used in tools such as Uppaal. We then apply the second CBR algorithm to TAN. We discuss several extensions of the domain, develop a basic test implementation, and report initial experimental results. Finally, we outline future work and provide a conclusion.
[This abstract was generated with the help of AI]
Documents