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

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 LearningLecture materials181:0018:00Recorded lectures
Guided Independent StudyDirected research and reading251:0025:00Background reading
Scheduled Learning And Teaching ActivitiesSmall group teaching41:004:00Practicals as present in person OR Online scheduled
Guided Independent StudyProject work341:0034:00Coursework (2 pieces)
Guided Independent StudyIndependent study181:0018:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesModule talk11:001:00Synchronous online introductory lecture
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

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