UPPAAL

Uppaal is een geïntegreerde tool-omgeving voor het modelleren, validatie en verificatie van real-time systemen gemodelleerd als netwerken van getimede automaten, uitgebreid met types data (begrensd gehele getallen, arrays, enz.).
Uppaal CORA is een tak van Uppaal voor Cost Optimal Bereikbaarheid Anslysis ontwikkeld door het Uppaal team als onderdeel van de VHS en AMETIST projecten. Overwegende Uppaal ondersteunt model checking van getimede automaten, Uppaal CORA maakt gebruik van een uitbreiding van getimede automaten genoemd LPta. LPta kunt u het model met de notie van kosten annoteren.
Dit kan de kosten van de vertraging in bepaalde situaties of de kosten van bepaalde acties. Uppaal CORA vindt dan optimale paden bijpassende doel omstandigheden.
Uppaal CORA is gebruikt in een aantal case studies. Sommige van deze worden beschreven op de pagina case study van deze site. Als u komen met interessante toepassingen, gelieve ons te contacteren. Wij zijn geïnteresseerd in wat je doet!
Vanwege de verschillende interne datastructuren, Uppaal CORA bestaat momenteel uit twee verschillende versies:
Een versie voor de vereenvoudigde geval van tijd optimale bereikbaarheid analyse.
Een versie voor de volledige taal van LPta.
Net Uppaal, Uppaal CORA is gratis voor niet-commercieel gebruik, zoals voor de evaluatie, onderzoek en onderwijs doeleinden.
Hier zijn een aantal belangrijke eigenschappen van "Uppaal":
Robuust
 
· De modelleertaal van Uppaal CORA is robuust in de richting van de veranderingen in het probleem gemodelleerd. Dit betekent dat de investering in technieken leidt niet verloren gaat wanneer het probleem verandert, omdat het gemakkelijk is om het bestaande model aan te passen.
 
Snel
 
· Hoewel de technologie is vrij nieuw, experimenteel en zeer verschillend van technieken die gebruikt worden in de traditionele operationeel onderzoek, Uppaal CORA concurrerend is in een aantal case studies.
 
Compatibel
 
· De taal van Uppaal CORA is een superset van Uppaal. Elke geldige Uppaal model is ook een geldig Uppaal CORA model. Dit maakt het gemakkelijk en handig om hergebruik en uw bestaande modellen aan te passen aan Uppaal CORA.
 
Actueel
 
· Uppaal CORA is gebaseerd op de meest recente interne ontwikkeling versie van Uppaal, met daarin de laatste prestaties en taal verbeteringen. Het is echter een experimenteel hulpmiddel en mist veel van de verificatie kenmerken van Uppaal.
Beperkingen:
Uppaal CORA vol LPta drager een aantal beperkingen. Deze beperkingen zijn niet fundamenteel, maar zijn een gevolg van het gebruik van nieuwe interne gegevens structuren met een momenteel beperkt feature set. Na verloop van tijd zullen deze beperkingen worden opgelost.
- Geen extrapolatie, vandaar de beëindiging is niet gegarandeerd, tenzij u garanderen dat ofwel:
· Het systeem is acyclisch.
· Alle klokken worden begrensd door invarianten.
- Alleen eenvoudige bereikbaarheid:
· Geen liveness check
· Geen impasse check
- Beperkt gebruik van geleiding:
· Ondersteuning voor (kosten + resterende) sorteren wordt uitgevoerd (beste eerste zoekopdracht)
· Ondersteuning voor heuristische variabele wordt uitgevoerd, maar de expressie kan niet verwijzen naar de variabele kosten.
Wat is er nieuw in deze release:
· Deze versie verhelpt crash bugs en een geheugenlek.