Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen


 




Zeige Wirtschaftsinformatik-Format Pdf_icon Digitale Medien-Format Pdf_icon Informatik-Format Pdf_icon Systems Engineering-Format Pdf_icon

Informatik-Ansicht

Formale Methoden der Softwaretechnik (deleted:Thu Jan 14 16:49:41 +0100 2016)


Formal Methods in Software Engineering 		Modulnummer
MB-699.05
Master
Pflicht/Wahl
Wahl Basis Ergänzung
Sonderfall
Zugeordnet zu Masterprofil
Basis Ergänzung
Sicherheit und Qualität
KI, Kognition, Robotik
Digitale Medien und Interaktion
Modulbereich : Mathematik und Theoretische Informatik
Modulteilbereich : 699 Spezielle Gebiete der Theoretischen Informatik
Anzahl der SWS
V UE K S Prak. Proj. ∑
0 0 4 0 0 0 4
Kreditpunkte : 6 Turnus

i. d. R. angeboten alle 2 Semester

Formale Voraussetzungen : -
Inhaltliche Voraussetzungen : Logik, Formale Modellierung
Vorgesehenes Semester : ab 1. Semester
Sprache : Deutsch
Ziele :

Die Studierenden verfügen über:

  • Vertiefte Kenntnisse in der Methodik formaler (logikbasierter) Systemspezifikation und -verifikation
  • Verständnis von dafür verwendeten Beweis- und Analyseverfahren, insbesondere formaler Kalküle und ihrer Algorithmen
  • Fähigkeit zur Verwendung formaler Modellierungs- und Verifikationswerkzeuge
  • Fähigkeit zur Auswahl geeigneter Werkzeuge und Verfahren für praktische Fragestellungen
Inhalte :
  • Modellierung mit Logik erster und höherer Stufe, sowie sowie mit Temporallogiken
  • Einführung in interaktive Modellierungswerkzeuge und Theorembeweiser
  • Ausgewählte Beweisverfahren wie Modellprüfung (Modelchecking, Resolutionsbeweisen, Tableauverfahren)
  • Semantik imperativer Sprachen und darauf basierende Verifikationskalküle
Unterlagen (Skripte, Literatur, Programme usw.) :

Ausgewählte Texte aus folgenden:

  • T. Nipkow, L. C. Paulson, M. Wenzel: Isabelle/HOL, a Proof Assistant for Higher-Order Logic. Springer 2002.
  • M. R. Huth and M. D. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
  • G. Winskel: The formal semantics of programming languages, MIT Press, 1993.
  • Edmund M. Clarke, Orna Grumberg and Doron Peled: Model Checking, MIT Press, 1999.
  • D. van Dalen: Logik and Structure, Springer 2004.

Sowie Papiere und Handbücher auf der Webseite der Veranstaltung.
Form der Prüfung : i.d.R. Bearbeitung von Übungsaufgaben und Fachgespräch oder mündliche Prüfung
Arbeitsaufwand
Präsenz 56
Übungsbetrieb/Prüfungsvorbereitung 124
Summe 180 h
Lehrende: PD Dr. C. Lüth, PD Dr. T. Mossakowski Verantwortlich PD Dr. C. Lüth
Zurück

Zeige Wirtschaftsinformatik-Format Pdf_icon Digitale Medien-Format Pdf_icon Informatik-Format Pdf_icon Systems Engineering-Format Pdf_icon