Formal Specification
- Announcement in HISLSF
- Time and Location: Mo 10:15 - 11:45, We 14:15 - 15:45, Leo 18
- Relevance: Master in Information Sytems
- Content:
- Algebraic Specification (OBJ, Maude)
- Model-based Specification (Z, B, VDM)
- Theorem Proving, Hoare Logic
- Model Checking
- Slides:
- Exercises:
- Every 14 days there will be an exercise
- Exercise sheet 1 - Solution slides
- Exercise sheet 2 - Solution slides
- Exercise sheet 3 - Solution slides
- Exercise sheet 4 - Solution slides
- Exercise sheet 5 - Solution slides
- Exercise sheet 6 - Solution slides
- Exercise slides 7
- Discussion forum:
- Moodle will be used to discuss the materials of this course.
- Moodle will be used to discuss the materials of this course.
- Links:
- Maude web pages (incl. manual)
- Maude book (LNCS 4350, available for free for WWU students via SpringerLink)
- Maude for Windows
- Z reference manual
- Z animator Jaza
- Input of Z-schemes in LaTeX-format for Jaza
- CTL model checker SMV (Manual)
- LTL model checker Spin
- Java Pathfinder
