Skip to main content


CSC8204 : High Integrity Software Development

  • Offered for Year: 2022/23
  • Module Leader(s): Dr Stephen Riddle
  • Owning School: Computing
  • Teaching Location: Newcastle City Campus
Semester 1 Credit Value: 10
ECTS Credits: 5.0


To introduce principles of high-integrity systems programming, use of restricted language sets and analysis techniques to develop dependable software

An increasing range of tools are available for the development of secure and dependable systems. This module introduces the programming principles that underpin systems that have predictable levels of dependability and shows how those principles are realised in the leading high-integrity programming systems. The module has a strong practical component.

Outline Of Syllabus

1.       High-Integrity and Safety-Critical Systems Context
1.1.       Nature of software, faults and failures
1.2.       Contract based development
1.3.       Correctness: partial and total
2.       Logic & Proof
2.1.       Propositional logic, inference rules, natural deduction, automated proof rules
2.2.       Predicate calculus and algebraic proof
3.       High-Integrity Languages
3.1.       Language principles
3.2.       Ada and SPARK language
3.2.1. Data information for flow analysis
3.2.2. Proof annotations
3.3.       SPARK static analysis and proof tools
3.3.1. Generation and simplification of verification conditions for partial correctness, exception freedom

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Structured Guided LearningLecture materials61:006:00Recorded online lecture and other material
Scheduled Learning And Teaching ActivitiesLecture161:0016:00Lectures in person OR online synchronous
Guided Independent StudyDirected research and reading181:0018:00Background reading
Scheduled Learning And Teaching ActivitiesSmall group teaching101:0010:00Practicals/Workshops as present in person OR Online synchronous scheduled
Guided Independent StudyProject work341:0034:00Coursework (1 pieces)
Guided Independent StudyIndependent study161:0016:00Lecture follow-up
Teaching Rationale And Relationship

Introductory lecture and recorded lecture materials 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 opportunities provided by practical classes, either in person or supported online. 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

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

Other Assessment
Description Semester When Set Percentage Comment
Practical/lab report1M10034 hours exercises in programming, logic and proof
Formative Assessments
Description Semester When Set Comment
Practical/lab report1MFormative tutorial exercises in high integrity programming
Assessment Rationale And Relationship

The coursework assessment assesses the design, tools selection and assessment skills on a substantial problem.

Reading Lists