Skip to main content

Module

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 LearningLecture materials101:0010:00Recorded Lectures
Guided Independent StudyAssessment preparation and completion201:0020:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesSmall group teaching121:0012:00Synchronous online interactive session
Scheduled Learning And Teaching ActivitiesSmall group teaching81:008:00Practicals as Present in Person OR Online scheduled
Guided Independent StudyProject work301:0030:00Coursework
Guided Independent StudyIndependent study201:0020:00Background reading and tool usage practicing
Total100: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 proj1M100n/a
Assessment Rationale And Relationship

The coursework allows students to reflect upon the practical aspects of formal modelling and verification technology.

Reading Lists

Timetable