UPPAAL

UPPAAL je integrované prostředí nástroj pro modelování, validaci a verifikaci real-time systémů modelovány jako sítě časovaných automatů, rozšířených s datovými typy (ohraničených celých čísel, pole, atd.)
UPPAAL CORA je pobočkou UPPAAL pro nákladově optimální dosažitelnost Anslysis vyvinutý UPPAAL týmem jako součást VHS a Ametist projekty. Vzhledem k tomu, UPPAAL podporuje kontrolu modelu časovaných automatů, UPPAAL CORA používá rozšíření časovaných automatů s názvem LPTA. LPTA vám umožňuje komentovat model s pojmem nákladů.
To může být náklady na zpoždění v určitých situacích nebo náklady jednotlivých akcí. UPPAAL CORA pak najde optimální cesty odpovídající branky podmínky.
Uppaal CORA byl použit v celé řadě případových studií. Některé z nich jsou popsány na stránce případové studie tohoto webu. Pokud jste přišli se zajímavými použití, prosím, kontaktujte nás. Máme zájem o jednání, co děláte!
Vzhledem k různým vnitřních datových struktur, UPPAAL CORA v současné době skládá ze dvou různých verzích:
Verze pro zjednodušený případ časové optimální analýzy dosažitelnosti.
Verze pro plné jazyk LPTA.
Stejně jako UPPAAL, UPPAAL CORA je zdarma pro použití neziskový, např pro vyhodnocení, výzkum a výuku.
Zde jsou některé klíčové rysy "UPPAAL":
Robustní
 
· Modeling Language of UPPAAL CORA je robustní vůči změnám v problému modelované. To znamená, že investice do modelování není ztracena při změně problém, protože je snadné upravit stávající vzor.
 
Rychlý
 
· I když technologie je poměrně nová, experimentální a velmi odlišné od technik používaných v tradičních operačního výzkumu, Uppaal CORA je konkurenceschopný v řadě případových studií.
 
Kompatibilní
 
· Jazyk UPPAAL CORA je podmnožinou UPPAAL. Jakýkoliv platný UPPAAL model je také platný modelem UPPAAL CORA. To umožňuje snadné a pohodlné, aby znovu použít a přizpůsobit své stávající modely UPPAAL CORA.
 
Aktuální
 
· UPPAAL CORA je založen na nejnovější verzi vnitřní rozvoje UPPAAL, obsahující nejnovější výkonu a jazykové vylepšení. Je to však experimentální nástroj a postrádá mnoho funkcí ověřování podle UPPAAL.
Omezení:
Uppaal CORA s plnou podporou LPTA má řadu omezení. Tato omezení nejsou zásadní, ale jsou výsledkem použití nové interní datové struktury se v současné době omezenou sadu funkcí. V průběhu času se tato omezení vyřešen.
- Ne extrapolace, tedy ukončení není zaručeno, pokud zaručí, že buď:
· Systém je acyklický.
· Všechny hodiny jsou ohraničeny invarianty.
- Pouze jednoduchá dosažitelnost:
· No živost kontrola
· Žádná kontrola zablokování
- Omezené použití vedení:
· Podpora (cena + zbývající) třídění je implementován (nejlépe první vyhledávání)
· Podpora pro heuristické proměnnou je implementována, ale výraz nemůže odkazovat na proměnné náklady.
Co je nového v této verzi:
· Tato verze opravuje pád chyby a nevracení paměti.