Visualization of Zones in Real-Time Models
Author
Brobak, Nicolai
Term
4. term
Education
Publication year
2018
Submitted on
2018-06-15
Pages
46
Abstract
Dette speciale undersøger, hvordan zoner (symbolske tilstande) i modeller af realtidssystemer kan visualiseres, da eksisterende værktøjer som UPPAAL og ECDAR kun viser zoner som tekstlige begrænsninger. Efter en introduktion til tidsmodeller (TLTS) og zoners rolle som konvekse polytoper gennemgås hjørneenumerering via pivotering og criss-cross-algoritmen som forudsætning for at kunne fremstille zoneprojektioner i tre dimensioner. Med udgangspunkt heri foreslås og implementeres en ny algoritme til enumerering af hjørner tilpasset realtidszoner, afledt af criss-cross-tilgangen, og den integreres i en prototype, der projicerer zoner til tre dimensioner og viser dem under symbolsk simulering. Værktøjets funktioner og brugergrænseflade beskrives, og nytten evalueres i et mindre studie, hvor seks testpersoner løste tolv opgaver relateret til realtidsmodeller og deres zoner. Resultaterne peger på, at zonevisualisering er et værdifuldt supplement til symbolske simulatorer til modeltjek af realtidssystemer, om end det er uklart, om den udviklede algoritme er den bedste til hjørneenumerering i denne sammenhæng. Specialet skitserer begrænsninger og muligheder for videre arbejde.
This thesis investigates how to visualize zones (symbolic states) in models of real-time systems, motivated by the lack of graphical zone views in existing tools such as UPPAAL and ECDAR, which present only textual constraints. After introducing timed models (TLTS) and the role of zones as convex polytopes, the work reviews vertex enumeration via pivoting and the criss-cross algorithm as prerequisites for rendering three-dimensional projections of zones. Building on this, it proposes and implements a new vertex-enumeration algorithm tailored to real-time zones, derived from the criss-cross approach, and integrates it into a prototype that projects zones to three dimensions and displays them during symbolic simulation. The tool’s features and interface are described, and its usefulness is evaluated in a small study where six participants solved twelve tasks related to real-time models and their zones. The results indicate that zone visualization is a valuable addition to symbolic simulators for real-time model checking, though it remains unclear whether the developed algorithm is the best choice for vertex enumeration in this setting. The thesis outlines limitations and directions for further work.
[This summary has been generated with the help of AI directly from the project (PDF)]
Keywords
Documents