Computer Science Home | People | Degrees | Papers | Research | Events | Other FCMS Subjects
 
Level 1 Papers

Level 2 Papers

Level 3 Papers

Level 4 Papers

Level 5 Papers

Summer School Papers

Industry Papers

CGRD524
Interaction Design

CGRD532
Information Visualisation

CGRD551
Studio Management

CGRD581
Report of an Investigation

CGRD591
Dissertation and Exhibition (1 Paper)

CGRD592
Dissertation and Exhibition (2 Paper)

CGRD593
Computer Graphic Design Thesis and Realisation

CGRD594
Computer Graphic Design Thesis and Realisation

COMP513
Computer Networks

COMP514
Carrier and ISP Networks

COMP518
Cyber Security

COMP520
Report of an Investigation

COMP521
Machine Learning Algorithms

COMP523
Data Stream Mining

COMP524
Interaction Design

COMP532
Information Visualisation

COMP536
Advanced Graphics and Computer Games

COMP539
Usability Engineering

COMP540
Software Engineering Methodologies

COMP542
Web Search: Technical and Social Issues

COMP548
Developing Mobile Applications

COMP550
Location-Based Systems as Context-Aware Systems

COMP552
Model Checking

COMP553
Extremely Parallel Programming

COMP554
Specification Languages and Models

COMP555
Bioinformatics

COMP556
Computational Finance

COMP560
Turing Topics in Computer Science

COMP589
Programming for Research

COMP590
Research in Computer Science

COMP591
Dissertation (1 Paper)

COMP592
Dissertation (2 Papers)

COMP593
Computer Science Thesis (3 papers)

COMP594
Computer Science Thesis (4 Papers)

2013 Papers
Level 5 Papers >> All Papers
COMP552A Model Checking

15 Points

This paper shows how reactive systems can be 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 systems. The paper also provides an introduction into the algorithms and data structures used to model check very large finite-state systems.

There will be assignments to practice the use of two different model checkers, and a test will 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.

Learning Outcomes
Having completed this paper, students will be able to specify the behaviour of reactive systems using finite-state machines and temporal logic. They will be able to use model checkers to check whether crucial properties are satisfied, and understand the way how model checkers work.

This paper contributes to the capabilities 1, 2, 4, 5, 6, 8, and 9 of the Software Engineering Graduate Profile.

Pre Requisite Papers
COMP235 Logic and Computation and
60 points at 300 level in Computer Science

Students entering this paper are expected to know about propositional logic and finite-state machines. The final assignment requires Java programming skils.

Corresponding Papers
COMP452 Model Checking

Lecturers and Tutors

A Semester

    Lecturer(s)

    • Dr. Robi Malik
      Room: G.2.23
      Phone: +64 7 838 4796


Moodle Link

Timetable
Official Timetable Information

Workload
Students are expected to spend about twelve hours per week on this paper: two hours in lectures, four hours reading and thinking, and six hours on the assignments.

Required Reading
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.

Computing Resources
The Linux computers in Computing Laboratory 6 (R G.18) can be used for the assignments.

Means of Assessment
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.

Assessment Ratio
Internal assessment/final examination ratio 1:0

Assessment Components

Assignment 1. Due Mon 18 Mar 9:00 A.M. Weight 20%
Assignment 2. Due Mon 15 Apr 9:00 A.M. Weight 20%
Test. Held Fri 10 May 9:00 A.M. Weight 30%
Assignment 4. Due Tue 4 Jun 9:00 A.M. Weight 30%

Grading Schedule
Numerical marks will be used to grade assignments and tests, with detailed schedules provided with each assessment item. The weighted total of marks over all assessment items will determine the final grade based on the University grading schedule.
An overall mark of 50% is required for a pass.

Assessment Deadlines
Assignment submission deadlines are firm. Late submissions will not be accepted.

Hand in and Return of Assignments
Assignment submission requirements will vary depending on the nature of each assignment, and specific instructions will be provided with each assignment. There will be electronic submissions through Moodle, plus paper components to be placed in a drop-in box.
Marked assignments and tests will usually be returned to students during the supervised lab following the submission deadline.

Attendance Policy
Class attendance is expected. The course notes provided are not comprehensive, additional material will be covered in class. You are responsible for all material covered in class.

Student Representatives
Colin Pilbrow

Academic Integrity
Follow this link for Academic Integrity information.

Performance Impairment
Follow this link for information on Performance Impairment.

Student Concerns and Complaints
Follow this link for Student Concerns and Complaints information.

Application for Extension
Follow this link for information on applying for an Extension.

Review of Grade
Follow this link for information on applying for a Review of Grade.

University Regulations
Your attention is drawn to the following regulations and policies, which are published in the University Calendar:

  © 2007 FCMS. The University of Waikato - Te Whare Wananga o Waikato