Skip to main content

Module

CSC8204 : High Integrity Software Development

  • Offered for Year: 2020/21
  • 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: SPARK
3.1.       Language principles
3.2.       Ada and SPARK language
3.2.1.       Annotations for flow analysis
3.2.2.       Proof annotations
3.3.       SPARK static analysis and proof tools
3.3.1.       Data and information flow analysis
3.3.2.       Generation and simplification of verification conditions for partial correctness, exception freedom

Teaching Methods

Module leaders are revising this content in light of the Covid 19 restrictions.
Revised and approved detail information will be available by 17 August.

Assessment Methods

Module leaders are revising this content in light of the Covid 19 restrictions.
Revised and approved detail information will be available by 17 August.

Reading Lists

Timetable