Sprawdzanie modelu Uppaal
| Deweloperzy |
Uniwersytet w Uppsali Uniwersytet w Aalborgu |
|---|---|
| Pierwsze wydanie | 1995 |
| Wersja stabilna | 4.0.14 / 20 maja 2014
|
| Wersja podglądu | 4.1.22 / 28 marca 2019
|
| Napisane w | C++ i GUI w Javie |
| System operacyjny |
Linux Mac OS X Microsoft Windows |
| Dostępne w | Angielski Duński Japoński Chiński Litewski |
| Typ | Sprawdzenie modelu |
| Licencja |
Licencje komercyjne Licencje akademickie |
| Strona internetowa | http://www.uppaal.org/ http://www.uppaal.com/ |
UPPAAL jest zintegrowanym środowiskiem narzędziowym do modelowania , walidacji i weryfikacji systemów czasu rzeczywistego modelowanych jako sieci automatów czasowych , rozszerzonych o typy danych (liczby całkowite ograniczone, tablice itp.).
Został użyty w co najmniej 17 studiach przypadków od czasu jego wydania w 1995 roku, w tym w Lego Mindstorms , w protokole audio Philips oraz w kontrolerach skrzyni biegów dla Mecel .
Narzędzie zostało opracowane we współpracy między grupą Design and Analysis of Real-Time Systems na Uniwersytecie w Uppsali w Szwecji oraz Basic Research in Computer Science na Uniwersytecie w Aalborgu w Danii .
Dostępne są następujące rozszerzenia:
- Cora do analizy osiągalności optymalnej pod względem kosztów.
- Tron do testowania systemów czasu rzeczywistego ON-line (testowanie zgodności czarnej skrzynki).
- Pokrycie dla COVERerage-optymalnego generowania testów off-line.
- Tiga do syntezy kontrolerów opartej na grach TImed.
- Port dla systemów czasowych opartych na komponentach, wykorzystujący techniki częściowej redukcji zamówień.
- Pro dla PRObabilistycznej analizy osiągalności. (wycofany)
- SMC do sprawdzania modeli statystycznych.
Linki zewnętrzne
- Witryna akademicka UPPAAL
- Witryna handlowa UPPAAL
- Zespół Projektowania i Analizy Systemów Czasu Rzeczywistego
- Jednostka DEIS, Wydział Informatyki na AAU
Kategorie: