FIT5138 - Advanced software engineering - 2017

This unit covers the core software engineering disciplines concerned with formally modelling software systems using logics and verifying the correctness of such specifications using mechanical/automated proof tools. Topics include mathematical logic, formal specification languages, theorem proving and model checking. It shows how to analyse model complex software systems, how to express properties that the system should adhere to and how to use mechanical/automated proof tools to formally verify such properties.

On successful completion of this unit students should be able to:

• articulate the role of formal logic and verification methods in the system development life cycle;
• categorise major techniques and approaches to software verification: theorem proving, model checking and model-based testing;
• develop software specifications and express desirable properties using a formal language such as the Event-B notation and LTL;
• install and use a theorem prover such as Rodin on a *nix/Mac OS X/Windows platform to verify the correctness of properties;
• install and use a LTL model checking system to verify the correctness of a system's temporal properties.

Examination (3 hours): 60%, In-semester assessment: 40%

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
2. Additional requirements (all students):
   • A minimum of 8 hours independent study per week for completing tutorial and project work, private study and revision.

See also Unit timetable information

Dr Yuan-Fang Li

FIT5136