COMPX554-21B (HAM)

Specification Languages and Models

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)

Steve Reeves

Steve Reeves
4398
G.1.26
See Moodle
steve.reeves@waikato.ac.nz

Lecturer(s)

Colin Pilbrow

Colin Pilbrow
9584
G.1.29
See Moodle
colin.pilbrow@waikato.ac.nz

Administrator(s)

: rachael.foote@waikato.ac.nz

Placement/WIL Coordinator(s)

Tutor(s)

Student Representative(s)

Lab Technician(s)

Librarian(s)

: alistair.lamb@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, 9 or 3 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.
    • For extensions starting with 3: dial +64 7 2620 + the last 3 digits of the extension e.g. 3123 = +64 7 262 0123.
Edit Staff Content

Paper Description

Edit Paper Description Content

This paper deals with various aspects of modelling systems using advanced, "good practice" methods from the software engineering field (specifically advanced software modelling and advanced software validation from the SWEBoK descriptions). To do this it will introduce at least one of the main software modelling, validation and verification languages, Z, including its semantics, logic and associated tools. It will also introduce the concept of refinement and its use in validating models against requirements and verifying implementations against the models.

Edit Paper Description Content

Paper Structure

Edit Paper Structure Content
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.
Edit Paper Structure Content

Learning Outcomes

Edit Learning Outcomes Content

Students who successfully complete the paper should be able to:

  • Modelling, reasoning, testing and proof
    Students will be able to build models of systems in a specification language like Z. They will also be able to use such models as a basis for arguing for the correctness of the model relative to the requirements. Further, they will see how to use such models as a basis for validation and verification using a modern, industry-standard tool (ProB).
    Linked to the following assessments:
Edit Learning Outcomes Content
Edit Learning Outcomes Content

Assessment

Edit Assessments 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. Using Z---Introduction to modelling and abstraction
20
  • Other: Via Moodle
2. Investigating Models---using specifications and a tool to validate
30
  • Other: Via Moodle
3. Specifying a security system---using all the previous work
50
  • Other: Via Moodle
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

"Using Z", Jim Woodcock and Jim Davies, Prentice-Hall Internaitonal Series on Computer Science, C.A.R.Hoare (ed.), Prentice-Hall, 1996.

Note that this book is now on line, for free! Go to usingz.com.

Edit Required Readings Content

Other Resources

Edit Other Resources Content
The ProB website (and associated downloads) might be useful.
Edit Other Resources Content

Online Support

Edit Online Support Content
All online support is accessible via Moodle or email direct to me.
Edit Online Support Content

Workload

Edit Workload Content
We have just two hours of tutorial contact per week, so I expect you to work around 12 more hours per week (averaged over the semester, perhaps) on the paper.
Edit Workload Content

Linkages to Other Papers

Edit Linkages Content
COMP235 Logic and Computation, COMP340 Reasoning about Programs, and a further 40 points at 300 level in Computer Science.
Edit Linkages Content

Prerequisite(s)

Prerequisite papers: COMPX361 or (COMP235 and COMP340) and a further 30 points at 300 level in Computer Science

Corequisite(s)

Equivalent(s)

Restriction(s)

Restricted papers: COMP454, COMP554

Edit Linkages Content