units

FIT3013

Faculty of Information Technology

12 April 2013 23 May 2013

Undergraduate - Unit

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, or view unit timetables.

LevelUndergraduate
FacultyFaculty of Information Technology
OfferedClayton Second semester 2013 (Day)

Synopsis

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, data and algorithm design; data and operation refinement; proofs of correctness; proof obligations.

Outcomes

At the completion of this unit students will have -

A knowledge and understanding of:

  • fundamentals of the Event-B Method;
  • applications of the Event-B Method;
  • Event-B specifications;
  • software Testing in the discrete domain;
  • the role of proof obligations and consistent specifications;
  • determination of Proof Obligation;
  • the role of refinement in developing formal specifications.

Developed attitudes that enable them to:

  • have an appreciation of the professional need to establish formal properties of software;
  • have a belief that formal specifications can improve the quality of software.

Developed the skills to:

  • use the Event-B notation to develop and prove software specifications;
  • install a Event-B Toolkit on a Unix/Linux/Windows platform;
  • write basic Event-B specifications;
  • refine and extend more advanced Event-B specifications.

Assessment

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

Chief examiner(s)

Dr Yuan-Fang Li

Contact hours

2 hrs lectures/wk, 1 hr tutorial/wk

This unit applies to the following area(s) of study

Software engineering
Systems development

Prerequisites

FIT2004 and one of MAT1830, MTH1112 or MAT1077

Prohibitions

CSE4213

Additional information on this unit is available from the faculty at:

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