units

FIT3013

Faculty of Information Technology

Skip to content | Change text size
 

print version

Monash University

Monash University Handbook 2011 Undergraduate - Unit

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.

LevelUndergraduate
FacultyFaculty of Information Technology
OfferedClayton Second semester 2011 (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.

Objectives

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

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