CSE4213 Formal methods in software engineering , Unit Information Guide (Semester 1, 2006)

Chief Examiner John Hurst
Clayton : John Hurst
Outline Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications. The B notation, schemas, schema calculus, schema types and operations; data and algorithm design; data and operation refinement; proofs of correctness. The place of formal methods in software engineering practice.
  1. an understanding of the Fundamentals of the B Method
  2. an awareness of the Applications of the B Method
  3. A reading knowledge of 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 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


Completion of CSE2303, MAT1830 or MTH1112 or MAT1077

A thorough knowledge of set theory is required, and students should also be familiar with first order predicate calculus. The Infotech Unit Avatar entry lists CSE2201 as an additional prerequisite, however, this prerequisite has not yet been approved by faculty.

Unit relationships There are no units that follow up material in this unit.
Texts and software

Required text(s)

Schneider, S., The B-Method: An Introduction, first edition, Palgrave, 2001 ISBN 0-333-79284-X.

Text books are available from the Monash University Book Shops. Availability from other suppliers cannot be assured. The Bookshop orders texts in specifically for this unit. You are advised to purchase your text book early.

Software requirements:

Software Details: B Toolkit

Vendor: B Core Pty Ltd

Software Title*: B Toolkit

Version*: 5.1.12


First Semester Week Required :??? week 2

License Details*: 50 seat Site Licence (spelt with a \\\\'C\\\\', notice!)


Software Details: LaTeX


Software Title*: LaTeX

Version*: latest


First Semester Week Required :??? week 2

License Details*: Freeware

Hardware requirements:

Intel-based Linux. A hardware licence is available Alternatively, if an X11 server is available, users can X11-serve onto ITS sng machines.

Recommended reading

Library access You may need to access the Monash library either personally to be able to satisfactorily complete the subject.  Be sure to obtain a copy of the Library Guide, and if necessary, the instructions for remote access from the library website.
Study resources

Study resources for CSE4213 are:


Structure and organisation



Study Guide

Key Dates

1 Introduction to B, Set Theory
2 Abstract machines
3 Modelling
4 Library Case Study
5 Proof Obligations Assignment 1 due
6 preconditions, Simple File System
7 Generalised Substitutions
8 Structuring Specifications Assignment 2 due
9 Machine Composition
10 Refinement
11 Beyond Specification
12 Data and Code Correctness Assignment 3 due
13 revision

The timetable for on-campus classes for this unit can be viewed in Allocate+


There are three assignments, each worth 20%, and one 2 hour examination paper, worth 40%.

Please note the assignment submission page at http://www.csse.monash.edu.au/subjects/assign_submit.html, which details information relating to the submission of assignment work, particularly the requirement that the deadline is 12noon on the date concerned.

Assessment Policy

To pass this unit you must:

Your score for the unit will be calculated by:

Assessment Requirements


Due Date


Assignment specifications will be made available . Information about assignments will be published on the Unit's Notices Newsgroup.

Assignment Submission Methods

Extensions and late submissions

Late submission of assignments

Assignments received after the due date will be subject to a penalty of 10% per day

This policy is strict because comments or guidance will be given on assignments as they are returned, and sample solutions may also be published and distributed, after assignment marking or with the returned assignment. 


It is your responsibility to structure your study program around assignment deadlines, family, work and other commitments. Factors such as normal work pressures, vacations, etc. are seldom regarded as appropriate reasons for granting extensions. 

Requests for extensions must be made by application to the school at least two days before the due date. You will be asked to forward original medical certificates in cases of illness, and may be asked to provide other forms of documentation where necessary. A copy of the email or other written communication of an extension must be attached to the assignment submission.

Grading of assessment

Assignments, and the unit, will be marked and allocated a grade according to the following scale:

HD High Distinction - very high levels of achievement, demonstrated knowledge and understanding, skills in application and high standards of work encompassing all aspects of the tasks.
In the 80+% range of marks for the assignment.
D Distinction - high levels of achievement, but not of the same standards. May have a weakness in one particular aspect, or overall standards may not be quite as high.
In the 70-79% range.
C Credit - sound pass displaying good knowledge or application skills, but some weaknesses in the quality, range or demonstration of understanding.
In the 60-69% range.
P Pass - acceptable standard, showing an adequate basic knowledge, understanding or skills, but with definite limitations on the extent of such understanding or application. Some parts may be incomplete.
In the 50-59% range.
N Not satisfactory -  failure to meet the basic requirements of the assessment.
Below 50%.

We will aim to have assignment results made available to you within two weeks after assignment receipt.

Feedback Feedback to you

You will receive feedback on your work and progress in this unit. This feedback may be provided through your participation in tutorials and class discussions, as well as through your assignment submissions. It may come in the form of individual advice, marks and comments, or it may be provided as comment or reflection targeted at the group. It may be provided through personal interactions, such as interviews and on-line forums, or through other mechanisms such as on-line self-tests and publication of grade distributions.

Feedback from you

You will be asked to provide feedback to the Faculty through a Unit Evaluation survey at the end of the semester. You may also be asked to complete surveys to help teaching staff improve the unit and unit delivery. Your input to such surveys is very important to the faculty and the teaching staff in maintaining relevant and high quality learning experiences for our students.

And if you are having problems

It is essential that you take action immediately if you realise that you have a problem with your study. The semester is short, so we can help you best if you let us know as soon as problems arise. Regardless of whether the problem is related directly to your progress in the unit, if it is likely to interfere with your progress you should discuss it with your lecturer or a Community Service counsellor as soon as possible.

Plagiarism and cheating

Plagiarism and cheating are regarded as very serious offences. In cases where cheating  has been confirmed, students have been severely penalised, from losing all marks for an assignment, to facing disciplinary action at the Faculty level. While we would wish that all our students adhere to sound ethical conduct and honesty, I will ask you to acquaint yourself with Student Rights and Responsibilities and the Faculty regulations that apply to students detected cheating as these will be applied in all detected cases.

In this University, cheating means seeking to obtain an unfair advantage in any examination or any other written or practical work to be submitted or completed by a student for assessment. It includes the use, or attempted use, of any means to gain an unfair advantage for any assessable work in the unit, where the means is contrary to the instructions for such work. 

When you submit an individual assessment item, such as a program, a report, an essay, assignment or other piece of work, under your name you are understood to be stating that this is your own work. If a submission is identical with, or similar to, someone else's work, an assumption of cheating may arise. If you are planning on working with another student, it is acceptable to undertake research together, and discuss problems, but it is not acceptable to jointly develop or share solutions unless this is specified by your lecturer. 

Intentionally providing students with your solutions to assignments is classified as "assisting to cheat" and students who do this may be subject to disciplinary action. You should take reasonable care that your solution is not accidentally or deliberately obtained by other students. For example, do not leave copies of your work in progress on the hard drives of shared computers, and do not show your work to other students. If you believe this may have happened, please be sure to contact your lecturer as soon as possible.

Cheating also includes taking into an examination any material contrary to the regulations, including any bilingual dictionary, whether or not with the intention of using it to obtain an advantage.

Plagiarism involves the false representation of another person's ideas, or findings, as your own by either copying material or paraphrasing without citing sources. It is both professional and ethical to reference clearly the ideas and information that you have used from another writer. If the source is not identified, then you have plagiarised work of the other author. Plagiarism is a form of dishonesty that is insulting to the reader and grossly unfair to your student colleagues.



Notices related to the unit during the semester will be placed on the Notices Newsgroup in the Unit Website. Check this regularly. Failure to read the Notices newsgroup is not regarded as grounds for special consideration.

Consultation Times

If direct communication with your unit adviser/lecturer or tutor outside of consultation periods is needed you may contact the lecturer and/or tutors at:

Associate Professor John Hurst
Associate Professor
Phone +61 3 990 55192
Fax +61 3 990 55146

All email communication to you from your lecturer will occur through your Monash student email address. Please ensure that you read it regularly, or forward your email to your main address. Also check that your contact information registered with the University is up to date in My.Monash.

Last updated: May 4, 2006