Distributed parameter sweep for UPPAAL models
Authors
Krag, Jimmy Merrild ; Freiberg, Peter Schmidt ; Villumsen, Brian
Term
1. term
Education
Publication year
2011
Submitted on
2011-01-11
Pages
59
Abstract
Denne rapport præsenterer UPPAAL PARMOS, en applikation til distribueret parameter sweep af UPPAAL-modeller, der skal automatisere gentagne verifikationskørsler og udnytte grid-ressourcer. Udgangspunktet er behovet for at effektivisere modelchecking af realtidssystemer i UPPAAL, hvor mange næsten ens kørsler ellers er tidskrævende og fejlbehæftede at udføre manuelt. Løsningen er udviklet med afsæt i en gennemgang af eksisterende parameter sweep-rammeværk og beslægtet arbejde og realiseres som en modulær arkitektur med et webservice-baseret front end og en simpel webportal til demonstration. UPPAAL PARMOS tilbyder et rigt API til indsendelse, adgang og ændring af opgaver og metadata, samt en specialudviklet syntaks, hvor mål, betingelser og parametricentre kan specificeres. Den modulære tilgang skal give fleksibilitet i optimering og tilpasning, og rapporten beskriver design- og implementeringsvalg samt relevante baggrundsbegreber fra distribuerede systemer. Test og resultater behandles senere i rapporten, men er ikke indeholdt i dette uddrag.
This report presents UPPAAL PARMOS, an application for distributed parameter sweeps of UPPAAL models that automates repetitive verification runs and leverages grid resources. The work addresses the need to streamline model checking for real-time systems in UPPAAL, where numerous near-identical runs are otherwise tedious and error-prone to perform manually. The solution builds on a survey of existing parameter sweep frameworks and related efforts and is realized as a modular architecture with a web service front end and a simple web portal for demonstration. UPPAAL PARMOS provides a rich API for submitting, accessing, and mutating tasks and metadata, along with a custom syntax that allows goals, conditions, and parameter intervals to be specified. The modular approach is intended to support flexibility in optimization and customization, and the report outlines key design and implementation choices as well as relevant background in distributed systems. Testing and results are discussed later in the report but are not included in this excerpt.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents