CSC8105 : System Validation
- Offered for Year: 2020/21
- 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
Please note that module leaders are reviewing the module teaching and assessment methods for Semester 2 modules, in light of the Covid-19 restrictions. There may also be a few further changes to Semester 1 modules. Final information will be available by the end of August 2020 in for Semester 1 modules and the end of October 2020 for Semester 2 modules.
Teaching Activities
| Category | Activity | Number | Length | Student Hours | Comment |
|---|---|---|---|---|---|
| Structured Guided Learning | Lecture materials | 18 | 0:40 | 12:00 | Lectures non-synchronous online |
| Guided Independent Study | Assessment preparation and completion | 32 | 1:00 | 32:00 | Coursework (modelling, coding and validation) |
| Guided Independent Study | Assessment preparation and completion | 6 | 1:00 | 6:00 | Writing up of report and collating validation results. |
| Scheduled Learning And Teaching Activities | Practical | 2 | 2:00 | 4:00 | Practicals (PiP) |
| Structured Guided Learning | Structured non-synchronous discussion | 20 | 1:00 | 20:00 | Lecture follow-up (Incl. Q&A) |
| Guided Independent Study | Independent study | 16 | 1:00 | 16:00 | Reviewing notes taken from recordings. |
| Guided Independent Study | Independent study | 10 | 1:00 | 10:00 | Reading of recommended texts on formal modelling and versifcation |
| 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.
Assessment Methods
Please note that module leaders are reviewing the module teaching and assessment methods for Semester 2 modules, in light of the Covid-19 restrictions. There may also be a few further changes to Semester 1 modules. Final information will be available by the end of August 2020 in for Semester 1 modules and the end of October 2020 for Semester 2 modules.
The format of resits will be determined by the Board of Examiners
Other Assessment
| Description | Semester | When Set | Percentage | Comment |
|---|---|---|---|---|
| Practical/lab report | 1 | M | 100 | Validation coursework (48 hours) One piece of coursework involving modelling, implementation and validation using tool support. |
Assessment Rationale And Relationship
The coursework assessment permits the assessment of practical skills relating to computer-aided validation and tool support, as well as formal modelling of concurrent and distributed software systems.
Reading Lists
Timetable
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC8105's Timetable