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.
The benefits of buying summaries with Stuvia:
Guaranteed quality through customer reviews
Stuvia customers have reviewed more than 700,000 summaries. This how you know that you are buying the best documents.
Quick and easy check-out
You can quickly pay through credit card or Stuvia-credit for the summaries. There is no membership needed.
Focus on what matters
Your fellow students write the study notes themselves, which is why the documents are always reliable and up-to-date. This ensures you quickly get to the core!
Frequently asked questions
What do I get when I buy this document?
You get a PDF, available immediately after your purchase. The purchased document is accessible anytime, anywhere and indefinitely through your profile.
Satisfaction guarantee: how does it work?
Our satisfaction guarantee ensures that you always find a study document that suits you well. You fill out a form, and our customer service team takes care of the rest.
Who am I buying these notes from?
Stuvia is a marketplace, so you are not buying this document from us, but from seller SylvieS. Stuvia facilitates payment to the seller.
Will I be stuck with a subscription?
No, you only buy these notes for $3.20. You're not tied to anything after your purchase.
