Assured Software Engineering and Proof (ASEP)
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.
Contact us
Toshiko Smith
MSc SCSE and Short Courses Team
Tom Rawle
Business and Partnership Manager
University of York CPD Team for Generative AI in Engineering and Manufacturing
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.
Prerequisites
A Bachelor's degree in Computer Science or equivalent.
If you are unsure about your previous experience, please email the CPD Team at cs-cpd@york.ac.uk so that we can assess your suitability for this course.
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.
How is this course taught?
The CPD will be taught over the course of 4 days. Half of the participants’ time will be spent in lectures, and the other half will be in problem-based learning classes (PBLs). The PBLs will provide the opportunity for participants to apply the theoretical knowledge they have learned. Typically, these will be composed of Isabelle-based exercises, which will be tackled in teams, and then answers presented to the whole group afterwards. The lectures are all also accompanied by Isabelle-based theory documents, which serve as interactive lecture notes.
When will this course be taught?
The course runs from 1pm on Monday 27 January until approximately 12.30pm on Friday 31 January 2025.
"A really good course. Helped understanding of the methods and specific tools. Definitely gained a better understanding of the formal methods and application within the industry domain. Gained more knowledge from the ASEP course and gave a better insight on the understanding and meaning. Would recommend to others for an understanding of the complexities of formal methods."
Software Assurance Engineer from Jacobs
Meet the lecturers
Book your place
Before you make your booking, please ensure that you have read our booking conditions.
Complete and return the form to cs-cpd
, 246kb)You can also pay for your course online.
You only need to complete the short booking form above, not the booking forms found on the online payment page.
Course fee: £2,500.00 GBP (VAT exempt)
To make a group booking please contact cs-cpd
Booking conditions
- Acceptance onto a short course is at the agreement of the course leader. They will want to assure themselves that you have the relevant level of background knowledge. You may therefore be asked to provide a CV detailing your knowledge / experience in particular areas.
- Course fees quoted include all relevant course materials, tuition, lunch and refreshments.
- For your place to be confirmed, a completed booking form with Purchase Order or payment is required before the course start date.
- Fees are payable to The University of York. Cheques should be drawn on a UK bank in pounds sterling and made payable to The University of York. Payment may also be made by Visa or Mastercard.
Cancellations
We regret that a fee must be charged when confirmed bookings are cancelled or transferred to future dates. In the event of a cancellation, you may nominate a substitute (acceptance of this substitution is subject to academic and availability conditions). If a suitable substitute cannot be found the following scale of charges will apply:
- 56 days or more before the course starts ‐ full refund
- 55 days or less ‐ 50% refund
- 28 days or less ‐ 25% refund
- 14 days or less ‐ no refund
We reserve the right to amend published information.
- Nikow, T. and Klein, G. Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/
- Woodcock J.C.P. and Davies J., Using Z: specification, refinement and proof, Prentice-Hall International, 1996
Contact us
Toshiko Smith
MSc SCSE and Short Courses Team
Tom Rawle
Business and Partnership Manager
University of York CPD Team for Generative AI in Engineering and Manufacturing