Skip to main content

Module

CSC8204 : High Integrity Software Development

  • Offered for Year: 2021/22
  • Module Leader(s): Dr Stephen Riddle
  • Lecturer: Dr Leo Freitas
  • Owning School: Computing
  • Teaching Location: Newcastle City Campus
Semesters
Semester 1 Credit Value: 10
ECTS Credits: 5.0

Aims

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 materials81:008:00Recorded lectures
Scheduled Learning And Teaching ActivitiesLecture81:008:00Lectures in person OR online scheduled
Guided Independent StudyDirected research and reading241:0024:00Background reading
Scheduled Learning And Teaching ActivitiesSmall group teaching101:0010:00Practicals as present in person OR Online scheduled
Guided Independent StudyProject work341:0034:00Coursework (2 pieces)
Guided Independent StudyIndependent study161:0016:00Lecture follow-up
Total100:00
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 report1M5017 hours exercises in logic and proof
Practical/lab report1M5017 hours programming assignment
Assessment Rationale And Relationship

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

Reading Lists

Timetable