School of Electronics and Computer Science:
COMP3011 Critical Systems
Basic Information
| School | Dept- Electronics & Computer Science |
|---|---|
| Known as | COMP3011. |
| Session and Semester | Semester Two, 2011 - 2012 |
| Credit | 10 Credit Points |
| Unit Leader | Dr. Michael R. Poppleton |
| Moderators | Bernd Fischer |
| Study | 100 nominal hours, of which approximately 30% on coursework |
| Assessment | Examination 70%, Coursework 30% |
| Coursework | 1 formal design exercise |
| Teaching | Lectures 24 |
| Prerequisites and Exclusions | May not be taken with: Unknown code: COMP6014 . Prerequisites: (COMP1001 - Introduction to Formal Methods or ELEC2017 - ). |
| Referral | On referral, this unit will be assessed 100% by examination. |
| Syllabus Approved |
Description
Aims
Increasingly, computers are being used in so-called critical systems, i.e., systems where protection of the safety of humans and the environment and protection of valuable assets are of vital importance. Examples of such systems are Fly-by-Wire aircraft, Nuclear power-plant monitoring, and secure financial transactions.
In this course, we look at techniques used in critical system software development that help ensure greater reliability, in particular, the B formal method. Hazard analysis techniques are used to identify potential hazards (i.e., breaches of safety) in a system design. Formal methods are used in the design of computer systems in order to increase their dependability.
Learning Outcomes
Knowledge and Understanding
Having successfully completed the module, you will be able to demonstrate knowledge and understanding of:
- Understand the concepts and terminology of system safety.
- Understand approaches to risk and hazard analysis in system safety.
- Understand how the use of formal methods on system development improves dependability.
- Understand approaches to systems security assurance.
Intellectual Skills
Having successfully completed the module, you will be able to:
- Be able to apply hazard analysis techniques in practical system development.
- Be able to write system specifications using the B notation
- Be able to analyse specifications using the ProB tool and be able to refine simple specifications
General Transferable (key) Skills
Having successfully completed the module, you will be able to:
Perform basic risk assessment of working or public environments
Topics Covered
- System safety: concepts and terminology.
- Risk assessment in system safety.
- Introduction to hazard analysis techniques: Fault-Tree Analysis, HAZOP, FME Analysis.
- Assurance of system security.
- Overview of formal methods and their role in ensuring safety.
- B formal method: notation methodology, toolkit.
Teaching and learning activities
Teaching methods include
Lectures (up to 2 per week) are used to introduce safety concepts, hazard analysis techniques and formal specification and analysis using B. Case studies are used to instruct students on the application of the techniques.
Learning activities include
The coursework is used to develop the students ability to apply hazard analysis and formal modelling to safety-critical systems.
Methods of assessment
| Assessment method | Number | % contribution to final mark |
|---|---|---|
| Exam [exam] | 1 | 70 |
| Coursework [cwork] | 1 | 30 |
Feedback and student support during module study
Two or three tutorial slots are used to work through selected B modelling examples, in support of the B lectures.
While the coursework is on-going, a tutorial slot is set aside to provide support and answer queries about the coursework. Feedback is also provided when the coursework is marked.
Relationship between the teaching, learning and assessment methods and the planned learning outcomes
The knowledge and understanding skills listed above will be taught in lectures. The intellectual skills will be taught through applications of the analysis techniques to case studies in lectures and re-inforced through the coursework.
The purpose of the exam is to test understanding of topics that it is difficult to fully assess in an assignment, and also to allow students to show that the abilities demonstrated in the coursework are their own.
Resources
Core Resources
- Steve Schneider, The B-Method: An Introduction. Palgrave 2001.
- Neil Storey, Safety Critical Computer Systems, Prentice Hall, 1996
Background Resources
- J.-R. Abrial, The B-Book, Cambridge University Press, 1996.
- K. Lano, The B Language and Method., Springer 1996
- J.B. Wordsworth, Software Engineering with B., Addison-Wesley 1996.
- Web sites such as:http://www.comlab.ox.ac.uk/archive/safety.html
- Nancy G. Leveson, Safeware: System Safety and Computers, , Addison-Wesley 1995.
Taught to
COMP3011
Non-existing cohort: "ceMEng3" (Optional)Pt III BSc Computer Science (Optional)
Non-existing cohort: "csBScAi3" (Optional)
Non-existing cohort: "csBScDs3" (Optional)
Non-existing cohort: "csBScIm3" (Optional)
Computer Science Integrated PhD (Optional)
Pt III MEng Computer Science with Artificial Intelligence (Optional)
Pt III MEng Computer Science (Optional)
Pt III MEng Computer Science with Distributed Systems & Networks (Optional)
Pt III MEng Computer Science with Image and Multimedia Systems (Optional)
Pt III MEng Computer Science with Mobile and Secure Systems (Optional)
ECS Socrates Students (Optional)
Pt III BEng Software Engineering (Optional)
Pt III 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.