Uppaal Model Denetleyicisi - Uppaal Model Checker

UPPAAL
Geliştirici (ler)Uppsala Üniversitesi
Aalborg Üniversitesi
İlk sürüm1995 (1995)
Kararlı sürüm
4.0.14 / 20 Mayıs 2014; 6 yıl önce (2014-05-20)
Önizleme sürümü
4.1.22 / 28 Mart 2019; 19 ay önce (2019-03-28)
YazılmışC ++ ve GUI içinde Java
İşletim sistemiLinux
Mac OS X
Microsoft Windows
Uyguningilizce Danimarka dili Japonca Çince Litvanyalı
TürModel kontrolü
LisansTicari Lisanslar
Akademik Lisanslar
İnternet sitesihttp://www.uppaal.org/ http://www.uppaal.com/

UPPAAL entegre araç çevre için modelleme, doğrulama ve doğrulama gerçek zaman ağları olarak modellenen sistemler zamanlı otomata, ile genişletildi veri tipleri (sınırlı tam sayılar, diziler vb.).

1995 yılında piyasaya sürülmesinden bu yana en az 17 vaka incelemesinde kullanılmıştır. Lego Mindstorms, için Philips ses protokolü ve şanzıman kontrolörlerinde Mecel.[1]

Araç, Gerçek Zamanlı Sistemlerin Tasarımı ve Analizi grubunun işbirliği ile geliştirilmiştir. Uppsala Üniversitesi, İsveç ve Bilgisayar Bilimlerinde Temel Araştırma Aalborg Üniversitesi, Danimarka.

Aşağıdaki uzantılar mevcuttur:

  • Cora Optimum Maliyet Erişilebilirlik Analizi için.
  • Tron Gerçek zamanlı sistemleri ON-line Test Etmek için (kara kutu uygunluk testi).
  • Örtmek KAPSAM-optimum çevrimdışı test üretimi için.
  • Tiga TImed GAmes tabanlı kontrolör sentezi için.
  • Liman Bileşen tabanlı zamanlamalı sistemler için, Kısmi Sipariş Azaltma Tekniklerinden yararlanma.
  • Pro Olasılıklı erişilebilirlik analizi için. (Üretimi durduruldu)
  • SMC İstatistiksel Model Kontrolü için.

Referanslar

  1. ^ "Durum çalışmaları".

Dış bağlantılar