Beta 1


Title Algoritmer og værktøjer for real-time logikker
Author Heise, William P.
Supervisor Hansen, Michael Reichhardt (Embedded Systems Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Bachelor thesis
Year 2008
Abstract Jeg har lavet programmer, der kan vericere hvorvidt en endelig tilstands maskine kan tilfredsstilles af en temporal formel. Det overordnet formål har været at opbygge en platform til verifikation af især interval logiske formler. Platformen er opbygget omkring .NET platformen og bygger især på funktions programmeringssproget F#. Der er dog ingen principielle vanskeligheder ved at overfører resultaterne og programmer til for eksempel et andet funktions programmeringssprog med imperative faciliteter. Konkret er tre model tjeknings algoritmer implementeret. Den første er en standart CTL model tjekker, som er lavet for at eksperimentere omkring platform arkitekturen. Derefter er der implementeret to model tjeknings algoritmer for formler, der udtrykkes i interval logikken Duration Calculus. Den første af disse algoritmer bygger på bottom-up model tjekning og en række grafalgoritmer. Den anden algoritme udvider den første i den forstand, at algoritmen generere en række Boolske constraints over lineære formler. Denne algoritme er implementeret, og der er udført eksperimenter på de genererede formler med solveren HySAT. I denne process blev det klar at for visse typer af DC formler, er det nødvendigt at indfører kvantorer i de lineære constraints, og derfor må en sat solver benyttes som understøtter (en stor delmængde af) Presburg aritmentik. Den opbygget platform omkring .NET og F# har vist sig at udgøre en slagkraftig basis for hurtig prototypning af avanceret model tjeknings algoritmer.
Series IMM-B.Sc.-2008-22
Fulltext
Original PDF bac08_22.pdf (0.63 MB)
Admin Creation date: 2008-07-03    Update date: 2008-07-03    Source: dtu    ID: 221245    Original MXD