[an error occurred while processing this directive] [an error occurred while processing this directive]
[an error occurred while processing this directive]
[an error occurred while processing this directive]
Monash University

FIT3013 Formal specification for software engineering - Semester 2, 2012

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.

Mode of Delivery

Clayton (Day)

Contact Hours

2 hrs lectures/wk, 1 hr tutorial/wk


Students will be expected to spend a total of 12 hours per week during semester on this unit as follows:

  • 2 hours in lectures
  • 1 hour in tutorials
  • 3 hours of study material revision
  • 6 hours practising with the verification tools (details to be advised), and developing assignment solutions.

Unit Relationships




FIT2004 and one of MAT1830, MTH1112 or MAT1077

Chief Examiner

Campus Lecturer


Yuan-Fang Li

Academic Overview


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.

Graduate Attributes

Monash prepares its graduates to be:
  1. responsible and effective global citizens who:
    1. engage in an internationalised world
    2. exhibit cross-cultural competence
    3. demonstrate ethical values
  2. critical and creative scholars who:
    1. produce innovative solutions to problems
    2. apply research skills to a range of challenges
    3. communicate perceptively and effectively

Assessment Summary

Examination (2 hours): 50%; In-semester assessment: 50%

Assessment Task Value Due Date
Assignment 1 - Event-B Specification and Proof Discharge 20% (Parts 1 and 2 = 10% each) Week 7, Friday
Assignment 2 - Model Checking 20% Week 11, Friday
Tutorial Exercises 10% Weekly
Examination 1 50% To be advised

Teaching Approach

Lecture and tutorials or problem classes
This teaching and learning approach provides facilitated learning, practical exploration and peer learning.


Our feedback to You

Types of feedback you can expect to receive in this unit are:
  • Informal feedback on progress in labs/tutes
  • Graded assignments without comments

Your feedback to Us

Monash is committed to excellence in education and regularly seeks feedback from students, employers and staff. One of the key formal ways students have to provide feedback is through SETU, Student Evaluation of Teacher and Unit. The University's student evaluation policy requires that every unit is evaluated each year. Students are strongly encouraged to complete the surveys. The feedback is anonymous and provides the Faculty with evidence of aspects that students are satisfied and areas for improvement.

For more information on Monash's educational strategy, and on student evaluations, see:

Previous Student Evaluations of this unit

The main concerns expressed with the unit last year relate to the organisation of lectures.  Accordingly, it is planned to have the lecture slides reorganised to make them flow more coherently. 

If you wish to view how previous students rated this unit, please go to

Required Resources

Please check with your lecturer before purchasing any Required Resources. Limited copies of prescribed texts are available for you to borrow in the library, and prescribed software is available in student labs.

The following software will be required in this unit. They can be downloaded for free from various sources and are available for all major operating systems.

  • LaTeX, available in different packages for different operating systems. Links will be provided by the lecturer during the semester.
  • Rodin, available from http://www.event-b.org/

Unit Schedule

Week Activities Assessment
0   No formal assessment or activities are undertaken in week 0
1 Administrivia & introduction to basic mathematical background knowledge Weekly assessed tutorials commence (10% of unit marks)
2 Introduction to B & Event-B  
3 Abstract machines in B  
4 Abstract machines through an example  
5 Event-B Semantics  
6 Proof obligations and discharge using Rodin  
7 Structuring specifications Assignment 1 due Week 7, Friday
8 Introduction to automata  
9 Introduction to model checking (1)  
10 Introduction to model checking (2)  
11 LTL model checking (1) Assignment 2 due Week 11, Friday
12 LTL model checking (2)  
  SWOT VAC No formal assessment is undertaken in SWOT VAC
  Examination period LINK to Assessment Policy: http://policy.monash.edu.au/policy-bank/

*Unit Schedule details will be maintained and communicated to you via your MUSO (Blackboard or Moodle) learning system.

Assessment Requirements

Assessment Policy

Faculty Policy - Unit Assessment Hurdles (http://www.infotech.monash.edu.au/resources/staff/edgov/policies/assessment-examinations/unit-assessment-hurdles.html)

Academic Integrity - Please see the Demystifying Citing and Referencing tutorial at http://lib.monash.edu/tutorials/citing/

Assessment Tasks


  • Assessment task 1
    Assignment 1 - Event-B Specification and Proof Discharge
    A proof-discharged Event-B specification of a problem (exact problem to be advised).

    This assignment is administered in two parts.  Part 1 is about defining the various parameters of the specification (in fact, a requirements analysis), and Part 2 is about coding the Event-B specification in Rodin and LaTeX.  The two parts will be offered separately, so that feedback may be returned on Part 1, before students complete Part 2.

    Assignment release date Week 2.
    20% (Parts 1 and 2 = 10% each)
    Criteria for assessment:

    Correctness and completeness of specification.

    Discharge of all proof obligations (mechanically or manually).

    Declarative style of specification.

    Due date:
    Week 7, Friday
  • Assessment task 2
    Assignment 2 - Model Checking
    A specification will be given, which is to be developed in a model in linear temporal logic. 

    A number of properties will also need to be expressed in LTL and verified by a model checker.

    Assignment release date Week 7.
    Criteria for assessment:

    Correctness and completeness of specification and properties.

    Declarative style of specification.

    Due date:
    Week 11, Friday
  • Assessment task 3
    Tutorial Exercises
    Students will be given exercise questions during each tutorial and asked to provide solutions for them.
    Criteria for assessment:

    Student attendance and completion of exercises.

    Quality or correctness of solutions to questions, demonstrating understanding of the learning materials.

    Due date:


  • Examination 1
    2 hours
    Type (open/closed book):
    Closed book
    Electronic devices allowed in the exam:
    Sample papers will be available on the unit website.

Assignment submission

It is a University requirement (http://www.policy.monash.edu/policy-bank/academic/education/conduct/plagiarism-procedures.html) for students to submit an assignment coversheet for each assessment item. Faculty Assignment coversheets can be found at http://www.infotech.monash.edu.au/resources/student/forms/. Please check with your Lecturer on the submission method for your assignment coversheet (e.g. attach a file to the online assignment submission, hand-in a hard copy, or use an online quiz).

Online submission

If Electronic Submission has been approved for your unit, please submit your work via the VLE site for this unit, which you can access via links in the my.monash portal.

Extensions and penalties

Returning assignments

Other Information


Student services

The University provides many different kinds of support services for you. Contact your tutor if you need advice and see the range of services available at www.monash.edu.au/students. For Sunway see http://www.monash.edu.my/Student-services, and for South Africa see http://www.monash.ac.za/current/

The Monash University Library provides a range of services and resources that enable you to save time and be more effective in your learning and research. Go to http://www.lib.monash.edu.au or the library tab in my.monash portal for more information. At Sunway, visit the Library and Learning Commons at http://www.lib.monash.edu.my/. At South Africa visit http://www.lib.monash.ac.za/.

Academic support services may be available for students who have a disability or medical condition. Registration with the Disability Liaison Unit is required. Further information is available as follows:

  • Website: http://monash.edu/equity-diversity/disability/index.html;
  • Email: dlu@monash.edu
  • Drop In: Equity and Diversity Centre, Level 1 Gallery Building (Building 55), Monash University, Clayton Campus, or Student Community Services Department, Level 2, Building 2, Monash University, Sunway Campus
  • Telephone: 03 9905 5704, or contact the Student Advisor, Student Commuity Services at 03 55146018 at Sunway
[an error occurred while processing this directive]