Assured Software Engineering and Proof (ASEP) teaches participants state-of-the-art techniques in assured development using model-based engineering and formal methods. These techniques are essential for development of safety- and security-critical systems including, for example, mobile and autonomous robots, which is a particular research focus at York. The importance of formal methods is reflected by their inclusion in several international standards, such as DO-178C for aerospace applications.

Course Description

Assured Software Engineering and Proof (ASEP) teaches participants state-of-the-art techniques in assured development using model-based engineering and formal methods. These techniques are essential for development of safety- and security-critical systems including, for example, mobile and autonomous robots, which is a particular research focus at York. The importance of formal methods is reflected by their inclusion in several international standards, such as DO-178C for aerospace applications.

This CPD will train participants to apply techniques like automated theorem proving and model checking in assured development. We will focus on the Isabelle system, which harnesses advanced techniques like functional programming, deductive proof, automated verification, and code generation. With Isabelle, we can subject models and programs to various analyses to find errors and requirement violations. We can also use code generation for rapid prototyping, where code can be synthesised automatically from models and executed for design space exploration.

Who is this course for?
This course is suitable for:

Practitioners across all domains including aerospace, military, railway, automotive, civil nuclear, civil maritime, medical devices and healthcare;
Developers of equipment safety cases during design for software, hardware, procedures, systems and/or platforms;
Developers of safety cases for operational safety and disposal;
Reviewers of safety cases within an organisation or as an independent activity;
Developers and reviewers of changes to existing safety-critical / safety-related equipment and operations;
Project managers where development of a safety case is a significant element of projects they manage;
Regulators of safety critical domains.

Learning outcomes
On this course you will:

Understand how model-based engineering benefits from formal verification techniques.
Apply interactive theorem proving using the Isabelle system.
Write and verify functional programs using theorem proving in Higher Order Logic.
Model, animate, and verify systems using specifications with pre- and post-conditions in the Z notation.
Apply techniques like refinement and promotion to support stepwise development of models and programs.