COMPX552-19A (HAM)

Model Checking

15 Points

Edit Header Content
Division of Health Engineering Computing & Science
School of Computing and Mathematical Sciences
Department of Computer Science

Staff

Edit Staff Content

Convenor(s)

Lecturer(s)

Administrator(s)

Placement Coordinator(s)

Tutor(s)

Student Representative(s)

Lab Technician(s)

Librarian(s)

: debby.dada@waikato.ac.nz

You can contact staff by:

  • Calling +64 7 838 4466 select option 1, then enter the extension.
  • Extensions starting with 4, 5 or 9 can also be direct dialled:
    • For extensions starting with 4: dial +64 7 838 extension.
    • For extensions starting with 5: dial +64 7 858 extension.
    • For extensions starting with 9: dial +64 7 837 extension.
Edit Staff Content

Paper Description

Edit Paper Description Content

This paper shows how reactive systems are modelled and analysed using finite-state machines and temporal logic, and how model checking tools can be used to verify crucial properties of safety-critical system. The paper also provides an introduction to the algorithms and data structures used to model-check very large finite-state systems.

Edit Paper Description Content

Paper Structure

Edit Paper Structure Content

There will be assignments used to practice the use of two different model checkers, as well as one Test to assess the theoretical aspects of temporal logic and model checking algorithms. During a final assignment, students will have the opportunity to build their own model checker.

Edit Paper Structure Content

Learning Outcomes

Edit Learning Outcomes Content

Students who successfully complete the course should be able to:

  • Specify the behaviour of reactive systems using finite-state machines and temporal logic
    Linked to the following assessments:
  • Use model checkers to check whether crucial properties are satisfied, and understand the way how model checkers work.
    Linked to the following assessments:
Edit Learning Outcomes Content
Edit Learning Outcomes Content

Assessment

Edit Assessments Content
This paper is fully internally assessed. There will be three computer-based assignments, each using a different model checking environment. An in-class test will assess competency in the theoretic aspects of model checking.
Edit Additional Assessment Information Content

Assessment Components

Edit Assessments Content

The internal assessment/exam ratio (as stated in the University Calendar) is 100:0. There is no final exam. The final exam makes up 0% of the overall mark.

The internal assessment/exam ratio (as stated in the University Calendar) is 100:0 or 0:0, whichever is more favourable for the student. The final exam makes up either 0% or 0% of the overall mark.

Component DescriptionDue Date TimePercentage of overall markSubmission MethodCompulsory
1. Assignment 1
18 Mar 2019
10:00 AM
20
  • Online: Submit through Moodle
2. Assignment 2
8 Apr 2019
10:00 AM
20
  • Online: Submit through Moodle
  • Hand-in: Assignment Box (G Block)
3. Test
10 May 2019
10:00 AM
30
  • In Class: In Lecture
4. Assignment 3
4 Jun 2019
10:00 AM
30
  • Online: Submit through Moodle
  • Hand-in: Assignment Box (G Block)
Assessment Total:     100    
Failing to complete a compulsory assessment component of a paper will result in an IC grade
Edit Assessments Content

Required and Recommended Readings

Edit Required Readings Content

Required Readings

Edit Required Readings Content
  • B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer, 2001.
  • Michael Huth, Mark Ryan, Logic in Computer Science, 2nd edition, Cambridge University Press, 2004.
Edit Required Readings Content

Online Support

Edit Online Support Content
Edit Online Support Content

Workload

Edit Workload Content

Students are expected to spend about 12 hours per week on this paper as follows:

  • two hours in lectures
  • four hours reading and thinking
  • six hours on the assignments
Edit Workload Content

Linkages to Other Papers

Edit Linkages Content

Prerequisite(s)

Prerequisite papers: COMP235 or COMPX361 and a further 45 points at 300 level in Computer Science

Corequisite(s)

Equivalent(s)

Restriction(s)

Restricted papers: COMP452, COMP552

Edit Linkages Content