Distributed CDDs - interfacing Uppaal:
Authors
Thomsen, Christian ; Kristensen, Ronnie
Term
4. term
Education
Publication year
2002
Abstract
Dette projekt præsenterer en distribueret implementering af CDD-datastrukturen, som bruges i verifikationsværktøjet Uppaal til at gemme den symbolske del af tilstande. Hver tilstand består af en diskret del (hvilket trin systemet er i) og en symbolsk del (begrænsninger repræsenteret som intervaller). En CDD er beslægtet med Binary Decision Diagrams (BDD’er), men håndterer intervaller frem for rene sand/falsk-værdier. Motivationen er at kunne verificere større modeller ved at dele én global CDD på tværs af flere computernoder, så fælles dele af den symbolske repræsentation kan deles på tværs af mange diskrete tilstande. Ud over selve fordelingen af datastrukturen er fire centrale operationer designet, den distribuerede semantik er beskrevet, og vigtige egenskaber for operationerne er bevist. I afprøvningerne gav én delt CDD fordelt over 4 noder op til 70% hukommelsesbesparelse sammenlignet med 4 separate CDD’er, med en køretidsstraf på 560–900% (cirka 6–10 gange langsommere). Derudover reducerede en mere kompakt hukommelsesrepræsentation af CDD-noderne forbruget med op til 20% i forhold til en eksisterende implementering, men med cirka 50% ekstra køretid. Testene viste dog, at hukommelsen i Uppaal ofte domineres af den diskrete del af tilstandene, ikke den symbolske. Fordi vores arbejde fokuserede på den symbolske del, kunne vi derfor ikke verificere større modeller i den distribuerede løsning end på en enkelt node. Afslutningsvis diskuteres mulige optimeringer, hvilke dele af designet der kan genbruges i andre projekter, der distribuerer beslutningsdiagrammer, samt en kort skitse til en datastruktur for den diskrete del.
This project presents a distributed implementation of the CDD data structure, used in the verification tool Uppaal to store the symbolic part of system states. Each state has a discrete part (which step the system is in) and a symbolic part (constraints represented as intervals). A CDD is related to Binary Decision Diagrams (BDDs) but represents intervals rather than simple true/false values. The goal is to verify larger models by sharing a single global CDD across multiple computing nodes, so common pieces of the symbolic representation can be reused across many discrete states. Beyond distributing the structure itself, we designed four core operations, defined the distributed semantics, and proved key properties of these operations. In experiments, one shared CDD distributed over 4 nodes reduced memory use by up to 70% compared to 4 separate CDDs, at a runtime penalty of 560–900% (about 6–10 times slower). A more compact in-memory representation of CDD nodes saved up to 20% relative to an existing implementation, with an additional runtime cost of about 50%. However, tests showed that in Uppaal the discrete part of states often dominates memory, not the symbolic part. Because our work focused on the symbolic part, the distributed solution did not let us verify larger models than on a single node. The final chapter discusses possible optimizations, which parts of the design may be reusable for other distributed decision diagram projects, and briefly outlines a data structure for the discrete part.
[This abstract was generated with the help of AI]
Documents