Monash University Handbook 2010 Undergraduate - Unit

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.

• 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.

• 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