UPPAAL

UPPAAL to zintegrowane środowisko narzędziem do modelowania, walidacji i weryfikacji systemów czasu rzeczywistego modelowanych jako sieci automatów czasowych, rozbudowane typy danych (tablice ograniczonych liczb całkowitych, etc.).
UPPAAL CORA jest oddział UPPAAL dla optymalnej kosztowo osiągalności Anslysis opracowany przez UPPAAL zespołu w ramach projektów VHS i ametist. Podczas gdy UPPAAL obsługuje modelu sprawdzanie automatów czasowych, UPPAAL CORA wykorzystuje rozszerzenie automatów czasowych o nazwie LPTA. LPTA pozwala na opisywanie model z pojęciem kosztu.
Może to być koszt opóźnienia w pewnych sytuacjach lub kosztu poszczególnych działań. UPPAAL CORA odnajduje optymalne ścieżki dopasowania warunków karnego.
UPPAAL CORA został wykorzystany w wielu studiach przypadku. Niektóre z nich są opisane na stronie studium przypadku z tej strony. Jeśli pochodzą z ciekawych zastosowań, prosimy o kontakt. Jesteśmy zainteresowani tym co robisz!
Ze względu na różne wewnętrznych struktur danych, UPPAAL CORA składa się obecnie z dwóch różnych wersjach:
Wersja dla uproszczonego przypadku czasu optymalnej analizy zdolności odbiorczej.
Wersja dla pełnego języku LPTA.
Jak UPPAAL, UPPAAL CORA jest darmowy do użytku non-profit, np do oceny, badań i celów dydaktycznych.
Oto kilka kluczowych cech "UPPAAL":
Krzepki
 
· Język modelowania UPPAAL CORA jest solidna kierunku zmian problemu wzorowany. Oznacza to, że inwestycja w modelowaniu nie jest stracone, gdy zmienia się problemem, ponieważ jest łatwy do przystosowania istniejącego modelu.
 
Szybko
 
· Chociaż technologia jest dość nowy, eksperymentalny i bardzo różni się od technik stosowanych w tradycyjnych badań operacyjnych, UPPAAL CORA jest konkurencyjna w wielu studiach przypadku.
 
Zgodny
 
· Język UPPAAL CORA jest rozszerzeniem UPPAAL. Wszelkie ważne jest również modelem UPPAAL Model UPPAAL ważny CORA. Umożliwia to łatwe i wygodne do ponownego wykorzystania i dostosowania istniejących modeli UPPAAL CORA.
 
Prąd
 
· UPPAAL CORA jest oparty na najnowszej wersji rozwojowej wewnętrznej UPPAAL, zawierający najnowsze ulepszenia wydajności i językowych. Jest to jednak narzędzie eksperymentalne i brakuje mu wielu funkcji weryfikacji, o UPPAAL.
Ograniczenia:
UPPAAL CORA z pełną obsługą LPTA posiada szereg ograniczeń. Ograniczenia te nie mają fundamentalne znaczenie, ale są wynikiem korzystania z nowych wewnętrznych struktur danych z obecnie ograniczony zestaw funkcji. Z biegiem czasu, ograniczenia te zostaną rozwiązane.
- Nie ekstrapolacja, więc rozwiązanie jest gwarantowana, chyba że nie gwarantuje, że:
· System jest acykliczny.
· Wszystkie zegary są ograniczone niezmienników.
- Tylko Proste osiągalność:
· Nie liveness wyboru
· Nie check impasu
- Ograniczone wykorzystanie przewodnich:
· Wsparcie dla (+ pozostałe koszty) sortowanie jest realizowany (najlepiej pierwszy wyszukiwania)
· Wsparcie dla zmiennej heurystycznej jest realizowany, ale wyrażenie nie może odnosić się do kosztów zmiennych.
Co nowego w tym wydaniu:
· To wydanie naprawia błędy i ruina przecieku pamięci.