CSC8105 : System Validation
- Offered for Year: 2021/22
- Module Leader(s): Professor Maciej Koutny
- Owning School: Computing
- Teaching Location: Newcastle City Campus
Semesters
| Semester 1 Credit Value: | 10 |
| ECTS Credits: | 5.0 |
Aims
To introduce basic formal techniques and computer aided verification topics relevant to the design and validation of concurrent and distributed computing systems.
To introduce methods and algorithms aimed at coping with the high complexity of concurrent and distributed designs.
To become familiar with an industrial strength protocol specification language and validation tool
Outline Of Syllabus
The role of formal techniques supporting specification and computer aided verification in the design and validation of concurrent and distributed computing systems.
Automata based models for the verification of behavioural properties of concurrent and distributed computing systems.
Verification techniques based on the state space exploration: coping with the state space explosion problem.
Examples of other verification techniques, such as bisimulation.
High level specification and computer aided verification of communication protocols.
Teaching Methods
Teaching Activities
| Category | Activity | Number | Length | Student Hours | Comment |
|---|---|---|---|---|---|
| Scheduled Learning And Teaching Activities | Lecture | 16 | 1:00 | 16:00 | Lectures |
| Guided Independent Study | Assessment preparation and completion | 18 | 1:00 | 18:00 | Lecture follow-up |
| Guided Independent Study | Assessment preparation and completion | 22 | 0:30 | 11:00 | Revision for end of Semester exam & exam duration |
| Scheduled Learning And Teaching Activities | Practical | 14 | 1:00 | 14:00 | practicals |
| Guided Independent Study | Project work | 28 | 1:00 | 28:00 | coursework |
| Guided Independent Study | Independent study | 11 | 1:00 | 11:00 | Background reading |
| Scheduled Learning And Teaching Activities | Scheduled on-line contact time | 2 | 1:00 | 2:00 | Preparation and guidance related to module coursework |
| Total | 100:00 |
Teaching Rationale And Relationship
Lectures will be used to introduce the learning material and for demonstrating the key concepts by example. Students are expected to follow-up lectures within a few days by re-reading and annotating lecture notes to aid deep learning.
This is a very practical subject, and it is important that the learning materials are supported by hands-on opportunities provided by practical classes. Students are expected to spend time on coursework outside timetabled practical classes.
Students aiming for 1st class marks are expected to widen their knowledge beyond the content of lecture notes through background reading.
Students should set aside sufficient time to revise for the end of semester exam.
Assessment Methods
The format of resits will be determined by the Board of Examiners
Exams
| Description | Length | Semester | When Set | Percentage | Comment |
|---|---|---|---|---|---|
| Written Examination | 90 | 1 | A | 66 | N/A |
Other Assessment
| Description | Semester | When Set | Percentage | Comment |
|---|---|---|---|---|
| Practical/lab report | 1 | M | 34 | Validation coursework (40 hours) |
Assessment Rationale And Relationship
The examination is an appropriate way to assess knowledge of the principles and theory of validation technology, as well as testing application skills on small-scale problems. The coursework assessment permits the assessment of practical skills relating to computer-aided validation and tool support on more open-ended problems, as well as formal modelling of concurrent and distributed software systems.
The examination involves the correct interpretation and analysis of precise formal models. Its duration is set to allow time for this to be done accurately.
Study abroad students may request to take their exam before the semester 1 exam period, in which case the length of the exam may differ from that shown in MOFS.
The alternate assessment plan: In case exams cannot run due to Covid, a 24 hour exam will be provided which can be taken from home.
N.B. This module has both “Exam Assessment” and “Other Assessment” (e.g. coursework). If the total mark for either assessment falls below 40%, the maximum mark returned for the module will normally be 40%.
Reading Lists
Timetable
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC8105's Timetable