UPPAAL

UPPAAL er et integrert verktøy miljø for modellering, validering og verifikasjon av sanntidssystemer modellert som nettverk av tidsbestemt automater, utvidet med datatyper (avgrenset heltall, tabeller, etc.).
UPPAAL CORA er en gren av UPPAAL for Cost Optimal Reachability Anslysis utviklet av UPPAAL teamet som en del av VHS og Ametist prosjekter. Mens UPPAAL støtter modellsjekking av tidsbestemt automater, bruker UPPAAL CORA en forlengelse av tidsbestemt automater kalt LPTA. LPTA lar deg kommentere modellen med tanken om kostnadene.
Dette kan være kostnaden av forsinkelsen i visse situasjoner eller kostnaden av bestemte handlinger. UPPAAL CORA finner deretter optimale stier matchende mål forhold.
UPPAAL CORA har vært brukt i en rekke case-studier. Noen av disse er beskrevet på casestudie side av dette nettstedet. Hvis du kommer opp med interessante bruksområder, kan du kontakte oss. Vi er interessert i å høre hva du gjør!
På grunn av ulike interne datastrukturer, består UPPAAL CORA i dag av to forskjellige versjoner:
En versjon for den forenklede tilfelle av tid optimal reachability analyse.
En versjon for hele språket LPTA.
Som UPPAAL, er UPPAAL CORA gratis for ikke-kommersiell bruk, f.eks for evaluering, forskning og undervisning.
Her er noen viktige trekk ved "UPPAAL":
Robust
 
· Modellering språket UPPAAL CORA er robust mot endringer i problemet modellert. Dette betyr at investeringen i modelleringen ikke går tapt når problemet endres, siden det er lett å tilpasse eksisterende modellen.
 
Fast
 
· Selv om teknologien er ganske ny, eksperimentell og svært forskjellig fra teknikker som brukes i tradisjonell operasjonell forskning, er UPPAAL CORA konkurransedyktig i en rekke case-studier.
 
Kompatibel
 
· Språket UPPAAL CORA er et overordnet UPPAAL. Enhver gyldig UPPAAL modellen er også en gyldig UPPAAL CORA modell. Dette gjør det enkelt og praktisk å bruke og tilpasse eksisterende modeller for å UPPAAL CORA.
 
Strøm
 
· UPPAAL CORA er basert på den nyeste intern utvikling versjon av UPPAAL, som inneholder de nyeste ytelse og språk forbedringer. Det er imidlertid et eksperimentelt verktøy og mangler mange av verifikasjons funksjonene UPPAAL.
Begrensninger:
UPPAAL CORA med full LPTA bæreren har en rekke begrensninger. Disse begrensningene er ikke fundamentale, men er et resultat av å bruke nye interne datastrukturer med en foreløpig begrenset funksjon sett. Over tid vil disse begrensningene løses.
- Ingen ekstrapolering, derav oppsigelse er ikke garantert med mindre du garantere at enten:
· Systemet er asyklisk.
· Alle klokker er avgrenset av invarianter.
- Enkelt reachability bare:
· Ingen liveness sjekk
· Ingen vranglås sjekk
- Begrenset bruk av guiding:
· Støtte for (pris + gjenstår) sortering er implementert (best først søk)
· Støtte for heuristisk variabel er implementert, men uttrykket kan ikke referere til kostnadene variable.
Hva er nytt i denne versjonen:
· Denne utgivelsen løser krasj bugs og en minnelekkasje.