FIT3013 - Formal specification for software engineering - 2018

Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications; the role of formal specifications in software engineering. The Event-B notation, the role of proof obligations and refinement, the LTL and CTL temporal logics, the model checking approach and techniques.

At the completion of this unit, students should be able to:

1. articulate the role and importance of formal modelling and verification;
2. develop Event-B specifications;
3. apply Rodin to analyse an Event-B specification and verify proof obligations;
4. distinguish and evaluate the trade-offs in system modelling using Event-B and temporal logics;
5. develop basic specifications and formulate properties in temporal logics;
6. utilise a model checker to verify such properties.

Examination (2 hours): 50%; In-semester assessment: 50%

Minimum total expected workload equals 12 hours per week comprising:

1. Contact hours for on-campus students:
   • Two hours of lectures
   • One 2-hour tutorial/lab
2. Additional requirements (all students):
   • A minimum of 8 hours independent study per week for completing lab and project work, private study and revision.

See also Unit timetable information

http://www.infotech.monash.edu.au/units/