School of Computing Science

School of Computing Science

CSC8105 : System Validation

  • Offered for Year: 2016/17
  • Module Leader(s): Prof. Maciej Koutny
  • Owning School: Computing Science
  • Teaching Location: Newcastle City Campus
Semesters
Semester 1 Credit Value: 10
ECTS Credits: 5.0
Pre Requisites
Pre Requisite Comment

None

Co Requisites
Co Requisite Comment

None

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.

Learning Outcomes

Intended Knowledge Outcomes

The ability to describe and discuss:
- two complementary validation technologies.
- a leading software system for automated validation of high-level prototypes of distributed systems.
- the practical implications of the state space explosion problem for the complexity of validation of distributed and concurrent systems.
- different algorithms used to validate distributed systems in a rigorous manner.
- behavioural equivalence of different system designs.

Intended Skill Outcomes

The ability to:
- formulate a practical solution to a problem, making effective use of time and resources available.
- assimilate, evaluate and analyse information as a result of independent or group research.
- design and validate high-level prototypes of concurrent distributed computing systems.

Graduate Skills Framework

Graduate Skills Framework Applicable: Yes
  • Cognitive/Intellectual Skills
    • Critical Thinking : Assessed
    • Data Synthesis : Present
    • Active Learning : Present
    • Literacy : Present
    • Information Literacy
      • Source Materials : Present
      • Synthesise And Present Materials : Assessed
      • Use Of Computer Applications : Assessed
  • Self Management
    • Self Awareness And Reflection : Present
    • Planning and Organisation
      • Goal Setting And Action Planning : Present
    • Personal Enterprise
      • Innovation And Creativity : Assessed
      • Independence : Present
      • Problem Solving : Assessed
  • Interaction
    • Communication
      • Written Other : Present
  • Application
    • Occupational Awareness : Present

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Scheduled Learning And Teaching ActivitiesLecture181:0018:00Lectures
Guided Independent StudyAssessment preparation and completion220:3011:00Revision for end of Semester exam & exam duration
Guided Independent StudyAssessment preparation and completion181:0018:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesPractical141:0014:00Practicals
Guided Independent StudyProject work281:0028:00Coursework
Guided Independent StudyIndependent study111:0011:00Background reading
Total100: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.

Reading Lists

Assessment Methods

The format of resits will be determined by the Board of Examiners

Exams
Description Length Semester When Set Percentage Comment
Written Examination901A66N/A
Other Assessment
Description Semester When Set Percentage Comment
Practical/lab report1M34validation 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.

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%.

Timetable

Past Exam Papers

General Notes

N/A

Disclaimer: The University will use all reasonable endeavours to deliver modules in accordance with the descriptions set out in this catalogue. Every effort has been made to ensure the accuracy of the information, however, the University reserves the right to introduce changes to the information given including the addition, withdrawal or restructuring of modules if it considers such action to be necessary.