In dit document zit een samenvatting van het onderwerp model-checking uit informatica-actief. Programmeertaal in Uppaal word beschreven, inclusief een uitgebreide en overzichtelijke begrippenlijst.
Informatica samenvatting Model Checking
Model Checking = een succesvolle methode om te bewijzen dat een ontwerp van een
computersysteem voldoet aan de eisen die er aan gesteld worden.
- Als invoer een ontwerp van een systeem (het "model") en een eigenschap
(de "specificatie") waaraan het systeem moet voldoen.
In CTL betekent:
E: "Er bestaat een pad waarvoor geldt dat"
A: "Voor alle paden geldt dat"
< >: "uiteindelijk"
[ ] "altijd"
Eis Model Checking is dat er sprake is van toestanden en van transities (overgangen) tussen
toestanden.
Wanneer je eenmaal een model hebt gemaakt met Uppaal kun je er twee dingen mee doen.
Allereerst kun je het model simuleren, dat wil zeggen stapsgewijs van de ene naar de andere
toestand springen. Daarnaast kun je ook eigenschappen van het model verifiëren ("model
checken").
Uppaal is ontwikkeld door onderzoekers uit Uppsala (Zweden) en Aalborg (Denemarken),
met hulp van andere onderzoeksgroepen, waaronder een groep van de Radboud Universiteit
in Nijmegen.
&& is Uppaal notatie voor 'en', net als in veel andere programmeertalen. Ook staat || voor
'of'. als...dan schrijf je in Uppaal met imply. == staat voor ‘wanneer’
Wanneer je geen grenzen noemt en kortweg int jobs; declareert, dan is impliciet de minimale
waarde van jobs -32768 en de maximale waarde 32768.
- Ondergrenzen kunnen aan timing worden beschreven met behulp van guards.
- Bovengrenzen geven aan timing: dit doen we met behulp van
zogenaamde invarianten.
Wanneer het systeem in een toestand komt met een committed locatie komt, dan moet altijd
eerst een transitie vanuit een committed locatie plaatsvinden.
In Uppaal kun je twee soorten parameters declareren: Call-by-value parameters en call-by-
reference parameters. In het eerste geval geef je alleen de waarde (value) van een variabele
door. De variabele zelf kun je niet veranderen. Bij call-by-reference geef je de hele variabele
door en kun je de waarde van de variabele ook veranderen. De ampersand & voor de naam
geeft aan dat de parameter werkt volgens call-by-reference. Wanneer je alleen de naam
gebruikt hanteert Uppaal call-by-value. Wanneer je in Uppaal klokken of kanalen als
parameter gebruikt, moet je deze aanroepen als call-by-reference.
Voordelen van het kopen van samenvattingen bij Stuvia op een rij:
Verzekerd van kwaliteit door reviews
Stuvia-klanten hebben meer dan 700.000 samenvattingen beoordeeld. Zo weet je zeker dat je de beste documenten koopt!
Snel en makkelijk kopen
Je betaalt supersnel en eenmalig met iDeal, creditcard of Stuvia-tegoed voor de samenvatting. Zonder lidmaatschap.
Focus op de essentie
Samenvattingen worden geschreven voor en door anderen. Daarom zijn de samenvattingen altijd betrouwbaar en actueel. Zo kom je snel tot de kern!
Veelgestelde vragen
Wat krijg ik als ik dit document koop?
Je krijgt een PDF, die direct beschikbaar is na je aankoop. Het gekochte document is altijd, overal en oneindig toegankelijk via je profiel.
Tevredenheidsgarantie: hoe werkt dat?
Onze tevredenheidsgarantie zorgt ervoor dat je altijd een studiedocument vindt dat goed bij je past. Je vult een formulier in en onze klantenservice regelt de rest.
Van wie koop ik deze samenvatting?
Stuvia is een marktplaats, je koop dit document dus niet van ons, maar van verkoper SylvieS. Stuvia faciliteert de betaling aan de verkoper.
Zit ik meteen vast aan een abonnement?
Nee, je koopt alleen deze samenvatting voor €2,99. Je zit daarna nergens aan vast.
