CSC3323 : Software Verification Technologies (Inactive)
CSC3323 : Software Verification Technologies (Inactive)
- Inactive for Year: 2024/25
- Module Leader(s): Dr Leo Freitas
- Owning School: Computing
- Teaching Location: Newcastle City Campus
Semesters
Your programme is made up of credits, the total differs on programme to programme.
| Semester 1 Credit Value: | 10 |
| ECTS Credits: | 5.0 |
| European Credit Transfer System | |
Pre-requisite
Modules you must have done previously to study this module
| Code | Title |
|---|---|
| CSC2021 | |
| CSC2023 |
Pre Requisite Comment
N/A
Co-Requisite
Modules you need to take at the same time
Co Requisite Comment
N/A
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
Learning Outcomes
Intended Knowledge Outcomes
On successful completion of the module, students will be able to describe:
1. How abstraction can be used to capture informal requirements as a formal (mathematical) specification
2. One or more formal specification languages (i.e. modelling language, proof support system language).
3. What can be claimed about the system under design
4. A working knowledge of proof support systems
Intended Skill Outcomes
To be able to make an informed choice from a range of formal software engineering tools and techniques, and to apply them to the development of realistic software and systems.
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.
Reading Lists
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.
Timetable
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC3323's Timetable
Past Exam Papers
- Exam Papers Online : www.ncl.ac.uk/exam.papers/
- CSC3323's past Exam Papers
General Notes
N/A
Welcome to Newcastle University Module Catalogue
This is where you will be able to find all key information about modules on your programme of study. It will help you make an informed decision on the options available to you within your programme.
You may have some queries about the modules available to you. Your school office will be able to signpost you to someone who will support you with any queries.
Disclaimer
The information contained within the Module Catalogue relates to the 2024 academic year.
In accordance with University Terms and Conditions, the University makes all reasonable efforts to deliver the modules as described.
Modules may be amended on an annual basis to take account of changing staff expertise, developments in the discipline, the requirements of external bodies and partners, and student feedback. Module information for the 2025/26 entry will be published here in early-April 2025. Queries about information in the Module Catalogue should in the first instance be addressed to your School Office.