Specification Languages and Models
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.
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.
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:
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.
Error: Assessment components must add up to 100%
At least one Assessment Component needs to be entered
|Component Description||Due Date||Time||Percentage of overall mark||Submission Method||Compulsory|
|1. Using Z---Introduction to modelling and abstraction||
|2. Investigating Models---using specifications and a tool to validate||
|3. Specifying a security system---using all the previous work||
Required and Recommended Readings*
"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.
Linkages to Other Papers*
Prerequisite papers: COMPX361 or (COMP235 and COMP340) and a further 30 points at 300 level in Computer Science
Restricted papers: COMP454, COMP554