Preface

This EPTCS volume contains the joint proceedings for the fourth international workshop on Formal Methods for Autonomous Systems (FMAS 2022) and the fourth international workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE 2022), which were held on the 26th and 27th of September 2022. FMAS 2022 and ASYDE 2022 were held in conjunction with 20th International Conference on Software Engineering and Formal Methods (SEFM'22), at Humboldt University Berlin.

For FMAS, this year's workshop was our return to having in-person attendance after two editions of FMAS that were entirely online because of the restrictions necessitated by COVID-19. We were also keen to ensure that FMAS 2022 remained easily accessible to people who were unable to travel, so the workshop facilitated remote presentation and attendance.

The goal of FMAS is to bring together leading researchers who are using formal methods to tackle the unique challenges presented by autonomous systems, to share their recent and ongoing work. Autonomous systems are highly complex and present unique challenges for the application of formal methods. Autonomous systems act without human intervention, and are often embedded in a robotic system, so that they can interact with the real world. As such, they exhibit the properties of safety-critical, cyber-physical, hybrid, and real-time systems. We are interested in work that uses formal methods to specify, model, or verify autonomous and/or robotic systems; in whole or in part. We are also interested in successful industrial applications and potential directions for this emerging application of formal methods.

As in previous years, FMAS 2022 encouraged the submission of both long and short papers. However, this year we asked for specific categories of submissions: vision papers and research previews, both of which were types of short paper; and experience reports and regular papers, both of which were types of long paper. We received 12 regular papers, 0 experience reports, 6 research previews, and 2 vision papers; 20 papers in total, 12 long and 8 short. The researchers who submitted papers to FMAS 2022 were from institutions in: Austria, Belgium, Brazil, France, Germany, Italy, the Netherlands, Spain, Sweden, the United Kingdom, and the United States of America. We were very pleased with the number of submissions for FMAS 2022, we had two more submissions than last year's fantastic result. It's very encouraging to see a steady number of submissions as FMAS establishes itself as a regular, annual workshop. Each paper received three reviews, and we accepted 14 papers in total: 9 long papers and 5 short papers (all research previews).

FMAS 2022 hosted two invited speakers. Taylor T. Johnson, from Vanderbilt University (USA), gave a talk entitled "Formal Verification for Neural Networks in Autonomous Cyber-Physical Systems"; and Marija Slavkovik, from University of Bergen, gave a talk entitled "Common Ground in Moral Norms". After each talk there was a discussion session, with questions provided by each invited speaker, to structure the discussion. These discussions aim to shape the future research in the area of formal methods for autonomous systems.

We would like to thank our brilliant programme committee and sub-reviewers for their helpful reviews and discussions behind the scenes. As ever, we are proud to have a set of reviewers who are so enthusiastic about FMAS and the work submitted to it. We thank them for their time and effort; without them, we could not assemble such an impressive programme of papers. We also thank our invited speakers, Marija Slavkovik, and Taylor T. Johnson; the authors who submitted papers; our EPTCS editor, Martin Wirsing; FME for its sponsorship; and all of the attendees (both virtual and in-person) this year.

Matt Luckcuck and Marie Farrell
Department of Computer Science and the Hamilton Institute,
Maynooth University, Ireland

Program Committee

• Christopher Bischopink, Carl von Ossietzky University of Oldenburg (Germany)
• Rafael C. Cardoso, University of Manchester (UK)
• Louise A. Dennis, University of Manchester (UK)
• Fatma Faruq, University of Manchester (UK)
• Angelo Ferrando, University of Genova (Italy)
• Michael Fisher, University of Manchester (UK)
• Mario Gleirscher, University of Bremen (Germany)
• Mallory S. Graydon, NASA Langley Research Center (USA)
• Jérémie Guiochet, University of Toulouse (France)
• Taylor T. Johnson, Vanderbilt University (USA)
• Raluca Lefticaru, University of Bradford (UK)
• Sven Linker, Lancaster University Leipzig (Germany)
• Lina Marsso, University of Toronto (Canda)
• Anastasia Mavridou, KBR Wyle/NASA Ames Research Center (USA)
• Claudio Menghi, McMaster University (Canada)
• Dominique Méry, Université de Lorraine, LORIA (France)
• Alice Miller, University of Glasgow (UK)
• Alvaro Miyazawa, University of York (UK)
• Rosemary Monahan, Maynooth University (Ireland)
• Natasha Neogi, NASA Langley Research Center (USA)
• Colin Paterson, University of York (UK)
• Ivan Perez, KBR Wyle/NASA Ames Research Center (USA)
• Maike Schwammberger, Carl von Ossietzky University of Oldenburg (Germany)
• Silvia Lizeth Tapia Tarifa, University of Oslo (Norway)
• Hao Wu, Maynooth University (Ireland)
• Mengwei Xu, University of Glasgow (UK)

Subreviewers

• Zheng Cheng, Université de Lorraine (France)
• Astrid Rakow, Carl von Ossietzky University of Oldenburg (Germany)
• Oisín Sheridan, Maynooth University (Ireland)
• Xingyu Zhao, University of Liverpool (UK)

ASYDE 2022 Organizers' Message

ASYDE 2022 provided a forum for researchers and practitioners to propose and discuss on automated software development methods and techniques, compositional verification theories, integration architectures, flexible and dynamic composition, and automated planning mechanisms.

During the last three decades, automation in software development has gone mainstream. Software development teams strive to automate as much of the software development activities as possible. Automation helps, in fact, to reduce development time and cost, as well as to concentrate knowledge by bringing quality into every step of the development process.

Realizing high-quality software systems requires producing software that is efficient, error-free, cost-effective, and that satisfies customer requirements. Thus, one of the most crucial factors impacting software quality concerns not only the automation of the development process but also the ability to verify the outcomes of each process activity and the goodness of the resulting software product as well. Realizing high-quality software systems requires producing software that is efficient, error-free, cost-effective, and that satisfies evolving requirements.

Unfortunately, for this edition, ASYDE has only 1 paper accepted. The paper was peer-reviewed by three program committee members.

We would like to thank the ASYDE Steering Committee for the support provided during the ASYDE 2022 organization. A special thanks goes to the SEFM 2022 Organizers who have been supportive and, in particular, to Dr. Paolo Masci (National Institute of Aerospace, USA), who has always been willing to consider or accept new suggestions and ideas, reacting quickly and positively to the ASYDE 2022 requests. We also want to thank the Chairs of the Fourth Workshop on Formal Methods for Autonomous Systems (FMAS), Dr Matt Luckcuck and Dr Marie Farrell (Maynooth University, Ireland), for including the ASYDE paper in FMAS proceedings.

September 2022

Organization

Program Committee Chairs

• Marco Autili - University of L'Aquila, Italy
• Luca Berardinelli - WIN-SE department, JKU Linz, Austria
• Alessio Bucaioni - Mälardalen University, Västerås, Sweden
• Claudio Pompilio - University of L'Aquila, Italy

Steering Committee

• Farhad Arbab - Centre for Math and CS, The Netherlands
• Marco Autili - University of L'Aquila, Italy
• Federico Ciccozzi - Mälardalen University, Sweden
• Dimitra Giannakopoulou - NASA, USA
• Pascal Poizat - Paris Nanterre University, France
• Massimo Tivoli - University of L'Aquila, Italy

Program Committee

• Luciano Baresi - Polytechnic University of Milan, Italy
• Steffen Becker - University of Stuttgart, Germany
• Antonio Brogi - University of Pisa, Italy
• Giovanni Denaro - University of Milano-Bicocca, Italy
• Antinisca Di Marco - University of L'Aquila, Italy
• Daniele Di Pompeo - University of L'Aquila, Italy
• Amleto Di Salle - University of L'Aquila, Italy
• Predrag Filipovikj - Scania Group, Sweden
• Francesco Flammini - Linnaeus University, Sweden
• Abel Gómez - Universitat Oberta de Catalunya, Spain
• Ludovico Iovino - Gran Sasso Science Institute, Italy
• Ehsan Khamespanah - University of Tehran, Iran
• Elena Lisova - Mälardalen University, Sweden
• Raffaela Mirandola - Polytechnic University of Milan, Italy
• Luca Pulina - University of Sassari, Italy
• Bilal Said - Softeam, France
• Cristina Seceleanu - Mälardalen University, Sweden
• Marjan Sirjani - Mälardalen University, Sweden
• Catia Trubiani - Gran Sasso Science Institute, Italy
• Manuel Wimmer - JKU Linz, Austria
• Apostolos Zarras - University of Ioannina, Greece

Formal Verification for Neural Networks in Autonomous Cyber-Physical Systems

The ongoing renaissance in artificial intelligence (AI) has led to the advent of data-driven machine learning (ML) methods deployed within components for sensing, actuation, and control in safety-critical cyber-physical systems (CPS). While such learning-enabled components (LECs) are enabling autonomy in systems like autonomous vehicles, robots, and other autonomous CPS, as demonstrated in part through recent accidents in semi-autonomous/autonomous CPS and by adversarial ML attacks, ensuring such components operate reliably in all scenarios is extraordinarily challenging. We will discuss formal methods for assuring specifications---mostly robustness and safety---in autonomous CPS using our software tools NNV (Neural Network Verification [1]) and Veritex [2], developed as part of an ongoing DARPA Assured Autonomy project. These tools have been evaluated in CPS development with multiple industry partners in automotive, aerospace, and robotics domains, and allow for analyzing neural networks and their usage in closed-loop systems. We will briefly discuss relevant ongoing community activities we help organize, such as the Verification of Neural Networks Competition (VNN-COMP) held with the International Conference on Computer-Aided Verification (CAV) the past few years, as well as the AI and Neural Network Control Systems (AINNCS) category of the hybrid systems verification competition (ARCH-COMP). We will conclude with a discussion of future directions in the broader safe and trustworthy AI domain, such as in new projects verifying neural networks used in medical imaging analysis.

References

1. https://github.com/verivital/nnv
2. https://github.com/verivital/veritex
3. Stanley Bak, Changliu Liu & Taylor T. Johnson (2021): The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR abs/2109.00498. arXiv:2109.00498.
4. Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs & Taylor T. Johnson (2020): Improved Geometric Path Enumeration for Verifying ReLU Neural Networks. In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification, Springer International Publishing, Cham, pp. 66-96, doi:10.1007/978-3-030-53288-8_4.
5. Taylor T. Johnson, Stanley Bak, Marco Caccamo & Lui Sha (2016): Real-Time Reachability for Verified Simplex Design. ACM Trans. Embed. Comput. Syst. 15(2), doi:10.1145/2723871.
6. Taylor T. Johnson, Diego Manzanas Lopez, Luis Benet, Marcelo Forets, Sebastian Guadalupe, Christian Schilling, Radoslav Ivanov, Taylor J. Carpenter, James Weimer & Insup Lee (2021): ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. In Goran Frehse & Matthias Althoff, editors: 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), EPiC Series in Computing 80, EasyChair, pp.90-119, doi:10.29007/kfk9.
7. Taylor T Johnson, Diego Manzanas Lopez, Patrick Musau, Hoang-Dung Tran, Elena Botoeva, Francesco Leofante, Amir Maleki, Chelsea Sidrane, Jiameng Fan & Chao Huang (2020): ARCH-COMP20 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. In Goran Frehse & Matthias Althoff, editors: ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), EPiC Series in Computing 74, EasyChair, pp. 107-139, doi:10.29007/9xgv.
8. Diego Manzanas Lopez, Patrick Musau, Hoang-Dung Tran, Souradeep Dutta, Taylor J. Carpenter, Radoslav Ivanov & Taylor T. Johnson (2019): ARCH-COMP19 Category Report: Artificial Intelligence and Neural Network Control Systems (AINNCS) for Continuous and Hybrid Systems Plants. In Goran Frehse & Matthias Althoff, editors: ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing 61, EasyChair, pp. 103-119, doi:10.29007/rgv8.
9. Diego Manzanas Lopez, Patrick Musau, Nathaniel P. Hamilton & Taylor T. Johnson (2022): Reachability Analysis of a General Class of Neural Ordinary Differential Equations. In Sergiy Bogomolov & David Parker, editors: Formal Modeling and Analysis of Timed Systems, Springer International Publishing, Cham, pp. 258-277, doi:10.1007/978-3-031-15839-1_15.
10. Patrick Musau, Nathaniel Hamilton, Diego Manzanas Lopez, Preston Robinette & Taylor T. Johnson (2022): On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers. In: 2022 IEEE International Conference on Assured Autonomy (ICAA), pp. 1-10, doi:10.1109/ICAA52185.2022.00010.
11. Neelanjana Pal & Taylor T Johnson (2022): Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool. In Anne Remke & Dung Hoang Tran, editors: Proceedings The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT, Online, 23rd August 2021, Electronic Proceedings in Theoretical Computer Science 361, Open Publishing Association, pp. 79-88, doi:10.4204/EPTCS.361.8.
12. Hoang-Dung Tran, Stanley Bak, Weiming Xiang & Taylor T. Johnson (2020): Verification of Deep Convolutional Neural Networks Using ImageStars. In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification, Springer International Publishing, Cham, pp. 18-42, doi:10.1007/978-3-030-53288-8_2.
13. Hoang-Dung Tran, Feiyang Cai, Manzanas Lopez Diego, Patrick Musau, Taylor T. Johnson & Xenofon Koutsoukos (2019): Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control. ACM Trans. Embed. Comput. Syst. (TECS, Special Issue from EMSOFT'19) 18(5s), doi:10.1145/3358230.
14. Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang & Taylor T. Johnson (2019): Star-Based Reachability Analysis of Deep Neural Networks. In Maurice H. ter Beek, Annabelle McIver & Jos\'e N. Oliveira, editors: Formal Methods - The Next 30 Years, Springer International Publishing, Cham, pp. 670-686, doi:10.1007/978-3-030-30942-8_39.
15. Hoang-Dung Tran, Patrick Musau, Diego Manzanas Lopez, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang & Taylor T. Johnson (2019): Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks. In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE '19, IEEE Press, p. 31-40, doi:10.1109/FormaliSE.2019.00012.
16. Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang & Taylor T. Johnson (2019): Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems. In Jorge A. P\'erez & Nobuko Yoshida, editors: Formal Techniques for Distributed Objects, Components, and Systems, Springer International Publishing, Cham, pp. 261-277, doi:10.1007/978-3-030-21759-4_15.
17. Hoang-Dung Tran, Neelanjana Pal, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Stanley Bak & Taylor T Johnson (2021): Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter. Formal Aspects of Computing 33(4), pp. 519-545, doi:10.1007/s00165-021-00553-4.
18. Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Stanley Bak & Taylor T. Johnson (2021): Robustness Verification of Semantic Segmentation Neural Networks Using Relaxed Reachability. In Alexandra Silva & K. Rustan M. Leino, editors: Computer Aided Verification, Springer International Publishing, Cham, pp. 263-286, doi:10.1007/978-3-030-81685-8_12.
19. Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak & Taylor T. Johnson (2020): NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification, Springer International Publishing, Cham, pp. 3-17, doi:10.1007/9783-030-53288-8_1.
20. Weiming Xiang, Hoang-Dung Tran & Taylor T. Johnson (2018): Output Reachable Set Estimation and Verification for Multilayer Neural Networks. IEEE Transactions on Neural Networks and Learning Systems 29(11), pp. 5777-5783, doi:10.1109/TNNLS.2018.2808470.
21. Weiming Xiang, Hoang-Dung Tran, Xiaodong Yang & Taylor T. Johnson (2021): Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach. IEEE Transactions on Neural Networks and Learning Systems 32(5), pp. 1821-1830, doi:10.1109/TNNLS.2020.2991090.
22. Xiaodong Yang, Taylor T Johnson, Hoang-Dung Tran, Tomoya Yamaguchi, Bardh Hoxha & Danil Prokhorov (2021): Reachability Analysis of Deep ReLU Neural Networks Using Facet-Vertex Incidence. In: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, HSCC '21, Association for Computing Machinery, New York, NY, USA, pp. 1-7, doi:10.1145/3447928.3456650.
23. Xiaodong Yang, Tom Yamaguchi, Hoang-Dung Tran, Bardh Hoxha, Taylor T. Johnson & Danil Prokhorov (2022): Neural Network Repair with Reachability Analysis. In Sergiy Bogomolov & David Parker, editors: Formal Modeling and Analysis of Timed Systems, Springer International Publishing, Cham, pp. 221-236, doi:10.1007/978-3-031-15839-1_13.

Common Ground in Moral Norms

Any ethically behaving autonomous system needs a specification of what the right and wrong thing to do is. Who decides what right and wrong is for a machine? In the absence of a moral theory that can be neatly translated into an algorithm (and machines that have high level of situational awareness), the specification of what is right and wrong is likely to come as a rule-of-thumb: dynamic, context specific and sourced from various stakeholders. These moral norms are likely to be conflicting. We explore: What is a common ground in a set of conflicting norms? How do we approach moral norm conflicts and build algorithms that resolve them?