Undergraduate - UnitFIT3013 - Formal specification for software engineering

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

Level	Undergraduate
Faculty	Faculty of Information Technology
Offered	Clayton Second semester 2012 (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

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