[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, 2014

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, the role of proof obligations and refinement, the LTL and CTL temporal logics, the model checking approach and techniques.

Mode of Delivery

Clayton (Day)

Workload Requirements

Minimum total expected workload equals 12 hours per week comprising:

(a.) Contact hours for on-campus students:

  • Two hours of lectures
  • One 2-hour tutorial/lab

(b.) Additional requirements (all students):

  • A minimum of 8 hours independent study per week for completing lab and project work, private study and revision.

Additional workload requirements

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

  • 2 hours in lectures
  • 2 hours in tutorials/labs
  • 3-4 hours of study material revision
  • 4-5 hours practising with the verification tools (details to be advised), and developing assignment solutions.

Unit Relationships

Prohibitions

CSE4213

Prerequisites

FIT2004 and one of MAT1830, MTH1112 or MAT1077

A knowledge of set theory, predicate logic, graph, automata and declarative programming is assumed, together with some experience in dealing with the first two.

Chief Examiner

Campus Lecturer

Clayton

Yuan-Fang Li

Lito Cruz

Tutors

Clayton

Lito Cruz

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 the Student Evaluation of Teaching and Units (SETU) survey. 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, see:

www.monash.edu.au/about/monash-directions/ and on student evaluations, see: www.policy.monash.edu/policy-bank/academic/education/quality/student-evaluation-policy.html

Previous Student Evaluations of this Unit

Previous feedback has informed improvements to this unit, including the incorporation of weekly 2-hour tutorials/labs for practice with the tools used in this unit: Rodin and NuSMV.

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

Academic Overview

Learning Outcomes

At the completion of this unit students should be able to:
  • articulate the role and importance of formal modelling and verification;
  • develop Event-B specifications;
  • apply Rodin to analyse an Event-B specification and verify proof obligations;
  • distinguish and evaluate the trade-offs in system modelling using Event-B and temporal logics;
  • develop basic specifications and formulate properties in temporal logics;
  • utilise a model checker to verify such properties.

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  
10 LTL model checking (1)  
11 LTL model checking (2) Assignment 2 due Week 11, Friday
12 CTL model checking  
  SWOT VAC No formal assessment is undertaken in 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 learning system.

Teaching Approach

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

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
Class participation 10% Weekly
Examination 1 50% To be advised

Assessment Requirements

Assessment Policy

Assessment Tasks

Participation

  • Assessment task 1
    Title:
    Assignment 1 - Event-B Specification and Proof Discharge
    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 developing the Event-B specification in Rodin. 

    Assignment release date Week 3.
    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:
    Week 7, Friday
  • Assessment task 2
    Title:
    Assignment 2 - Model Checking
    Description:
    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.
    Weighting:
    20%
    Criteria for assessment:

    Correctness and completeness of specification and properties.

    Declarative style of specification.

    Due date:
    Week 11, Friday
  • Assessment task 3
    Title:
    Class participation
    Description:
    Students will be assessed on class participation: active engagement in problem solving in tutorials.
    Weighting:
    10%
    Criteria for assessment:

    Completion of exercises.

    Quality or correctness of solutions to questions, demonstrating 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.

Learning resources

Monash Library Unit Reading List (if applicable to the unit)
http://readinglists.lib.monash.edu/index.html

Faculty of Information Technology Style Guide

Feedback to you

Examination/other end-of-semester assessment feedback may take the form of feedback classes, provision of sample answers or other group feedback after official results have been published. Please check with your lecturer on the feedback provided and take advantage of this prior to requesting individual consultations with staff. If your unit has an examination, you may request to view your examination script booklet, see http://intranet.monash.edu.au/infotech/resources/students/procedures/request-to-view-exam-scripts.html

Types of feedback you can expect to receive in this unit are:

  • Informal feedback on progress in labs/tutes
  • Graded assignments with comments

Extensions and penalties

Returning assignments

Assignment submission

It is a University requirement (http://www.policy.monash.edu/policy-bank/academic/education/conduct/student-academic-integrity-managing-plagiarism-collusion-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). Please note that it is your responsibility to retain copies of your assessments.

Online submission

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

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.

Recommended Resources

Materials of this units are mainly drawn from the following two textbooks:

  • Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.
  • Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. Vol. 26202649. Cambridge: MIT press, 2008.

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: www.policy.monash.edu.au/policy-bank/academic/education/index.html

Key educational policies include:

Faculty resources and policies

Important student resources including Faculty policies are located at http://intranet.monash.edu.au/infotech/resources/students/

Graduate Attributes Policy

Student Charter

Student services

Monash University Library

Disability Liaison Unit

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]