UPPAAL

UPPAAL este un mediu instrument integrat pentru modelarea, validare și verificare a sistemelor în timp real modelat ca rețele de automate temporizate, acordate cu tipuri de date (numere întregi delimitate, tablouri, etc.).
UPPAAL CORA este o ramură a UPPAAL pentru cost optim Accesibilitatea Anslysis dezvoltat de echipa UPPAAL ca parte a proiectelor VHS și Ametist. Întrucât UPPAAL sprijină modelul verificarea automate temporizat, UPPAAL CORA foloseste o extensie de automate temporizate numit LPTA. LPTA vă permite să adnota modelul cu noțiunea de cost.
Acest lucru poate fi costul de întârziere în anumite situații sau costul anumitor acțiuni. UPPAAL CORA găsește apoi căi optime potrivite condiții gol.
UPPAAL CORA a fost folosit într-o serie de studii de caz. Unele dintre acestea sunt descrise pe pagina de studiu de caz a acestui site. Dacă ați veni cu utilizari interesante, vă rugăm să ne contactați. Suntem interesați să auzim ceea ce faci!
Datorită diferitelor structuri de date interne, UPPAAL CORA format în prezent din două versiuni diferite:
O versiune pentru cazul simplificat de timp de analiza optim accesibilitatea.
O versiune pentru limba plin de LPTA.
Ca UPPAAL, UPPAAL CORA este gratuit pentru uz non-profit, de exemplu, pentru evaluare, cercetare, și în scopuri didactice.
Iată câteva caracteristici cheie ale "UPPAAL":
Robust
 
· Limbajul de modelare a UPPAAL CORA este robust spre schimbări în problema modelat. Acest lucru înseamnă că investiția în modelare nu este pierdut în cazul în care problema se schimbă, deoarece este ușor să se adapteze modelul existent.
 
Rapid
 
· Desi tehnologia este destul de nou, experimental și foarte diferit de tehnici utilizate în cercetarea operațională tradițional, UPPAAL CORA este competitivă într-o serie de studii de caz.
 
Compatibil
 
· Limbajul UPPAAL CORA este un superset de UPPAAL. Orice model UPPAAL valabil, de asemenea, un model de UPPAAL CORA valabil. Acest lucru îl face ușor și convenabil de a reutiliza și să adapteze modelele existente la UPPAAL CORA.
 
Curent
 
· UPPAAL CORA se bazează pe cea mai recentă versiune de dezvoltare internă a UPPAAL, care conține cele mai recente îmbunătățiri de performanță și de limbă. Este totuși un instrument experimental și nu are multe din caracteristicile de verificare a UPPAAL.
Limitări:
UPPAAL CORA cu suport complet LPTA are o serie de limitări. Aceste restricții nu sunt fundamentale, dar sunt un rezultat de utilizare a noilor structuri de date interne cu un set de caracteristici limitat în prezent. De-a lungul timpului, aceste limitări vor fi rezolvate.
- Nu extrapolare, prin urmare, încetarea nu este garantat decât dacă garantează că:
· Sistemul este aciclic.
· Toate ceasurile sunt delimitate de invarianți.
- Numai de accesibilitate simplă:
· Nu verificare vivacitatea
· Nu verificare impas
- Utilizarea limitată a directoare:
· Suport pentru sortare (cost rămas +) este pusă în aplicare (cel mai bine prima căutare)
· Suport pentru variabila euristica este pus în aplicare, dar expresia nu se poate referi la variabila de cost.
Ce este nou în această versiune:
· Această versiune rezolvă bug-uri de avarie și o scurgere de memorie.