School of Electronics and Computer Science:
COMP6004 Formal Design of Systems
Basic Information
| School | Dept- Electronics & Computer Science |
|---|---|
| Known as | COMP6004. |
| Status | This syllabus is still provisional. |
| Session and Semester | Semester Two, 2011 - 2012 |
| Credit | 20 Credit Points |
| Unit Leader | Dr Corina Cirstea |
| Teachers | Gennaro Parlato |
| Moderators | Dr Pawel Sobocinski |
| Study | 200 study hours |
| Assessment | Exam 50%, coursework 50% |
| Coursework | 2 courseworks |
| Teaching | 24 lectures |
| Referral | On referral, this unit will be assessed 100% by examination. |
| Syllabus Approved |
Description
Aims
The aim of this course is to expose students to mechanised formal tools which help ensure correctness and hence reliability of computer systems. Students will learn about the theory underlying model checking and will gain experience with model checking tools.
Learning Outcomes
Knowledge and Understanding
Having successfully completed the module, you will be able to demonstrate knowledge and understanding of:
- temporal logics
- the theoretical underpinnings of model checking
- model-checking tools and their uses
Intellectual Skills
Having successfully completed the module, you will be able to:
- compare and evaluate different verification systems
- appreciate when model checking is appropriate
Practical Skills
Having successfully completed the module, you will be able to:
- apply a verification tool (SPIN) to system analysis
General Transferable (key) Skills
Having successfully completed the module, you will be able to:
- summarise up-to-date research publications
Topics Covered
- Temporal logics
- Theory of model checking
- Model checking practice
- The SPIN model checker
- Familiarisation with tools that support the design of correct systems
- Other verification tools such as FDR, SMV, Alloy
- Designing systems rigorously
- Checking properties in a designed system (semi-) automatically
- Using counterexamples to eliminate errors
Teaching and learning activities
Teaching methods include
- Lectures (2 per week).
- Tutorials (1 per week).
Learning activities include
Small exercises aimed to aid students' understanding of temporal logics and of the theory underpinning model checking.
A coursework on modeling and verification using the SPIN model checker.
Methods of assessment
| Assessment method | Number | % contribution to final mark |
|---|---|---|
| Practical Application of Model Checking [cwork] | 2 | 50 |
| Written Examination [exam] | 1 | 50 |
Feedback and student support during module study
The tutorials will be used to discuss the solutions to exercises and to answer questions.
Detailed coursework feedback will be provided within 3 weeks of the submission deadline.
Relationship between the teaching, learning and assessment methods and the planned learning outcomes
The knowledge and understanding skills will be gained in the lectures/tutorials and by independent study, and will be assessed through the exam and the two courseworks.
The intellectual and practical skills will be gained through the two courseworks.
Resources
Background Resources
- Huth, M. and Ryan, M., Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004 [Library] [Shops]
- Clarke, E.M., Grumberg, O. and Peled D.A., Model-Checking, MIT Press, 1999 [Library] [Shops]
- Holzmann, G.D., The Spin Model Checker: Primer and Reference Manual, Addison Wesley 2003 [Library] [Shops]
Taught to
COMP6004
Computer Science Integrated PhD (Optional)Pt IV MEng Computer Science with Artificial Intelligence (Optional)
Pt IV MEng Computer Science (Optional)
Pt IV MEng Computer Science with Distributed Systems & Networks (Optional)
Pt IV MEng Computer Science with Image and Multimedia Systems (Optional)
Pt IV MEng Computer Science with Mobile and Secure Systems (Optional)
MSc in Software Engineering (Compulsory)
Pt IV MEng Electronic Engineering (Optional)
Pt IV MEng Electronic Engineering with Artificial Intelligence (Optional)
Pt IV MEng Electronic Engineering with Computer Systems (Optional)
Pt IV MEng Electronic Engineering with Nanotechnology (Optional)
Pt IV MEng Electronic Engineering with Optical Communications (Optional)
Pt IV MEng Electronic Engineering with Power Systems (Optional)
Pt IV MEng Electronic Engineering with Mobile and Secure Systems (Optional)
Pt IV MEng Electronic Engineering with Wireless Communications (Optional)
ECS Socrates Students (Optional)
MSc in System on Chip (Optional)
Pt IV MEng Software Engineering (Optional)
Students who are not registered on an ECS approved programme may take this module subject to meeting its pre-requisites and the availability of resources. To confirm this, please can you contact the module leader (as listed above) in the first instance. They will then refer you on to the appropriate director of studies for formal approval of your selection.
Change Log
2012-01-13 14:28:30.140 - cc22012-01-13 14:27:48.083 - cc2
2011-04-04 18:59:41.710 - Roll script