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.
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.
