Model Checking

NUMMER: 150324
KÜRZEL: ModCh
DOZENT: Prof. Dr. Thomas Zeume
FAKULTÄT: Center of Computer Science
SPRACHE: Deutsch
SWS: 4
CREDITS: 5
WORKLOAD:
ANGEBOTEN IM: jedes Wintersemester

INFOS

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"


PRÜFUNGUNGSFORM

Ter­min nach Ab­spra­che mit dem Do­zen­ten. Prü­fungs­form: münd­lich Prü­fungs­an­mel­dung: Flex­Now Dauer: 30min


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

keine


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