Model Checking

NUMMER:	150324
KÜRZEL:	ModCh
MODULBEAUFTRAGTE:R:	Prof. Dr. Thomas Zeume
DOZENT:IN:	Prof. Dr. Thomas Zeume
FAKULTÄT:	Fakultät für Informatik
SPRACHE:	Deutsch
SWS:	4
CREDITS:	5
WORKLOAD:
ANGEBOTEN IM:	jedes Wintersemester

BESTANDTEILE UND VERANSTALTUNGSART

Be­ginn: Don­ners­tag den 29.​10.​2020 Vor­le­sung Don­ners­tags: ab 10:00 bis 12.​00 Uhr im On­line Übung: siehe "Sons­ti­ges"

LERNFORM

Win­ter­se­mes­ter 2020/2021 Die Or­ga­ni­sa­ti­on und sämt­li­che Kurs­ak­ti­vi­tä­ten er­fol­gen über einen Mood­le-Kurs. Mood­le-Kurs: https://​moodle.​ruhr-uni-bo­chum.​de/​m/​course/​view.​php?​id=32921

LERNZIELE

In die­ser Ver­an­stal­tung wer­den die theo­re­ti­schen Grund­la­gen des Model Che­ckings ver­mit­telt, mit einem Fokus auf lo­gik-ba­sier­ten Spe­zi­fi­ka­ti­ons­spra­chen. Die Spe­zi­fi­ka­ti­ons­spra­chen LTL und CTL wer­den ein­ge­führt, ihre Aus­drucks­stär­ke un­ter­sucht, und die wich­tigs­ten al­go­rith­mi­schen An­sät­ze für das Model Che­cking vor­ge­stellt. Diese Ver­an­stal­tung rich­tet sich an Stu­die­ren­de der Ma­the­ma­tik, In­for­ma­tik und ITS.

INHALT

Wie kann die Kor­rekt­heit von Soft­ware und Hard­ware for­mal über­prüft wer­den? Im Model Che­cking wer­den Soft­ware- und Hard­ware-Mo­du­le durch Tran­si­ti­ons­sys­te­me for­ma­li­siert; ge­wünsch­te Ei­gen­schaf­ten mit Hilfe lo­gi­scher For­ma­lis­men for­mal be­schrie­ben; und mit Hilfe von Al­go­rith­men au­to­ma­ti­siert über­prüft, ob ein Tran­si­ti­ons­sys­tem eine for­mal spe­zi­fi­zier­te Ei­gen­schaft be­sitzt.

VORAUSSETZUNGEN CREDITS

Bestandene Modulabschlussprüfung

EMPFOHLENE VORKENNTNISSE

- Grund­la­gen­vor­le­sun­gen Ma­the­ma­tik

- Ein­füh­rung in die Theo­re­ti­sche In­for­ma­tik (ggf. kann das nö­ti­ge Wis­sen auch nach­ge­holt wer­den)

- Hilf­reich: Logik in der In­for­ma­tik, Da­ten­struk­tu­ren und ele­men­ta­re Pro­gram­mier­kennt­nis­se

LITERATUR

1. Clar­ke, Ed­mund M., Grum­berg, Orna, Kro­ening, Da­ni­el, Peled, Doron, Veith, Hel­mut "Model Che­cking", MIT Press, 2018
2. Baier, Christel, Ka­to­en, Joost-Pie­ter "Prin­ci­ples of Model Che­cking", MIT Press, 2008