Skip to the content | Change text size
PDF unit guide

FIT3013 Formal specification for software engineering - Semester 1, 2009

Unit leader :

John Hurst

Lecturer(s) :

Clayton

  • John Hurst

Introduction

This unit is a core 6 point unit in the Bachelor of Software Engineering.  It is a recoding of the previous unit, CSE4213.  In this unit you will learn how to bring some mathematical formalism to the design and specification of software projects.  The software tool, Rodin, will be used to support the methodology developed by the unit, namely, the Event-B method.  Students will write and prove some simple software designs to see how the formalism can be used in a practical context.

Unit synopsis

Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications. The Event-B notation; abstract machines, contexts, machine types and operations; proof obligations and proof discharging; data and algorithm design; data and operation refinement; proofs of correctness. The place of formal methods in software engineering practice.

Learning outcomes

  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 write basic Event-B specifications
  12. The ability to refine and extend more advanced Event-B specifications

Workload

  • 2x1 hour lectures per week
  • 1x1 hour tutorial per week
  • 3 hours of contact material revision per week
  • 3-6 hours (average) per week practising skills with the Rodin tool suite, and developing assignment solutions.

Unit relationships

Prerequisites

Completion of FIT2004 and (MAT1830 or MTH1112 or MAT1077)

A thorough knowledge of set theory is required, and students should also be familiar with first order predicate calculus.

Relationships

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

Continuous improvement

Monash is committed to ‘Excellence in education’ (Monash Directions 2025 - http://www.monash.edu.au/about/monash-directions/directions.html) and strives for the highest possible quality in teaching and learning.

To monitor how successful we are in providing quality teaching and learning Monash regularly seeks feedback from students, employers and staff. One of the key formal ways students have to provide feedback is through Unit Evaluation Surveys. The University’s Unit Evaluation policy (http://www.policy.monash.edu/policy-bank/academic/education/quality/unit-evaluation-policy.html) requires that every unit offered is evaluated each year. Students are strongly encouraged to complete the surveys as they are an important avenue for students to “have their say”. The feedback is anonymous and provides the Faculty with evidence of aspects that students are satisfied and areas for improvement.

Faculties have the option of administering the Unit Evaluation survey online through the my.monash portal or in class. Lecturers will inform students of the method being used for this unit towards the end of the semester.

Student Evaluations

If you wish to view how previous students rated this unit, please go to http://www.adm.monash.edu.au/cheq/evaluations/unit-evaluations/

Improvements to this unit

The main concerns expressed with the unit last year relate to the usability of the software tool, Rodin.  Accordingly, it is planned to devote a few lectures to the use of this tool early in the unit, so that students become more familiar with its use before the need to use it in assignments is required.

Unit staff - contact details

Unit leader

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

Lecturer(s) :

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

Teaching and learning method

Learning resources for the unit will be made available on-line through both the unit web pages at

   http://www.csse.monash.edu.au/~ajh/teaching/fit3013/2009/index.xml

 and the Moodle pages

  http://moodle.med.monash.edu.au/course/view.php?id=79

 Besides the scheduled lectures and tutorials, students will be expected to use additional hours in this unit in developing their understanding of, and skills in, the use of the Rodin software suite.  Manuals for the software will be available through the web pages.  Students are also expected to interact dynamically through the semester via the use of the Moodle discussion pages

Tutorial allocation

On-campus students should register for tutorials/laboratories using Allocate+.

Communication, participation and feedback

Monash aims to provide a learning environment in which students receive a range of ongoing feedback throughout their studies. You will receive feedback on your work and progress in this unit. This may take the form of group feedback, individual feedback, peer feedback, self-comparison, verbal and written feedback, discussions (on line and in class) as well as more formal feedback related to assignment marks and grades. You are encouraged to draw on a variety of feedback to enhance your learning.

It is essential that you take action immediately if you realise that you have a problem that is affecting your study. Semesters are 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.

Unit Schedule

Week Topic Key dates
1 Introduction to B, Set Theory  
2 Abstract machines  
3 Using Rodin  
4 Modelling Discussion 1 due
5 Case Study Assignment 1 due
6 Proof Obligations  
Mid semester break
7 Generalised Substitutions Discussion 2 due
8 Structuring Specifications  
9 Machine Composition Discussion 3 due
10 Refinement  
11 Refinement Assignment 2 due
12 Data and Code Correctness Discussion 4 due
13 Revision  

Unit Resources

Prescribed text(s) and readings

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

Recommended text(s) and readings

Required software and/or hardware

Software Details: the Event-B Toolkit, Rodin

Vendor: open source

Software Title*: Rodin

Version*: 0.8.2

OS*: Linux, Mac or Windows

First Semester Week Required :week 2

License Details*: open source

Software Details: LaTeX

Vendor:

Software Title*: LaTeX

Version*: latest

OS*: Mac OSX, Linux or Windows

First Semester Week Required :week 2

License Details*: Freeware

Equipment and consumables required or provided

The software is available for Mac OSX, Linux or Windows.  Students can download whichever version they prefer to use.

Study resources

Study resources we will provide for your study are:

Available from either

  http://www.csse.monash.edu.au/~ajh/teaching/fit3013/2009/index.xml 

or 

  http://moodle.med.monash.edu.au/course/view.php?id=79

Library access

The Monash University Library site contains details about borrowing rights and catalogue searching.  To learn more about the library and the various resources available, please go to http://www.lib.monash.edu.au.

The Educational Library and Media Resources (LMR) is also a very resourceful place to visit at http://www.education.monash.edu.au/library/

Monash University Studies Online (MUSO)

All unit and lecture materials are available through MUSO (Monash University Studies Online). Blackboard is the primary application used to deliver your unit resources. Some units will be piloted in Moodle. If your unit is piloted in Moodle, you will see a link from your Blackboard unit to Moodle (http://moodle.monash.edu.au) and can bookmark this link to access directly. In Moodle, from the Faculty of Information Technology category, click on the link for your unit.

You can access MUSO and Blackboard via the portal: http://my.monash.edu.au

Click on the Study and enrolment tab, then Blackboard under the MUSO learning systems.

In order for your Blackboard unit(s) to function correctly, your computer needs to be correctly configured.

For example:

  • Blackboard supported browser
  • Supported Java runtime environment

For more information, please visit: http://www.monash.edu.au/muso/support/students/downloadables-student.html

You can contact the MUSO Support by phone : (+61 3) 9903 1268

For further contact information including operational hours, please visit: http://www.monash.edu.au/muso/support/students/contact.html

Further information can be obtained from the MUSO support site: http://www.monash.edu.au/muso/support/index.html

Assessment

Unit 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 44% then a mark of 44-N will be recorded for the unit.

Assignment tasks

  • Assignment Task

    Title : Discussion

    Description :

    The Moodle discussion forum will be used to support class discussion about various topics during the semester.  There will be several seminal starter topics posted by the lecturer, and all students are expected to make at least one individual original response to each posting.

    Weighting : 20%

    Criteria for assessment :

    There will be 4 topics for discussion, distributed over the semester, and relating to issues discussed in lectures.  Students are encouraged to post several times for each topic, and to respond to points raised either by the lecturer or by other students.  Each posting will be assessed for originality, correctness and appropriateness to the topic under discussion.  Each topic is worth 5% of the total, and full marks are only possible if a student posts at least twice (at least one posting must include some rebuttal or other response to a previous posting by another poster).

    Due date : within 4 weeks of starter posting, or the end of semester, whichever comes first

    Remarks ( optional - leave blank for none ) :

    This was a popular assessment in 2008, but many students lost easy marks because they failed to participate.

  • Assignment Task

    Title : Assignment 1: Specification

    Description :

    A proof-discharged event-B specification of a problem (exact problem to be advised)

    Weighting : 20%

    Criteria for assessment :

    Correctness and completeness of specification, discharge of all proof obligations (mechanically or manually), and declarative style of specification.

    Due date : end of week 5

    Remarks ( optional - leave blank for none ) :

    Release date week 1

  • Assignment Task

    Title : Assignment 2: Refinement

    Description :

    A proof-discharged event-B refinement of the specification begun in Assignment 1

    Weighting : 20%

    Criteria for assessment :

    Correctness, declarative style, proof discharges

    Due date : end of week 11

    Remarks ( optional - leave blank for none ) :

    Release date week 6

Examinations

  • Examination 1

    Weighting : 40%

    Length : 2 hours

    Type ( open/closed book ) : Closed book

    Remarks ( optional - leave blank for none ) :

    Sample papers are available on the web pages


Assignment submission

assignments must be submitted as PDF files through the Moodle submission framework, and labelled with the studentID os the author.

Assignment coversheets

All assignments must include a signed cover sheet, which must be submitted electronically as a single PDF file, called <studentID>-Ax-cover.pdf, where <studentID> is the student's 8 digit ID, and x is the assignment number. 

 The cover sheet is available from http://infotech.monash.edu.au/resources/student/assignments/

University and Faculty policy on assessment

Due dates and extensions

The due dates for the submission of assignments are given in the previous section. Please make every effort to submit work by the due dates. 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. Students are advised to NOT assume that granting of an extension is a matter of course.

Requests for extensions must be made to the unit lecturer at your campus 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.

Late assignment

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

Return dates

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

Assessment for the unit as a whole is in accordance with the provisions of the Monash University Education Policy at http://www.policy.monash.edu/policy-bank/academic/education/assessment/

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

Plagiarism, cheating and collusion

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 the University Plagiarism policy and procedure (http://www.policy.monash.edu/policy-bank/academic/education/conduct/plagiarism-procedures.html) which applies to students detected plagiarising.

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.

Register of counselling about plagiarism

The university requires faculties to keep a simple and confidential register to record counselling to students about plagiarism (e.g. warnings). The register is accessible to Associate Deans Teaching (or nominees) and, where requested, students concerned have access to their own details in the register. The register is to serve as a record of counselling about the nature of plagiarism, not as a record of allegations; and no provision of appeals in relation to the register is necessary or applicable.

Non-discriminatory language

The Faculty of Information Technology is committed to the use of non-discriminatory language in all forms of communication. Discriminatory language is that which refers in abusive terms to gender, race, age, sexual orientation, citizenship or nationality, ethnic or language background, physical or mental ability, or political or religious views, or which stereotypes groups in an adverse manner. This is not meant to preclude or inhibit legitimate academic debate on any issue; however, the language used in such debate should be non-discriminatory and sensitive to these matters. It is important to avoid the use of discriminatory language in your communications and written work. The most common form of discriminatory language in academic work tends to be in the area of gender inclusiveness. You are, therefore, requested to check for this and to ensure your work and communications are non-discriminatory in all respects.

Students with disabilities

Students with disabilities that may disadvantage them in assessment should seek advice from one of the following before completing assessment tasks and examinations:

Deferred assessment and special consideration

Deferred assessment (not to be confused with an extension for submission of an assignment) may be granted in cases of extenuating personal circumstances such as serious personal illness or bereavement. Information and forms for Special Consideration and deferred assessment applications are available at http://www.monash.edu.au/exams/special-consideration.html. Contact the Faculty's Student Services staff at your campus for further information and advice.