Formal Models and Formal Requirements
industrial collaborators:
academic collaborators: University of Edinburgh
initiated : 2009/08/01
last updated: 2010/07/20

selected page:

Project staff and support

Marek Kwiatkowski (Intern, The University of Edinburgh)
Marcelin Fortes da Cruz (Company Supervisor, Airbus)
Sanjiv Sharma (Company Supervisor, Airbus)
Ian Stark (Academic Mentor, The University of Edinburgh)
Tristram Armour (Technology Translator, Industrial Mathematics KTN)

This Internship project was carried out at Airbus, in conjunction with the University of Edinburgh. It is part of the KTN's Industrial Mathematics Internships Programme, co-funded by EPSRC. Start date: August 2009; duration: 6 months.

"We are very pleased to report that Marek Kwiatkowski was a great addition to our team and produced some excellent work. Marek’s work enabled us to make significant progress in our broader researcher programme. A notable outcome was a jointly authored paper, Formal assessment of hybrid functions, which had been accepted for publication and oral presentation at the Embedded Real-Time Software 2010 Conference. We presented it on 20th May in Toulouse and received many positive comments on the quality of the work," said industrial supervisor, Sanjiv Sharma.

Project Summary

Airbus specifies, designs and implements complex mechatronic functions into systems featuring analogue and digital data and signals, and where continuous controls interact in various physical domains as well as with discrete reactive controls. The braking system, where the wheel-tyre-brake assembly, the electro-hydro-mechanical control loop and the reactive control interact, can serve as an example.

The interplay of continuous and discrete features - their hybrid nature - lies at the heart of these functions, and thus cannot be ignored in the process of their design, validation and implementation. The main aim of this project is to explore the potential for automated (i.e. performed by a computer) verification of hybrid designs. The topic of formalisation of engineering specifications features prominently in this work, because it is a prerequisite for any kind of automated analysis.

The outcomes and benefits

The adoption of process algebras by Airbus is particularly important because of the necessity to reason about behaviour. If the required engineering specification language had a process algebra as its core, then a formal notion of behaviour would be associated with every specification and furthermore, this notion would be susceptible to inductive reasoning. Moreover, the use of a parsimonious process algebra as an intermediate language would potentially simplify the implementation of any software tools.

related resources:
» Formal Models and Formal Requirements
  Technical Summary
other projects:
[Find other Aerospace and defence projects]