UPPAAL

UPPAAL е интегрирана среда инструмент за моделиране, утвърждаване и проверка на системите за реално време, моделирани като мрежи от навременна автомати, удължени с типове данни (обградени числа, масиви, и т.н.).
UPPAAL CORA е клон на UPPAAL за оптимална цена Достъпност Anslysis разработен от UPPAAL, след като част от проектите на VHS и Аметист. Като има предвид, UPPAAL подкрепя модел проверка на навременна автомати, UPPAAL CORA използва разширение на навременна автомати нарича LPTA. LPTA ви позволява да поясняват модела с понятието разходи.
Това може да бъде стойността на забавяне в някои ситуации или стойността на определени действия. След UPPAAL CORA намира оптимални маршрути съвпадение условия за гол.
UPPAAL CORA е бил използван в редица казуси. Някои от тях са описани в страницата на този сайт казус. Ако излезе с интересни приложения, моля свържете се с нас. Ние сме заинтересовани в изслуша това, което правите!
Поради различни вътрешни структури от данни, UPPAAL CORA понастоящем се състои от два различни варианта:
Версия за опростена случай на времето оптимален анализ на достъпност.
Версия за пълния езика на LPTA.
Подобно UPPAAL, UPPAAL CORA е безплатна за използване с нестопанска цел, напр за оценка, изследване и образователна цел.
Ето някои основни характеристики на "UPPAAL":
Здрав
 
· Езикът моделиране на UPPAAL CORA е стабилна към промени в проблема моделирани. Това означава, че вашата инвестиция в моделирането не се губи, когато се променя на проблема, тъй като то е лесно да се адаптират съществуващия модел.
 
Бърз
 
· Въпреки че технологията е доста нов, експериментален и много различен от техники, използвани в традиционната изследване на операциите, UPPAAL CORA е конкурентна в редица казуси.
 
Съвместим
 
· Езикът на UPPAAL CORA е надмножество на UPPAAL. Всяко валидно UPPAAL модел също е валиден UPPAAL CORA модел. Това го прави лесен и удобен за повторната употреба и адаптиране на съществуващите си модели, за да UPPAAL CORA.
 
Ток
 
· UPPAAL CORA се основава на най-новата версия вътрешния развитие на UPPAAL, съдържаща най-новите подобрения в производителността и език. Тя обаче е експериментален инструмент и няма много от функциите за проверка на UPPAAL.
Ограничения:
UPPAAL CORA с пълна поддръжка LPTA има редица ограничения. Тези ограничения не са основни, но са резултат от използването на нови вътрешни структури от данни с ограничената понастоящем набор от функции. С течение на времето, тези ограничения ще бъдат решени.
- Не екстраполация, а оттам прекратяване не е гарантирана, освен ако не ви гарантира, че:
· Системата е ациклична.
· Всички часовници са обградени с инварианти.
- Simple достижимост само:
· Не liveness проверка
· Не проверка безизходица
- Ограничено използване на направляваща:
· Подкрепа за (цена + оставащото) за сортиране се осъществява (най-добре първо търсене)
· Подкрепа за евристично променлива се осъществява, но изразът не може да се отнася до променлива цена.
Какво е новото в тази версия:
· Тази версия поправя краш бъгове и теч на паметта.