Formele systeemmodellering voor software

Studiefiche
Vanaf academiejaar 2014-2015
Formele systeemmodellering voor software (E002021)
Cursusomvang
(nominale waarden; effectieve waarden kunnen verschillen per opleiding)
Studiepunten 6.0
Studietijd 180.0 u
Contacturen
67.5 u
Aanbodsessies en werkvormen in academiejaar 2014-2015
A (semester 2)
werkcollege: geleide oefeningen
werkcollege: PC-klasoefeningen
project
hoorcollege
Lesgevers in academiejaar 2014-2015
Laermans, Eric
TW05
Aangeboden in onderstaande opleidingen in 2014-2015
Bachelor of Science in de ingenieurswetenschappen:
computerwetenschappen
22.5 u
7.5 u
1.25 u
30.0 u
Verantwoordelijk lesgever
stptn
6
aanbodsessie
A
Onderwijstalen
Nederlands
Trefwoorden
Formele methoden, software, calculationele formele logica, functioneel
predicatenrekenen, kwantoren, formele semantiek, concurrency, geautomatiseerde
hulpmiddelen
Situering
Algemeen uitgangspunt: "Professional [software] engineers can often be distinguished
from other designers by the engineers' ability to use mathematical models to describe
and analyze their products." [David L. Parnas]. Daarom zal dit vak een
wetenschappelijke onderbouwing bieden voor de vakeigen aspecten van de opleiding
computerwetenschappen, en wel in voldoende mate om de student in staat te stellen
deze in de context van de andere vakken zelf verder uit te diepen en er de voordelen
van te genieten.
Inhoud
•
•
•
•
•
•
•
•
•
•
• Inleiding: Funmath als taal voor formele modellering, basisbegrippen
voor formeel rekenen
• Formele logica: calculationele propositielogica en predicatenlogica, met
• toepassingen in verzamelingenleer, functies, relaties; formele fundamenten voor
• inductie
• Formele specificatie en modellering voor software: functionele programma's,
• afleiding van Hoare-semantiek voor imperatieve programma's
• Formele specificatie en modellering van systemen met concurrency en
• tijdsafhankelijkheid: temporele calculus, TLA+/TLC, liveness- en fairness• voorwaarden
Begincompetenties
Wiskundige maturiteit, abstractievermogen, basisvorming programmeren en
programmeertalen
Eindcompetenties
• Calculationeel redeneren in de computerwetenschappen
• Vlot formeel rekenen met predicaten en kwantoren.
(Goedgekeurd)
1
•
•
•
•
•
Toepassen van modelleringswijzen op systeemspecificaties en op realisaties in
software.
Formeel redeneren over temporele logica's en temporele specificatiepatronen.
Opstellen van en redeneren over formele systeemmodellen in TLA+.
Werken met een model checker (i.h.b. TLC) en interpreteren van de resultaten.
Creditcontractvoorwaarde
Toelating tot dit opleidingsonderdeel via creditcontract is mogelijk mits gunstige beoordeling
van de competenties
Examencontractvoorwaarde
Dit opleidingsonderdeel kan niet via examencontract gevolgd worden
Didactische werkvormen
Hoorcollege, project, werkcollege: geleide oefeningen, werkcollege: PC-klasoefeningen
Toelichtingen bij de didactische werkvormen
Het project gaat over systeemmodellering en model checking.
Leermateriaal
• Cursusnota's (300 blz.) (download gratis).
• Lamport, Leslie, Specifying systems: the TLA+ language and tools for hardware and
• software engineers, Boston (Mass.) : Addison-Wesley, 2003. ISBN: 032114306X
• Location: T56.CD265
• Softwarehulpmiddelen: TLA+, TLC (alle gratis download).
Referenties
• Raymond Boute, Functional Mathematics: a Unifying Formal Approach to Modeling
• Systems, Circuits and Programs, 2008 (free download)
• Gries, David and Schneider, Fred B., A logical approach to discrete math, New York
• (N.Y.) : Springer, 1995. ISBN: 0-387-94115-0 Location: T57.W.0287
• Lamport, Leslie, Specifying systems: the TLA+ language and tools for hardware and
• software engineers, Boston (Mass.) : Addison-Wesley, 2003. ISBN: 032114306X
• Location: T56.CD265 (gratis download)
• Apt, Krzysztof R. and Olderog, E.-R., Verification of sequential and concurrent
• programs, New York : Springer-Verlag, 1997. ISBN: 0387948961 Location: T56.
• CF068
• Holzmann, Gerard J., The spin model checker: primer and reference manual, Boston,
• MA : Addison-Wesley, 2004. ISBN: 0-321-22862-6 Location: TBBS.TA168.H65
• Roever, W.-P. de, Concurrency verification: introduction to compositional and
• noncompositional methods, New York : Cambridge University Press, 2001. ISBN:
• 0521806089 Location: T57.C.0548
Vakinhoudelijke studiebegeleiding
Evaluatiemomenten
periodegebonden en niet-periodegebonden evaluatie
Evaluatievormen bij periodegebonden evaluatie in de eerste examenperiode
Openboekexamen
Evaluatievormen bij periodegebonden evaluatie in de tweede examenperiode
Openboekexamen
Evaluatievormen bij niet-periodegebonden evaluatie
Verslag
Tweede examenkans in geval van niet-periodegebonden evaluatie
Examen in de tweede examenperiode is mogelijk
Toelichtingen bij de evaluatievormen
• Periodegebonden evaluatie: schriftelijk (oefeningen)examen met open boek.
• Niet-periodegebonden evaluatie: beoordeling van het ingezonden werkstuk;
• frequentie: 1 project met deadline op het einde van de lessenperiode.
Eindscoreberekening
De evaluatie van het project (verslag + code) telt voor 30% van de eindscore. De
overige 70% wordt bepaald door het examen.
(Goedgekeurd)
2

Download Report