Integrating NorduGrid system with Uppaal verification tool
Authors
Liu, Dong ; Huong, Hoang Thi Thu
Term
4. term
Education
Publication year
2004
Abstract
This thesis investigates how to integrate D‑Uppaal (the distributed version of the Uppaal verification tool) with NorduGrid to make the verification of large and complex real‑time systems more accessible to non‑expert users. The motivation is that large models require substantial computing resources, which grid technologies can provide across institutions, while existing grid tools are primarily command‑line based and cumbersome for ordinary application users. The research question is how to design and implement a user‑friendly integration so that distributed verification can be launched directly from the Uppaal interface without manual grid commands. The method includes a requirements analysis targeting no command‑line interaction, use of multiple CPUs, concurrent tasks, and security; the design of a system architecture and user interface (including a grid monitor and xRSL parameter handling); and the implementation of core classes (e.g., SystemInspector, VerificationGrid, CheckTimeOut, GraphProxy, and SinglePanel) that automate NorduGrid proxy management, job submission, status monitoring, result retrieval, and cancellation via NorduGrid tools. Prior experiments (from the previous semester) demonstrated that running D‑Uppaal on NorduGrid enables verification of larger systems; this work packages that capability into an integrated solution, allowing one‑click execution from Uppaal. The evaluation presented in the report centers on design and implementation; specific performance outcomes are not included in the provided excerpt. The contribution is a prototype that lowers the barrier to high‑performance verification by unifying resource management, security, and job lifecycle control within Uppaal’s user interface.
Denne afhandling undersøger, hvordan D‑Uppaal (den distribuerede version af verifikationsværktøjet Uppaal) kan integreres med NorduGrid for at gøre verifikation af store og komplekse realtidssystemer mere tilgængelig for almindelige brugere. Baggrunden er, at store modeller kræver betydelige beregningsressourcer, og at Grid‑teknologi kan levere disse ressourcer på tværs af institutioner, men at eksisterende grid‑værktøjer typisk betjenes via kommandolinjer og derfor er svære at anvende i praksis. Afhandlingens forskningsspørgsmål er, hvordan man designer og implementerer en brugervenlig integration, så verificering kan startes direkte fra Uppaal uden at brugeren skal håndtere grid‑kommandoer. Metodisk omfatter arbejdet kravanalysen “ingen kommandosystem”, brug af flere CPU’er, samtidige opgaver og sikkerhed; design af systemarkitektur og brugergrænseflade (herunder grid‑monitor og parametre til xRSL); samt implementering af centrale klasser (fx SystemInspector, VerificationGrid, CheckTimeOut, GraphProxy og SinglePanel), der automatisk håndterer NorduGrid‑proxy, jobafsendelse, statusovervågning, resultathentning og eventuel afbrydelse via NorduGrid‑værktøjer. Tidligere eksperimenter (fra forrige semester) viste, at kørsel af D‑Uppaal på NorduGrid gør det muligt at verificere større systemer; nærværende arbejde omsætter denne erfaring til en integreret løsning, hvor verifikation kan igangsættes med ét klik fra Uppaal. Evalueringen i rapporten fokuserer på design- og implementeringsaspekter; konkrete ydelsesresultater er ikke beskrevet i det medfølgende uddrag. Bidraget er en prototype, der sænker adgangsbarrieren til high‑performance verifikation ved at samle ressourcestyring, sikkerhed og joblivscyklus i Uppaal’s brugergrænseflade.
[This apstract has been generated with the help of AI directly from the project full text]
