School of Computing Science

School of Computing Science

CSC8204 : High Integrity Software Development

  • Offered for Year: 2016/17
  • Module Leader(s): Dr Stephen Riddle
  • Lecturer: Dr Leo Freitas
  • Owning School: Computing Science
  • Teaching Location: Newcastle City Campus
Semesters
Semester 1 Credit Value: 10
ECTS Credits: 5.0
Pre Requisites
Pre Requisite Comment

N/A

Co Requisites
Co Requisite Comment

N/A

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

Learning Outcomes

Intended Knowledge Outcomes

To be able to describe and discuss:
- processes and techniques for development of high-integrity software,
- pitfalls of "standard" programming languages and the motivation for safe subsets of programming languages,
- the role of techniques and tools to develop and analyse software.

Intended Skill Outcomes

The ability to select and apply techniques for development of high-integrity software.
The ability to critically analyse software and explain safety implications.
The ability to justify design decisions to a high level of rigour as part of a dependability case.

Graduate Skills Framework

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

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Scheduled Learning And Teaching ActivitiesLecture201:0020:00Lectures
Guided Independent StudyAssessment preparation and completion240:3012:00Revision for end of Semester exam & exam duration
Guided Independent StudyAssessment preparation and completion201:0020:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesPractical101:0010:00Practicals
Guided Independent StudyProject work201:0020:00Coursework
Guided Independent StudyIndependent study181:0018: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 Examination901A60N/A
Other Assessment
Description Semester When Set Percentage Comment
Practical/lab report1M2010 hours
Practical/lab report1M2010 hours
Assessment Rationale And Relationship

The written examination assesses the attainment of knowledge outcomes in the context of high-integrity software development. The coursework assessment assesses the design, tools selection and assessment skills on a substantial problem.


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 the MOF.

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.