This unit replaces CSE4213 in the new Bachelor of Software Engineering structure. It is largely unchanged from that unit, although this description is more up-to-date.

29/05/2014 - Change tutorial from 1 hour to 2 hours.

14/05/14 - Admin update: minor change to learning outcomes (as approved by ADE).

26/06/13 Model checking has been a very active research area and it's been successfully applied in the industry as well. I feel that it is important to introduce this very important formal verification technique, also as it nicely complements formal methods. For implementation Semester 2, 2013.

This unit provides students with an understanding of the inexorable role of formality. It replaces CSE4213 and builds upon MAT1830 (predicate logic) and CSE2201 (software development).

The unit provides the formal foundations for the discipline of software engineering, specifically supporting the needs of software engineers to know about: analysis, synthesis and design of complex systems; mathematical foundations of software engineering and applying mathematics to software problems; software engineering process and life-cycle; software systems interfaces and design; software architecture and reuse; software development methodologies and notations; programming languages and operating systems; quality frameworks, validation and reliability as it applies to software systems; software and other applicable engineering standards including documentation; development and maintenance environments for large scale software systems; and software system measurements including evaluating system performance.

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

• Articulate the role and importance of formal modelling and verification;
• Develop Event-B specifications;
• Apply Rodin to analyse an Event-B specification and verify proof obligations;
• Distinguish and evaluate the trade-offs in system modelling using Event-B and temporal logics;
• Develop basic specifications and formulate properties in temporal logics;
• Utilise a model checker to verify such properties.

020103

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.

On-campus

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

Minimum total expected workload equals 12 hours per week comprising:

(a.) Contact hours for on-campus students:

FIT

FIT2004 and one of MAT1830, MTH1112 or MAT1077