Navigation Fachbereich und Zentren:
wissen.leben | WWU Münster
Formal Specification
- Announcement in HISLSF
- Time and Location: Mo 10:15 - 11:45, We 14:15 - 15:45, Leo 18
- Exam: Feb. 03, 2010, 14:15-15:45 h, Leo 18
- Post-exam Review: Apr. 13, 2010, 13:00-15:00 h, room 338 (WI)
- Start: October 14, 2009
- Relevance: Master in Information Sytems
- Content:
- Algebraic Specification (OBJ, Maude)
- Model-based Specification (Z, B, VDM)
- Soundness Proofs, Hoare Logic
- Theorem Proving (Isabelle)
- Model Checking
- Slides:
- Chapter 1: Introduction (state: Oct. 12, 2009)
- Chapter 2: Algebraic Specification (state: Oct. 21, 2009; typos on slides 19,22,23,26,35,37 corrected)
- Chapter 3: Basics of Logic (state: Oct. 20, 2009)
- Chapter 4: Specification Language Z (state: Nov. 23, 2009)
- Chapter 5: Theorem Proving (state: Nov. 23, 2009)
- Chapter 6: Model Checking, Part 1 (state: Dec. 10, 2009)
- Chapter 6: Model Checking, Part 2 (state: Feb. 01, 2010; colors on slide 129 corrected)
- Discussion forum:
OpenUSS will be used to discuss the materials of this course. Please navigate to "WWU > FB04 > PI > FS-WS 09/10"
- E-Assessment system:
The E-Assessment system EASy will be used to support the processing of Exercise 5 (Hoare Logic).
Access to EASy is exclusively possible from the WWU network or via VPN client.
The Demo Slides may help you to familiarise with EASy.
