CSC8204 : High Integrity Software Development
- Offered for Year: 2022/23
- Module Leader(s): Dr Stephen Riddle
- 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 Learning | Lecture materials | 6 | 1:00 | 6:00 | Recorded online lecture and other material |
| Scheduled Learning And Teaching Activities | Lecture | 16 | 1:00 | 16:00 | Lectures in person OR online synchronous |
| Guided Independent Study | Directed research and reading | 18 | 1:00 | 18:00 | Background reading |
| Scheduled Learning And Teaching Activities | Small group teaching | 10 | 1:00 | 10:00 | Practicals/Workshops as present in person OR Online synchronous scheduled |
| Guided Independent Study | Project work | 34 | 1:00 | 34:00 | Coursework (1 pieces) |
| Guided Independent Study | Independent study | 16 | 1:00 | 16:00 | Lecture follow-up |
| Total | 100: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 report | 1 | M | 100 | 34 hours exercises in programming, logic and proof |
Formative Assessments
| Description | Semester | When Set | Comment |
|---|---|---|---|
| Practical/lab report | 1 | M | Formative 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
Timetable
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC8204's Timetable