Distrbuted parameter sweep for UPPAAL models
Authors
Villumsen, Brian ; Freiberg, Peter Schmidt ; Krag, Jimmy Merrild
Term
2. term
Education
Publication year
2011
Submitted on
2011-06-01
Pages
106
Abstract
Når man afprøver mange indstillinger for parametre (en parametergennemsøgning), er antallet af mulige kombinationer ofte meget stort, og derfor er særlige værktøjer vigtige. Denne afhandling præsenterer U PPAAL PARMOS, en applikation til parametergennemsøgning, som fordeler verifikationer af en UPPAAL-model på flere ressourcer. Værktøjet anvender en optimeringsmetode til at prioritere, hvilke modelkonfigurationer der undersøges først, så man hurtigere får adgang til de mest relevante resultater. Afhandlingen beskriver både designet af U PPAAL PARMOS samt implementering og test. Derudover undersøges heuristiske optimeringsalgoritmer, og tre af disse bruges i U PPAAL PARMOS: Hill-Climbing, Simulated Annealing og Pareto Archived Evolution Strategy. Eksperimenter med vores implementering tyder på, at der er gode grunde til at anvende U PPAAL PARMOS for hurtigere at opnå ønskede resultater.
When exploring many parameter settings (a parameter sweep), the number of possible combinations is often very large, so dedicated tools are important. This thesis presents U PPAAL PARMOS, a parameter sweep application that distributes verification runs of a UPPAAL model across multiple resources. The tool uses an optimization scheme to prioritize which model configurations to check first, providing faster access to the most relevant results. The thesis describes the design of U PPAAL PARMOS, as well as its implementation and testing. It also studies heuristic optimization algorithms and employs three of them in U PPAAL PARMOS: Hill-Climbing, Simulated Annealing, and Pareto Archived Evolution Strategy. Experiments with our implementation indicate that there are solid grounds for using U PPAAL PARMOS to obtain faster access to desired results.
[This abstract was generated with the help of AI]
Documents