UPPAAL

UPPAAL er et integreret værktøj miljø til modellering, validering og verificering af realtidssystemer modelleret som netværk af tidsindstillet automater, forlænget med datatyper (afgrænset heltal, arrays, etc.).
UPPAAL CORA er en gren af ​​UPPAAL for Cost Optimal Sikring af adgang Anslysis udviklet af UPPAAL hold som en del af VHS og Ametist projekter. Hvorimod UPPAAL understøtter model kontrol af tidsstyret automater, bruger UPPAAL CORA en forlængelse af tidsbestemt automata kaldet LPTA. LPTA tillader dig at anmærke modellen med begrebet omkostninger.
Det kan være udgifter til forsinkelser i visse situationer eller omkostningerne ved bestemte handlinger. UPPAAL CORA finder derefter optimale stier matchende goal betingelser.
UPPAAL CORA har været anvendt i en række casestudier. Nogle af disse er beskrevet på casestudiet side af dette websted. Hvis du kommer op med interessante anvendelsesmuligheder, så kontakt os. Vi er interesseret i at høre, hvad du gør!
På grund af forskellige interne datastrukturer, UPPAAL CORA består i øjeblikket af to forskellige versioner:
En version til den forenklede tilfælde af tid optimal sikre adgang analyse.
En version til den fulde sprog LPTA.
Ligesom UPPAAL, UPPAAL CORA er gratis for non-profit brug, f.eks til evaluering, forskning og undervisning.
Her er nogle vigtige funktioner i "UPPAAL":
Robust
 
· Modelleringen sprog UPPAAL CORA er robust over for ændringer i det problem modelleret. Det betyder, at din investering i modellering ikke går tabt, når problemet ændrer sig, da det er let at tilpasse den eksisterende model.
 
Hurtig
 
· Selv om teknologien er forholdsvis nyt, eksperimenterende og meget forskellige fra teknikker, der anvendes i traditionel operationel forskning, er UPPAAL CORA konkurrencedygtig i en række casestudier.
 
Kompatibel
 
· Sproget i UPPAAL CORA er en overordnet UPPAAL. En gyldig UPPAAL model er også et gyldigt UPPAAL CORA model. Dette gør det nemt og bekvemt at genbruge og tilpasse dine eksisterende modeller til at UPPAAL CORA.
 
Nuværende
 
· UPPAAL CORA er baseret på den nyeste interne version udvikling UPPAAL, der indeholder de nyeste resultater og sproglige forbedringer. Det er dog en eksperimentel værktøj og mangler mange af verifikation funktioner i UPPAAL.
Begrænsninger:
UPPAAL CORA med fuld LPTA støtte har en række begrænsninger. Disse begrænsninger er ikke grundlæggende, men er et resultat af at anvende nye interne datastrukturer med en øjeblikket er begrænset feature sæt. Over tid vil disse begrænsninger blive løst.
- Ingen ekstrapolation, dermed opsigelse er ikke garanteret, medmindre du garantere, at enten:
· Systemet er acyklisk.
· Alle ure er afgrænset af invarianter.
- Kun Simple sikre adgang:
· Ingen liveness kontrol
· Ingen dødvande kontrol
- Begrænset brug af vejledende:
· Støtte til (cost + tilbage) sortering gennemføres (bedste første søgning)
· Støtte til heuristisk variabel gennemføres, men udtrykket kan ikke henvise til omkostningerne variabel.
Hvad er nyt i denne version:
· Denne version løser nedbrud bugs og en hukommelsesfejl.