units

FIT3013

Faculty of Information Technology

Skip to content | Change text size
 

print version

Monash University Handbook 2010 Undergraduate - Unit

6 points, SCA Band 2, 0.125 EFTSL

LevelUndergraduate
FacultyFaculty of Information Technology
OfferedClayton First semester 2010 (Day)
Coordinator(s)Associate Professor John Hurst

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)

Associate Professor John Hurst

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