Engineering Doctorate (EngD) Studentship in Verification of High Integrity Software Product Lines - FULLY FUNDED, sponsored by Aero Engine Controls

Applications are invited for a Research Engineer to work on a research project in the verification of high-integrity software product lines, commencing asap. The research project is fully funded and will be carried out in conjunction with studying for an Engineering Doctorate (EngD) in Large Scale Complex IT Systems (LSCITS). The Programme is a full time, 4-year doctoral level research degree involving a taught component, similar in scope to an MSc, and a research component requiring the Research Engineer to work closely with a sponsoring organisation.

The Sponsoring Organisation: Aero Engine Controls (AEC)
The successful candidate will also be based at Aero Engine Controls (AEC) in Derby and will be assigned an industrial supervisor from AEC and an academic supervisor from the University of York.

The Research Project:

Verification is the major source of non-recurring cost in the development of high-integrity systems. Industry data shows that the verification effort can account for at least 50% of the development costs for traditional high-integrity lifecycles. Therefore, any benefits a software product line approach can bring to reducing the verification burden or spreading the cost of verification across multiple product instances would provide business benefit. Conversely, any product line practice that hinders verification or requires additional verification activities to be performed must be outweighed by cost and schedule savings elsewhere.

For verification to be cost effective within a high-integrity product line development as much verification evidence as possible needs to be provided as a core asset. However, this may not be achievable if approaches such as compositional development are adopted, and the transformations used are not property preserving

The verification challenge for high-integrity product lines is twofold; demonstrating that it is possible to perform the required verification on the product line and then to show that the verification evidence still holds for the product. There is little work in the literature that addresses these problems and this is a significant research challenge. The student will research approaches to the verification of product lines, in particular one or more of the following topics :

• Use of static analysis techniques, including the use of formal proof, to demonstrate a product asset has been composed correctly from a product line asset.
• Approaches to ensure that test data and evidence is compositional – tests for individual features are not compromised by the inclusion of other unrelated features.
• Approaches to capturing variability in test cases and procedures.

Applicants should be highly motivated and have a minimum of an upper second-class honours degree in Computer Science or Software Engineering or an MSc in Computer Science, Software Engineering or similar discipline. Candidates should also a strong background in software engineering, an understanding of embedded control system development, and good communication skills. Prior relevant commercial / industrial experience would be advantageous.