FIT3013 - Formal specification for software engineering

Leader(s): John Hurst

Offered

Clayton First semester 2009 (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

1. Fundamentals of the B Method;
2. Applications of the B Method;
3. A reading knowledge of B specifications;
4. Software Testing in the discrete domain;
5. The role of proof obligations and consistent specifications;
6. Determination of Proof Obligation;
7. The role of refinement in developing formal specifications;
8. An appreciation of the professional need to establish formal properties of software;
9. A belief that formal specifications can improve the quality of software;
10. Skills in using the B notation to develop and prove software specifications;
11. The ability to install a B Toolkit on a Unix/Linux platform;
12. The ability to write basic B specifications;
13. The ability to refine and extend more advanced B specifications.

Assessment

Assignments: 50%
Examination: 50%

Contact hours

3 x contact hrs/week

Prerequisites

FIT2004 and (MAT1830 or MTH1112 or MAT1077)

Prohibitions

CSE4213, GCO4013, SFT3302

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

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