For almost four decades, formal methods have been considered as a software engineering approach to developing reliable systems. Their power lies in the use of a mathematical notation to specify properties of a system, and computer computation to check correctness of the same. Although formal methods have successfully evolved over the years to meet the requirements of modern software development, their application has been relatively slow. The problem is that to be applied successfully, formal methods need both engineering skills and expert knowledge. Lero has great capacity and research power in this field. Over the last years, Lero has been tackling some of the most challenging topics of formal methods:

  • Knowledge representation and reasoning: Tackles transferring data into context-relevant information and then that information into conclusions exhibiting knowledge. Moreover, it deals with the exhibition of artificial awareness.
  • Verification and validation: Deals with the problem of establishing trust in software-intensive systems, or how to prove software is correct, reliable and sound.

Safety: Adds to safety through formal verification and validation that allows for early detection of safety flaws. Moreover, it tackles the specification and implementation of safety requirements for safety-critical systems.

Impact Story

Lero has developed the KnowLang formal method tackling the knowledge representation and awareness reasoning for autonomous and adaptive systems. KnowLang was initially developed as part of the research conducted by Lero for the ASCENS project on "Knowledge representation and self-awareness". The EU commission awarded this work the highest possible mark "excellent". The approach has been used to simulate self-adaptation and awareness for the three ASCENS case studies, including the Volkswagen's eMobility platform. 

The overall impact of the new R&D in KnowLang is expected to be in the very challenging field of verification and validation of adaptive systems through simulation. As more applications involve using autonomous and adaptive systems in a critical context, ensuring the correct and safe adaptive behaviour of quality-driven software has become extremely important.

Case Study

KnowLang has been used in multiple proof-of-concept case studies including case studies where autonomy safety requirements for autonomous vehicles are modeled with KnowLang and tested through simulation. The targeted model tackles safety of a self-driving car that engages in interaction with a non-deterministic and open-world environment. In this exercise, we maximize the safety guarantee that “the car would never injure a pedestrian” by modeling and testing all the critical situations involving the car itself in close proximity to pedestrians. With KnowLang, we formalize these situations as system and environment states and formalize self-adaptive behavior driving the car in such situations.

Related Publications

  • Mike Hinchey, Jonathan P. Bowen, and Emil Vassev. Formal Methods. In: P.A. Laplante (ed.), Encyclopaedia of Software Engineering. Taylor & Francis, 2010, pp. 308-320. DOI: 10.1081/E-ESE-120044199.
  • Emil Vassev and Mike Hinchey. Autonomy Requirements Engineering for Space Missions. NASA Monographs in Systems and Software Engineering. Springer, August 2014. ISBN: 978-3-319-09815-9. DOI: 10.1007/978-3-319-09816-6 and the book at Amazon.com
  • Emil Vassev and Mike Hinchey. KnowLang: Knowledge Representation for Self-Adaptive Systems. IEEE Computer, Volume 48 (2), February 2015, pp. 81-84. DOI: 10.1109/MC.2015.50
  • Emil Vassev and Mike Hinchey. Adaptation to the Unforeseen: Can We Trust Autonomous and Adaptive Systems?. In: Proceedings of the 3rd International Conference on Vehicle Technology and Intelligent Transport Systems (VEHITS 2017). April 22-24. Porto, Portugal. To appear.

Expert Contact - Prof. Mike Hinchey

Click here to view Mike's profile and contact information