Runtime Quantitative Verification of Self-Adaptive AI Systems

 Principal Investigator: Dr Radu Calinescu
 Co-Investigator: Prof Richard Paige
 Type of project: Dstl National UK PhD programme
 Project partner:
    Defence Science & Technology Laboratory
 Start date: October 2012
 End date: September 2016

Project summary

The autonomous AI systems used in critical applications from domains as diverse as defence, security and space exploration face a double challenge:

These challenges have traditionally been addressed by researchers from different research areas. AI researchers have been developing systems capable of autonomous behaviour and self-adaptation for several decades. In contrast, formal specification, modelling, analysis and verification techniques are typically used to improve the integrity of systems whose functionality is fixed at design time.

This project will integrate techniques from both research areas, and develop a novel approach for the engineering of autonomous AI systems in which the compliance of the adaptation decisions with the system requirements will be verified formally, at runtime. The project will devise lightweight and scalable techniques for the analysis of key dependability, performance and cost properties of autonomous AI systems, and use them to develop software tools that support robust and predictable system adaptation. The new approach and tools for the engineering of autonomous AI systems will be validated in real-world case studies developed jointly with Dstl.


PhD student: Simos Gerasimou


R. Calinescu, K. Johnson, Y. Rafiq, S. Gerasimou, G. Costa Silva and S. N. Pehlivanov (2013) — Continual Verification of Non-Functional Properties in Cloud-Based Systems. Invited paper at the 5th International Workshop on Non-functional Properties in Modeling: Analysis, Languages, Processes, pages 1-5.

K. Johnson, R. Calinescu and S. Kikuchi (2013) — An Incremental Verification Framework for Component-Based Software Systems. In: 16th International ACM Sigsoft Symposium on Component-Based Software Engineering, 33-42.

R. Calinescu (2013) — Emerging Techniques for the Engineering of Self-Adaptive High-Integrity Software. To appear in: Javier Camara, Rogerio de Lemos, Carlo Ghezzi and Antonia Lopes (editors), Assurances for Self-Adaptive Systems, Springer.

R. Calinescu, C. Ghezzi, M. Kwiatkowska, R. Mirandola (2012) — Self-adaptive software needs quantitative verification at runtime, Communications of the ACM, 55(9):69-77, September 2012.