The 25^th International Conference on Formal Engineering Methods

Mike Hinchey is Professor of Software Engineering at University of Limerick, Ireland, where he was previously Head of Department of Computer Science and Information Systems and Director of Lero-the Science Foundation Ireland Research Centre for Software, a national research centre headquartered at University of Limerick. He is Past President of IFIP, the International Federation for Information Processing (www.ifip.org) and Past Chair of the IEEE UK & Ireland Section. He is Director-elect of IEEE Region 8 (Europe, Middle East, Africa) and serves on IEEE Computer Society Board of Governors. Prior to joining University of Limerick, Professor Hinchey was the Director of the NASA Software Engineering Laboratory. In 2009, he was awarded NASA’s Kerley Award as Innovator of the Year and is one of only 36 people recognized in the NASA Inventors Hall of Fame. Professor Hinchey holds a B.Sc. in Computer Systems from University of Limerick, an M.Sc. in Computation (Mathematics) from University of Oxford and a PhD in Computer Science from University of Cambridge. Professor Hinchey is a Chartered Engineer, Chartered Engineering Professional, Chartered Mathematician and Chartered Information Technology Professional, as well as a Fellow of the IET, British Computer Society, Engineers Ireland, and Irish Computer Society, of which he is also Past President. He is Editor-in-Chief of Innovations in Systems and Software Engineering: a NASA Journal and Journal of the Brazilian Computer Society. In 2018, he became an Honorary Fellow of the Computer Society of India and was the SEARCC Global ICT Professional of the Year 2018.

Title: Formal Specification of Autonomy Features with ARE and KnowLang

Abstract:

Autonomous systems, such as autonomous vehicles, extend upstream the regular software-intensive systems with special autonomy features. The identification of such features is not necessarily an easy task. Sometimes, those can be explicitly stated by stakeholders or in preliminary material available to requirements engineers. Often though, they are implicit, so a process of formal specification intended to capture the autonomy features has to be undertaken. This paper elaborates on a methodology for capturing and specification of autonomy features where autonomy requirements are captured with ARE (Autonomy Requirements Engineering) and then are specified with KnowLang. a framework for knowledge representation and reasoning. In this approach, autonomy features are detected as special self-* objectives backed up by different capabilities and quality characteristics. The self-* objectives provide the system’s ability to autonomously discover, diagnose, and cope with various problems. The captured autonomy requirements are formally specified with the KnowLang notation and then compiled to a knowledge base that is to be used by the KnowLang Reasoner.

Naijun Zhan is a distinguished research professor of Institute of Software Chinese Academy of Sciences (ISCAS). He got his bachelor degree and master degree both from Nanjing University, and his PhD from ISCAS. Prior to join ISCAS, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, modal and temporal logic, and so on. He is in the editorial boards of Journal of Automated Reasoning, Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Electronics, and Journal of Computer Research and Development, a member of the steering committees of SETTA and MEMOCODE, the pc co-chairs of FM 2021, SETTA 2016, the general co-chairs of MEMOCODE 2018, MEMOCODE2019 and ICESS 2019, and serves more than 100 international conferences program committees e.g., CAV, FM, TACAS, RTSS, HSCC, ICCPS, EMSOFT and so on. He published more than 100 papers in international leading journals and conferences, 2 books and 4 book chapters, and edited 4 conference proceedings and 4 journal special issues.

Title: Synthesizing (Differential) Invariants by Reduction Non-Convex Programming to SDP

Abstract:

Invariant Generation plays a central role in the verification of programs and hybrid systems. As the constraint solving techniques advance rapidly in recent years, particularly optimization-based constraint solving, optimization based invariant generation becomes more and more promising and has been successfully applied to verification of programs and hybrid systems. However, how to deal with non-convex programming derived from invariant generation is still challenging. In this talk, I report our recent work on efficient invariant generation by reduction non-convex programming to SDP.

Mark Lawford is Chair and Professor of the Department of Computing and Software at McMaster University (Canada). He is a Co-Founder and a past Director of McMaster Centre for Software Certification (McSCert), the 2024 IEEE TCSE Synergy award recipient. He joined McMaster University in 1998, where he helped to develop the software engineering and mechatronics engineering programs. Throughout his career he has work with industry on the practical application of formal methods and model based software engineering to safety critical real-time software. After working with industry partners in the nuclear and medical domains earlier in his career, over the past decade he has increasingly focused on working with OEMs on assurance of automotive systems.

Title: Challenges and Opportunities in Assurance of Software Defined Vehicle

Abstract:

Automotive innovation is increasingly software driven. As a result of the competitive environment requiring a yearly release of new automotive models featuring the latest driver assistance features and innovation in electrification, safety critical software is being developed at an unprecedented scale on extremely tight deadlines. To be competitive automotive manufacturers and parts suppliers need to change how they develop and assure software intensive systems. This presents a tremendous opportunity for researchers in the application of formal methods and model based software engineering to have a significant impact on industry practice. In this talk we highlight our recent work on model based software engineering, incremental assurance and the potential for applications of formal methods to help the automotive industry make the transition to the Software Defined vehicle.