Electronic System Level Design and Verification (HM-ES-th2 en HM-ES-pr2)
© Harry Broeders.
Deze pagina is bestemd voor studenten van de Haagse Hogeschool - Faculteit
Technologie, Innovatie & Samenleving groep E-EMSYS = minor Embedded Systems.
Let op! Deze pagina bevat mogelijk
verouderde informatie, kijk op Blackboard voor de meest recente informatie!
Inhoud
Inleiding
Het vak Electronic System Level Design and Verification houd zich bezig met
het hele gebied van Electronic System Level design van Embedded Systems en met
de verificatie van dit soort systemen. Je zult kennis maken de formele
verificatie methode "model checking" en je zult zelf een bepaald onderwerp uit
ESL design verder uitdiepen (en er een essay over schrijven) en presenteren aan
de klas.
Theorie HM-ES-th2
Beschikbaar materiaal:
Hoe schrijf je een essay? Zie: http://www1.aucegypt.edu/academic/writers/index.htm.
Deze link is helaas dood. Gelukkig heb ik deze print nog: How to Write an Essay.pdf.- Voorbeelden van essays uit het verleden:
- Voorbeelden van stellingen of vragen die je zou kunnen gebruiken als
onderwerp van je essay (maar het is natuurlijk veel leuker om zelf iets te
bedenken):
- Goed artikel over het gebruik van
SPIN en PROMELA.
Verplicht leesvoer! (behalve pagina 19 t/m 22)
- Nederland artikel over SPIN en PROMELA van
Hans van Tiel uit het blad Elektronica (2010). Aanbevolen leesvoer!
- Nederland
artikel over Formele Verificatie van Frits Vaandrager uit het blad
Bits&Chips (2012).
Aanbevolen leesvoer!
- Goed artikel over
model checking in het algemeen en de werking van SPIN in het bijzonder.
Alleen voor degene die het
leuk vind om eens een meer wetenschappelijk artikel te lezen (en niet bang
zijn van een beetje discrete wiskunde).
- SPIN refence card. met dank aan Mordechai Ben-Ari.
- Presentatie over SPIN en PROMELA.
- Small tutorial UPPAAL. Verplicht leesvoer!
- Full tutorial UPPAAL. Alleen voor degene die meer wil
weten. Bevat een duidelijke beschrijving van de Query Language (in
paragraaf 2.2).
- A
First Introduction to Uppaal. Aanbevolen leesvoer!
- Inhoud en sheets per les.
De sheets kunnen na afloop van een les nog worden bijgewerkt.
- Les 1 t/m 4
: SPIN en PROMELA.
- Les 1 en 2:
Introductie ESL en met de nadruk op validatie en verificatie.
Inleiding parallellisme en de problemen daarbij. Hele korte intro
SPIN en Promela. Huiswerk: Print +
Bestudeer artikel over het
gebruik van SPIN en PROMELA (behalve pagina 19 t/m 22). Zorg
dat je pagina 18 over Linear Temporal Logic (LTL) goed snapt! In
het laatste deel 22 t/m 27 kun je over de syntax van de commando's
heenlezen want wij gaan in het practicum niet zelf SPIN vanaf de
command line aanroepen maar we gaan de GUI JSpin gebruiken. De
begrippen die op pagina 22 t/m 27 worden besproken zijn echter wel
van belang.
- Les 3 en 4:
Introductie SPIN en PROMELA. Aan de hand van vragen die jullie
hebben naar aanleiding van het huiswerk + demo van het gebruik van
SPIN en PROMELA. Uitwerking van de kikker puzzel met SPIN en
PROMELA.
- Les 5, 6, 7 en 8: Schrijven essay.
Tijdens deze lessen wordt je ondersteund in het schrijven van je
essay.
- Les 9 en 10: UPPAAL.
Introductie UPPAAL met voorbeelden.
- Les 11 t/m 14: Presentaties van de essays.
- Promela voorbeelden:
- Drie oplossingen van de kikker puzzel die in les 4 is behandeld:
- frogs1.pml LTL: frogs1.prp In dit model wordt slechts 1
proces gebruikt.
- frogs2.pml LTL: frogs2.prp In dit model wordt voor elke
steen (of lelieblad) 1 proces gebruikt. Elk proces gebruikt
dezelfde code.
- frogs3.pml LTL: frogs3.prp In dit model wordt voor elke
kikker 1 proces gebruikt. Er zijn 2 verschillende soorten processen
(mannetjes en vrouwtjes)
- UPPAAL voorbeelden:
- ...
Toetsing
De toetsing bestaat uit 3 delen:
- Het schrijven van een essay. Proposal inleveren: 28 november 2014. Essay
inleveren 19 december 2014 voor 23:59 uur (eind week 5). Het essay
moet worden ingeleverd op Blackboard: https://blackboard.hhs.nl/webapps/eph-ephorus-assignment-bb_bb60/do/submitdoc?course_id=_45163_1&content_id=_1471791_1
- Het geven van een presentatie (in week 6 of 7). Zie voor het rooster: ES_1415_planning_presentaties_ES-th2.pdf.
De presentatie moet exact 10 min duren. Daarna zijn er nog 5 minuten
beschikbaar om vragen te beantwoorden. Het beoordelingsformulier voor de
presentatie vind je hier: ES_1415_beoordeling_presentatie.pdf.
- Het doen van een practicum op het gebied van model-checking. Het
practicum wordt afgesloten en beoordeeld in week 7 en de herkansing vindt
plaats in week 10.
Het essay en de presentatie worden beoordeeld met een cijfer en het
practicum met een Onvoldoende / Voldoende. Het eindcijfer is het gewogen
gemiddelde van de twee behaalde cijfers (het cijfer voor het essay telt 2x en
het cijfer voor de presentatie telt 1x) als het practicum een voldoende is. Als
het practicum onvoldoende is dan is het eindcijfer een 1. Het
beoordelingsformulier dat gebruikt wordt om het essay te beoordelen vind je
hier: Beoordelingsformulier_Essay.pdf.
JSpin installeren
Om JSpin te kunnen gebruiken heb je een werkende versie van de Java Virtual
Machine nodig. Op de meeste systemen zal Java al geïnstalleerd zijn. Zo niet
dan kun je het hier ophalen en vervolgens installeren: http://www.java.com/nl/download/manual.jsp
Om JSpin te installeren moet je de volgende files downloaden (of op school
kopiëren vanaf Q:\Grp_Elektrotechniek\Embedded_systems\downloads) en
installeren:
Als je onnodige warnings tijdens het verifiëren van Spin modellen wilt
voorkomen moet je in de file config.cfg regel 20:
C_COMPILER_OPTIONS=-o pan pan.c
vervangen door:
C_COMPILER_OPTIONS=-w -o pan pan.c
Indien nodig kun je dit instructiefilmpje bekijken waarin de installatie van
JSpin wordt voorgedaan: http://www.youtube.com/watch?v=UOr1iiuaKYY.
UPPAAL installeren
Om UPPAAL te kunnen gebruiken heb je een werkende versie van de Java Virtual
Machine nodig. Op de meeste systemen zal Java al geïnstalleerd zijn. Zo niet
dan kun je het hier ophalen en vervolgens installeren: http://www.java.com/nl/download/manual.jsp
Om UPPAAL te installeren moet je het volgende formulier invullen waarmee je
de file uppaal-4.0.14-aca.zip download (of deze file op school kopiëren van
Q:\Grp_Elektrotechniek\Embedded_systems\downloads).
Deze file uppaal-4.0.14-aca.zip moet je vervolgens uitpakken.
Practicum HM-ES-pr2
Opdrachten:
1-12-2013