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.
Minimum total expected workload equals 12 hours per week comprising:
(a.) Contact hours for on-campus students:
(b.) Additional requirements (all students):
Students will be expected to spend a total of 12 hours per week during semester on this unit as follows:
CSE4213
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.
Yuan-Fang Li
Lito Cruz
Lito Cruz
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 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
| 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.
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 |
Faculty Policy - Unit Assessment Hurdles (http://intranet.monash.edu.au/infotech/resources/staff/edgov/policies/assessment-examinations/assessment-hurdles.html)
Academic Integrity - Please see resources and tutorials at http://www.monash.edu/library/skills/resources/tutorials/academic-integrity/
Correctness and completeness of specification.
Discharge of all proof obligations (mechanically or manually).
Declarative style of specification.
Correctness and completeness of specification and properties.
Declarative style of specification.
Completion of exercises.
Quality or correctness of solutions to questions, demonstrating understanding of the learning materials.
Monash Library Unit Reading List (if applicable to the unit)
http://readinglists.lib.monash.edu/index.html
Faculty of Information Technology Style Guide
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:
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.monash.edu.au/exams/special-consideration.html
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.
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.
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.
Materials of this units are mainly drawn from the following two textbooks:
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:
Important student resources including Faculty policies are located at http://intranet.monash.edu.au/infotech/resources/students/
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 http://www.monash.edu.au/students. For Malaysia 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, resources and programs that enable you to save time and be more effective in your learning and research. Go to www.lib.monash.edu.au or the library tab in my.monash portal for more information. At Malaysia, visit the Library and Learning Commons at http://www.lib.monash.edu.my/. At South Africa visit http://www.lib.monash.ac.za/.