Die Vorbesprechung findet am Donnerstag, 17.10.2013 ab 12:00 Uhr in O27-412 statt.

Mit formalen Spezifikationssprachen lassen sich nicht nur Anforderungen an Systeme präzise formulieren, sondern auch Eigenschaften (wie etwa Sicherheit oder Lebendigkeit) beweisen oder logische Schlussfolgerungen ziehen, die z.B. herangezogen werden können, um die Plausibilität und die Adäquatheit der Anforderungen zu überprüfen.

Das Seminar befasst sich mit verschiedenen aktuellen formalen Spezifikationssprachen (z.B. ASM, CafeOBJ, RAISE, TLA+, VDM und Z), ihrer Semantik und der Art und Weise, wie man damit Beweise führen kann.

• D. Bjørner und M. C. Henson (Herausgeber): Logics of Specification Languages. Monographs in Theoretical Computer Science, Springer, 2008.