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

Changes for 2010

1. Discussion fora indicated that many students did not see how specifications could be turned into code. I should develop a few examples along the lines of the approx Square Root Machine, that does end up as code (although using an informal translator - we still await an automatic code generator for Event-B).
2. This comment below from a student captures an issue that needs to be addessed: how do we get students to appreciate what formality offers to them? I suspect that the "me! right here! right now!" generation does not want to invest the effort in understanding the advantages of formality. Need to push this line a lot more.
   I'm not entirely convinced yet because I've never seen it produce anything useful that can't be done by conventional means.
3. The lecture notes could do with a tidy-up. Suggest the incremental learning material model that I have invented be pursued. The experiment to use SLIDY was not really successful (proper LaTeX and Beamer slides are more professional, but require more work).
4. The development of the concept of proof obligations needs more careful thought. This quote reveals:
   It is a bit wired that even we do not know what proof obligation is but still need to use it in first assignment. By the way, Andrew, your "joking" is wrongly spelled.
   (interesting that the poster takes another student to task for a typo, but has "wired" one in himself!

Changes for 2009

1. Switching to Event-B. This is under implementation. 20090616: and has been completed.)
2. Develop a better startup interface for Rodin 20090616: lecture 2 demonstrated a basic machine, and early lectures and tutorials used Rodin on-line. This has definitely seen students become more comfortable with running the software, although they still have difficult with the conceptualization of the whole thing!
3. Develop a Rodin tutorial specifically for FIT3013 (to be done)
4. Think about a better mechanism for assignment marking. Need a better LaTeX production and feedback. 20090616: Assignment 1 had a revised framework, being split into two parts. Part 1 was desined to get students doing a simple task ealry on - this had the desired effect, and I did not see the same problems of lack of familiarity with the tool as happened in 2008; but more documentation is still needed. The down side was that the revised framework did make it harder to mark. Requiring students to submit both pdf and project files allowed the marking to use whichever rendering seemed more appropriate: pdfs pointed quickly to the good students, the project (especially the POs) pointed to where students had a lack of understanding.

Previous News Items

Document History

This page maintained by John Hurst. Copyright Monash University Copyright Policy	312 accesses since 02 Feb 2009
Generated at 20090703:0842 from an XML file modified on 20090618:1550 Maintainer use only; not generally accessible: Local ServerWork ServerCSSE Server

462 accesses since 02 Feb 2009, HTML cache rendered at 20091122:0551