Model Checking

NUMMER:	211000
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
ANGEBOTEN IM:	jedes Sommersemester

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

- 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