[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]

Academic Overview

Learning Objectives

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 - Specification 20% (Parts 1 and 2 = 10% each) Part 1 due Friday Week 5, Part 2 due Friday Week 7
Assignment 2 - Refinement 20% Friday Week 11
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.

Feedback

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:
http://www.monash.edu.au/about/monash-directions/directions.html
http://www.policy.monash.edu/policy-bank/academic/education/quality/student-evaluation-policy.html

Previous Student Evaluations of this unit

If you wish to view how previous students rated this unit, please go to
https://emuapps.monash.edu.au/unitevaluations/index.jsp

Required Resources

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 Tutorial Exercises
2 Introduction to B & Event-B Tutorial Exercises
3 Abstract machines in B Tutorial Exercises
4 Abstract machines through an example Tutorial Exercises
5 Semantics & proof obligations in B Tutorial Exercises; Assignment 1 (Part 1) due Friday Week 5
6 Generalised substitutions Tutorial Exercises
7 Structuring specifications Tutorial Exercises; Assignment 1 (Part 2) due Friday Week 7
8 Machine composition Tutorial Exercises
9 Refinement I Tutorial Exercises
10 Refinement II Tutorial Exercises
11 Data and code correctness Tutorial Exercises; Assignment 2 due Friday Week 11
12 Revision Tutorial Exercises
  SWOT VAC No formal assessment is undertaken SWOT VAC
  Examination period LINK to Assessment Policy: http://policy.monash.edu.au/policy-bank/
academic/education/assessment/
assessment-in-coursework-policy.html

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

Assessment Requirements

Assessment Policy

To pass a unit which includes an examination as part of the assessment a student must obtain:

  • 40% or more in the unit's examination, and
  • 40% or more in the unit's total non-examination assessment, and
  • an overall unit mark of 50% or more.

If a student does not achieve 40% or more in the unit examination or the unit non-examination total assessment, and the total mark for the unit is greater than 50% then a mark of no greater than 49-N will be recorded for the unit

Assessment Tasks

Participation

  • Assessment task 1
    Title:
    Assignment 1 - Specification
    Description:
    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.
    Weighting:
    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:
    Part 1 due Friday Week 5, Part 2 due Friday Week 7
  • Assessment task 2
    Title:
    Assignment 2 - Refinement
    Description:
    A proof-discharged Event-B refinement of the specification begun in Assignment 1.

    Assignment 2 will extend the functionality of the specification developed in Assignment 1. 

    Assignment release date Week 7.
    Weighting:
    20%
    Criteria for assessment:

    Correctness and completeness of specification.

    Discharge of all proof obligations (mechanically or manually).

    Declarative style of specification.

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

    Student attendance and completion of exercises.

    Quality or correctness of solutions to questions (demonstrates understanding of the learning materials).

    Due date:
    Weekly

Examinations

  • Examination 1
    Weighting:
    50%
    Length:
    2 hours
    Type (open/closed book):
    Closed book
    Electronic devices allowed in the exam:
    None
    Remarks:
    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).

Extensions and penalties

Submission must be made by the due date otherwise penalties will be enforced.

You must negotiate any extensions formally with your campus unit leader via the in-semester special consideration process: http://www.infotech.monash.edu.au/resources/student/equity/special-consideration.html.

Returning assignments

Students can expect assignments to be returned within two weeks of the submission date or after receipt, whichever is later

Other Information

Policies

Monash has educational policies, procedures and guidelines, which are designed to ensure that staff and students are aware of the University's academic standards, and to provide advice on how they might uphold them. You can find Monash's Education Policies at:
http://policy.monash.edu.au/policy-bank/academic/education/index.html

Key educational policies include:

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 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. Students who have a disability or medical condition are welcome to contact the Disability Liaison Unit to discuss academic support services. Disability Liaison Officers (DLOs) visit all Victorian campuses on a regular basis

[an error occurred while processing this directive]