Newcastle University > Undergraduate > Find a Degree > Module

• Offered for Year: 2020/21

• Module Leader(s): Dr Leo Freitas
• Teaching Assistant: Mr Chris Napier

• Owning School: Computing
• Teaching Location: Newcastle City Campus

Semesters

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
1.1.       The nature of software (SW) verification; verification principles (correctness, concurrency, abstraction, refinement, design decisions, documented assumptions, model-based testing)
1.2.       Understanding expertise required and costs involved; identifying the right technique to the task at hand.
2.       Modelling and Specification
2.1.       From a requirements document and produce an initial abstract specification of the problem.
2.2.       Elicit properties of interest from these requirements as formal consistency conditions, and make a specification of them that is amenable to analysis and verification.
2.3.       Foundations of formal modelling: propositional and predicate logic, data types and invariants; state-based models; mathematical toolkits.
2.4.       Propose design decisions as improved specifications; designs must be amenable to proof and consistency checking of desired properties;
2.5.       Possibly propose code-level contracts from formal design.
3.       Verification & Validation
3.1.       Understand verification support systems able to discharge formal consistency conditions from modelling activities
3.2.       Understand what it means for one specification to be a design refinement of another by establishing a link from the requirements to code-contracts
3.3.       Study alternative (to formal) techniques aiming at understanding the costs and conditions under which to undertake a formal or rigorous development process.
3.4.       Understand the importance of automated proof support and proof engineering (i.e. the process of mechanising a complex model)
3.5.       Metrics for complexity, reliability, expertise, time costs

Teaching Methods

Please note that module leaders are reviewing the module teaching and assessment methods for Semester 2 modules, in light of the Covid-19 restrictions. There may also be a few further changes to Semester 1 modules. Final information will be available by the end of August 2020 in for Semester 1 modules and the end of October 2020 for Semester 2 modules.

Teaching Activities

Teaching Rationale And Relationship

Lectures provide the knowledge. Practicals to provide additional background.

Assessment Methods

Please note that module leaders are reviewing the module teaching and assessment methods for Semester 2 modules, in light of the Covid-19 restrictions. There may also be a few further changes to Semester 1 modules. Final information will be available by the end of August 2020 in for Semester 1 modules and the end of October 2020 for Semester 2 modules.

The format of resits will be determined by the Board of Examiners

Exams

Other Assessment

Assessment Rationale And Relationship

The open book exam will assess knowledge. Coursework to reinforce some of the lecture material.

Study abroad students considering this module should contact the School to discuss its availability and assessment.

N.B. This module has both “Exam Assessment” and “Other Assessment” (e.g. coursework). If the total mark for either assessment falls below 35%, the maximum mark returned for the module will normally be 35%.

Reading Lists

• CSC3323's Reading List

Timetable

• Timetable Website: www.ncl.ac.uk/timetable/
• CSC3323's Timetable