AAU Student Projects - visit Aalborg University's student projects portal
A master's thesis from Aalborg University
Book cover


Improving the Model Checking Activity - H-UPPAAL: A New Integrated Development Environment for Model Checking

Authors

;

Term

4. term

Education

Software, Master

Publication year

2017

Submitted on

Pages

74

Abstract

Model checking bruges til automatisk at verificere, om et systems model lever op til ønskede egenskaber, men forskningen har primært fokuseret på hastighed og ressourceforbrug. Dette projekt adresserer selve arbejdsprocessen i model checking ved at introducere H-UPPAAL, et nyt integreret udviklingsmiljø, der bygger på UPPAAL og tilføjer hierarkier samt IDE-lignende funktioner for at støtte modellering, verifikation og analyse. Projektets centrale spørgsmål er: Hvordan kan introduktion af hierarkier og integrerede udviklingsfunktioner forbedre arbejdsgangen i model checking-aktiviteten? For at besvare spørgsmålet udvikles værktøjet og vurderes gennem ekspertindsigt, brugbarhedsvurdering og en præstationstest, hvor H-UPPAAL sammenlignes med det etablerede værktøj UPPAAL. De rapporterede evalueringer peger på, at de nye begreber skaber værdi for model checking-arbejdet, selvom detaljerede, kvantitative resultater ikke fremgår af dette uddrag.

Model checking automatically verifies whether a system model satisfies desired properties, yet most research emphasizes speed and resource use. This project targets the broader workflow of model checking by introducing H-UPPAAL, a new integrated development environment that builds on UPPAAL and adds hierarchies and IDE-like features to support modeling, verification, and analysis. The core research question is: How can hierarchies and integrated development features improve the workflow of the model checking activity? To answer it, the authors develop the tool and evaluate it through expert input, usability assessment, and a performance test comparing H-UPPAAL with the mature UPPAAL tool. The reported evaluations indicate that the introduced concepts add value to model checking practice, although detailed quantitative results are not included in this excerpt.

[This summary has been generated with the help of AI directly from the project (PDF)]

Keywords

model checking ; verification ; uppaal ; huppaal ; h-uppaal ; hierarchies ; integrated development environment ; IDE ; performance ; test ; evaluation ; usability

Documents

Download
View record in AAU Student Projects