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 in 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.
翻译:该卷载有在2022年9月26日和27日举办的第四届自动化和可核查的软件系统全新发展系统正式方法国际讲习班(FMAS 2022)和在2022年9月26日和27日举办的第四届自动和可核查的软件系统开发系统国际讲习班(ASYDE 2022)的联合程序。FMAS 2022和ASYDE 2022是结合第二十届软件工程和正式方法国际会议(SEFMF'22)在柏林洪堡特大学举行的。关于FMAS,今年的讲习班是经过两版FMAS全线在线限制的两版之后,我们又恢复了面对面的出席。我们还热切希望确保2022年自动和可核查的软件系统能够为无法旅行的人提供方便的无障碍访问。因此,该讲习班为远程介绍和出席提供了便利。FSYDE2022的目的是将正在使用正式方法应对自主系统带来的独特挑战的研究人员聚集在一起,分享最近和正在进行的工作。自主系统对于正式方法的应用是十分复杂和独特的挑战。自主系统在没有人类干预的情况下运作,而且经常被嵌入一个自动的机能系统,在这种机能系统中,我们可以进行真正的核查。