CSC3323 : Software Verification Technologies
- Offered for Year: 2021/22
- Module Leader(s): Dr Leo Freitas
- Owning School: Computing
- Teaching Location: Newcastle City Campus
Semesters
| Semester 1 Credit Value: | 10 |
| ECTS Credits: | 5.0 |
Aims
To train students with practical aspects of formal modelling and verification technology as parts of a well-founded set of tools and techniques within software engineering.
Outline Of Syllabus
1. Background
2. The nature of software (SW) verification; verification principles (correctness, concurrency, abstraction, refinement, design decisions, documented assumptions, model-based testing)
3. Understanding expertise required and costs involved; identifying the right technique to the task at hand.
4. Modelling and Specification
5. From a requirements document and produce an initial abstract specification of the problem.
6. Elicit properties of interest from these requirements as formal consistency conditions, and make a specification of them that is amenable to analysis and verification.
7. Foundations of formal modelling: propositional and predicate logic, data types and invariants; state-based models; mathematical toolkits.
8. Propose design decisions as improved specifications; designs must be amenable to proof and consistency checking of desired properties;
9. Possibly propose code-level contracts from formal design.
10. Verification & Validation
11. Understand verification support systems able to discharge formal consistency conditions from modelling activities
12. Understand what it means for one specification to be a design refinement of another by establishing a link from the requirements to code-contracts
13. Study alternative (to formal) techniques aiming at understanding the costs and conditions under which to undertake a formal or rigorous development process.
14. Understand the importance of automated proof support and proof engineering (i.e. the process of mechanising a complex model)
15. Metrics for complexity, reliability, expertise, time costs
Teaching Methods
Teaching Activities
| Category | Activity | Number | Length | Student Hours | Comment |
|---|---|---|---|---|---|
| Structured Guided Learning | Lecture materials | 10 | 1:00 | 10:00 | Recorded Lectures |
| Guided Independent Study | Assessment preparation and completion | 20 | 1:00 | 20:00 | Lecture follow-up |
| Scheduled Learning And Teaching Activities | Small group teaching | 12 | 1:00 | 12:00 | Synchronous online interactive session |
| Scheduled Learning And Teaching Activities | Small group teaching | 8 | 1:00 | 8:00 | Practicals as Present in Person OR Online scheduled |
| Guided Independent Study | Project work | 30 | 1:00 | 30:00 | Coursework |
| Guided Independent Study | Independent study | 20 | 1:00 | 20:00 | Background reading and tool usage practicing |
| Total | 100:00 |
Teaching Rationale And Relationship
Lectures provide the knowledge. Practicals to provide additional background.
Assessment Methods
The format of resits will be determined by the Board of Examiners
Other Assessment
| Description | Semester | When Set | Percentage | Comment |
|---|---|---|---|---|
| Design/Creative proj | 1 | M | 100 | n/a |
Assessment Rationale And Relationship
The coursework allows students to reflect upon the practical aspects of formal modelling and verification technology.
Reading Lists
Timetable
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC3323's Timetable