units

FIT5138

Faculty of Information Technology

18 September 2017 26 April 2024
Monash University

Postgraduate - Unit

This unit entry is for students who completed this unit in 2015 only. For students planning to study the unit, please refer to the unit indexes in the the current edition of the Handbook. If you have any queries contact the managing faculty for your course or area of study.

print version

6 points, SCA Band 2, 0.125 EFTSL

Refer to the specific census and withdrawal dates for the semester(s) in which this unit is offered.

LevelPostgraduate
FacultyFaculty of Information Technology
OfferedNot offered in 2015

Synopsis

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.

Outcomes

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.

Assessment

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

Workload requirements

Minimum total expected workload equals 12 hours per week comprising:

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

  • Two hours of lectures
  • One 2-hour tutorial

(b.) 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

Chief examiner(s)

Dr Yuan-Fang Li

Prerequisites

FIT5136