Unit Outline

Unit Synopsis | Workloads | Improvement | Previous News Items

Welcome to FIT3013! These web pages should be your first port of call for any information specific to this subject. If the information you seek is not here, drop me a note and I'll endeavour to fix it for you.

Please note that these pages will be regularly updated throughout the semester. You are encouraged to bookmark the home page in your browser, and visit it at least once per week.

Unit Synopsis

The Handbook Entry for FIT3013 is available, but not very accurate. See below for more up-to-date information about the unit objectves and learning outcomes. Or you can look at the FIT3013 Avatar Entry.

The Undergraduate Handbook itself is at: http://www.monash.edu.au/pubs/handbooks/undergrad/

The faculty Unit Guide (PDF) page for this unit is available. Note that this guide can give valuable insights into how to study the unit.

For example, I often get asked "Is such-and-such a topic examinable?". You can see what material is examinable by looking at the learning objectives. If some topic contributes to that learning objective, it is examinable. To help you understanding the relationship between the learning objectives and examinable material, every major learning activity identified in these web pages has a link to the corresponding learning objective(s). Simply hover your mouse over the learning material link to see the learning objective pop up.

Unit Objectives

The Unit Objectives are an important aid to understand what the subject is all about. In them, we try to define what the university (through the Clayton School of Information Technology) thinks is important about the subject.

1. an understanding of the Fundamentals of the Event-B Method
2. an awareness of the Applications of the Event-B Method
3. A reading knowledge of Event-B specifications
4. The use of Software Testing in the discrete domain
5. The role of proof obligations and consistent specifications
6. How to extract a Determination of Proof Obligation
7. an understanding of 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 Event-B notation to develop and prove software specifications
11. The ability to install an Event-B toolkit (such as Rodin) on a Unix/Linux/Mac/Windows platform
12. The ability to write basic Event-B specifications
13. The ability to refine and extend more advanced Event-B specifications

Prerequisite knowledge

Material covered by the following units, as noted:

MAT1830 or MTH1112 or MAT1077

What is essential from these units is a thorough understanding of sets and set theory, particular the notion of a relation between elements of sets.

FIT2004

This unit covers algorithm and data design methods, skills which are needed in the refinement process. The concept of a proof for program specification is also covered in this unit.

FIT2024

This unit covers the concepts of program specification.

Relationship to following units

There are no units that follow up material in this unit.

Workloads

Students are expected to attend the two lectures each week, and 1 tutorial. Lectures will require private study in order to keep up with the pace of materials. In addition, a significant amount of time should be spent working with the Rodin software system that supports the Event-B method.

Improvement

The unit evaluation from 2007 CSE4213 is not available, since an insufficient number of students completed the unit evaluation survey. If you have any comments on the delivery of this unit, you are invited, nay encouraged, to email John Hurst with your comments! I cannot fix things that I do not know are broken!

Lecturer Reflections

These are some of the things I (ajh) would like to change for 2008:

1. Switching to Event-B. This is under implementation.

These are suggested changes for 2009:

1. Develop a better startup interface for Rodin
2. Develop a Rodin tutorial specifically for FIT3013
3. Think about a better mechanism for assignment marking. Need a better LaTeX production and feedback.

Previous News Items

Document History

This page maintained by John Hurst. Copyright Monash University Copyright Policy	394 accesses since 25 Jun 2008
Generated at 20090704:1155 from an XML file modified on 20090129:1618 Maintainer use only; not generally accessible: Local ServerWork ServerCSSE Server

465 accesses since 25 Jun 2008, HTML cache rendered at 20091124:1623