Context and objectives. The idea of the meeting is to bring together researchers and practitioners working on state-based methods for developing safety-critical systems. Over the last three decades the traditional formal methods community has focused on theories and foundation techniques as well as classical safety-critical systems as case studies in order to demonstrate the value of formal methods.
On the other hand, application of formal methods has been evolving as new types of systems appear such as, e.g., automated driving systems, component-based systems integrating AI-components, machine learning-based systems, and quantum systems. Therefore, it is now essential to discuss emerging challenges and new viewpoints for values of formal methods by investigating tooling experience and advanced case studies crossing the traditional and new areas. Our meeting thus targets the tool aspect and case studies while previous meetings have focused on more theoretical foundation aspects.
The meeting is dedicated to the cross-fertilization of state-based and machine-based formal methods, like Abstract State Machines (ASM), Alloy, B, TLA, VDM, Z, etc. These formal methods share common foundations and are widely used in both academia and industry for the design and analysis of software and hardware systems. Let us note here that the meeting title starting with ”State-based development” emphasizes the fact that for both groups of state-based and machine-based methods,their formal semantics can be given in terms of state-transition systems.
The meeting aims at a vital exchange of knowledge and experience among the research communities around different formal methods. To this end, the organisers intend to build up shared real-life artifacts or case studies, to which state-based formal methods have been successfully applied at special sessions of the well-established international conferences, such as ABZ[1], FASE[2] IFM[3], ICFEM[4], TASE[5], etc. They witness that rigorous case studies, model-based simulations, and scientific reflection on problems and practices in the software industry are of increasing interest to researchers and practitioners. For example, the meeting can benefit from the case studies of the ABZ series (cf. https://abz-conf.org/case-studies/) starting from 2014, such as a mechanical lung ventilator[6], a hemodialysis machine [10], an adaptive exterior light and speed control system [7], a landing gear system [3], the hybrid ERTMS/ETCS Level 3 for international train system [6], a partly-autonomous scheduler of landing sequences of aircraft in airports[7], etc.
The meeting targets to highlight the advances in the state-based development of safety-critical systems, but also to work together on some remaining challenging aspects, among which are, e.g., dynamic reconfiguration [4], run-time enforcement for safety assurance [9], software variability [5], sustainable software development [2], etc.
In addition, this meeting aims to bring together existing and potential users and developers of existing toolsets, such as Rodin platform8, Asmeta toolset9[1], Pro-B tooset10 [8], TLA[11], Alloy[12], etc. Indeed, the meeting is an opportunity to share tool experiences and gain an understanding of ongoing tool developments. Thus the meeting can contribute to fostering a broader community of their users and developers and to coordinate tool development efforts better.

1 https://abz-conf.org/
2 https://etaps.org/2023/conferences/
3 http://www.ifmconference.org/
4 https://icfem2024.info/
5 https://tase2024.github.io/index.html
6 https://github.com/foselab/abz2024_casestudy_MLV
7 https://sites.google.com/view/abz-aman-casestudy/home
8 https://www.event-b.org/
9 https://asmeta.github.io/
10 https://prob.hhu.de/w/index.php?title=Main_Page
11 http://lamport.azurewebsites.net/tla/toolbox.html
12 https://alloytools.org/about.html

Topics. Consequently, discussions and presentations shall address or contribute to the topics below:

Model-based verification, testing and validation, in particular, run-time enforcement, modelbased simulation and model animation. These three particular topics are challenging in statebased modeling. Indeed, the state-based models and additional artifacts (properties, policies, etc.) must be light enough for a run-time systems’ analysis, as well as for their development and validation using simulation and animation exploiting models to handle uncertainties and events in systems’ environment.

Tool improvements for addressing new system characteristics (e.g., distribution, composition, reconfiguration, time and energy constraints, etc.); Dynamic adaptation and reconfiguration are very active research topics aiming to help managing time and energy constraints. On their side, distribution and composition issues are challenging for state-based approaches, e.g., for their soundness while managing interactions for a better coordination. In this context, tool improvement is still expected, namely for dealing with implicit or explicit hypotheses, contracts, theories, etc.

Case studies to share successful experience and limitations met. Witnesses from case study competitions and special sessions of the above-mentioned international conferences show that case studies with lessons learned pave the way for improving the existing methods and also for strengthening research on state-based development. Recently, successful experience with statebased methods and tools for developing cyber-physical systems, or also interactive software systems has served as a base to research methodology discussed during the Shonan meeting NO.205 in November 2023. This is why we do expect challenging research topics coming from case studies and tool development experience.

Beyond the technical results targeted by the proposed Shonan meeting, social, economic, and resilience impacts are expected on the foundations of software development and formal models alignment.

Meeting organisation. Overall, the meeting is thought as a series of discussions around shared reallife case studies, to share the success stories and work on remaining challenging topics. Starting from the list of the identified shared case studies, we plan to collect topics from the participants on the successfully used methods and approaches, but also on the threads to the validity of their experiments, the limitations met and the remaining challenging issues, in order to discuss them in the working groups and to go further together. Moreover, based on the success stories with the case studies and the limitations met, we intend to discuss the research topics such that, e.g., leveraging state-based analysis performance by combining methods and tools, integrating constraints on resources for an incremental development of case-studies, analysing insightful tools performance results and experience in applying state-based development to practical situations and systems, etc. Let us note that we only intend to have limited short talks to share the background, state-of-the-art in relation with the case studies before moving to the discussions.
Finally, once this meeting is completed, we intend to publish a book gathering the main contributions and results, in order to share them with the community.
Position w.r.t. the previous Shonan meetings. The meeting is thought as a next logical phase of meetings focused on formal methods for the rigorous development of safety-critical systems. Indeed,let us mention the four meetings on formal methods and formal approaches to software engineering: "Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems" (NO.090, November 2016), "Towards industrial application of advanced formal methods for cyber-physical system engineering" (NO.121, November 2018), and, more recent "Formal Methods for Trustworthy AI-based Autonomous
Systems" (NO.178, October 2023) and "Formal Method Extensions to Support Domain Theories" (NO.205, November 2023). In addition, there are logical links with the meetings "Science and Practice of Engineering Trustworthy Cyber-Physical Systems (TCPS)" (NO.055, October 2014), and "Modelling and Analysing Resilient Cyber-Physical Systems" (NO.118, December 2018), namely concerning model-based design and engineering principles for cyber-physical systems.
After those meetings, it is a rather normal course of events to analyze their impact on the community via shared non-trivial examples, with the available feedback and lessons learned. Furthermore, as stated before, our Shonan meeting proposal focuses on case studies feedback to address the identified challenges that are still relevant for both academia and industry, whereas all those meetings, except perhaps NO.055 for CPSs, have rather dealt with theoretical aspects of software engineering. Emphasizing the challenges in the case studies and corresponding automated tools’ aspects naturally makes a difference from the previous meetings, and helps gather research strength and build capacity.

[1] P. Arcaini, A. Bombarda, S. Bonfanti, A. Gargantini, E. Riccobene, and P. Scandurra. The ASMETA approach to safety assurance of software systems. In A. Raschke, E. Riccobene, and K.-D. Schewe, editors, Logic, Computation and Rigorous Methods - Essays Dedicated to Egon Börger on the Occasion of His 75th Birthday, volume 12750 of Lecture Notes in Computer Science, pages 215–238. Springer, 2021.
[2] S. Biffl, E. Navarro, R. Mirandola, and D. Weyns. Architecting for a sustainable digital society. J. Syst. Softw., 200:111668, 2023.
[3] F. Boniol and V. Wiels. The landing gear system case study. In F. Boniol, V.Wiels, Y. Ait Ameur, and K.-D. Schewe, editors, ABZ 2014: The Landing Gear Case Study, pages 1–18, Cham, 2014. Springer International Publishing.
[4] R. de Lemos et. al. Software engineering for self-adaptive systems: Research challenges in the provision of assurances. In R. de Lemos, D. Garlan, C. Ghezzi, and H. Giese, editors, Software Engineering for Self-Adaptive Systems III. Assurances - International Seminar, Dagstuhl Castle, Germany, December 15-19, 2013, Revised Selected and Invited Papers, volume 9640 of Lecture Notes in Computer Science, pages 3–30. Springer, 2013.
[5] M. Galster, D. Weyns, M. Goedicke, U. Zdun, J. Cunha, and J. Chavarriaga. Variability and complexity in software design: Towards quality through modeling and testing. ACM SIGSOFT Softw. Eng. Notes, 42(4):35–37, 2017.
[6] T. S. Hoang, M. Butler, and K. Reichl. The hybrid ERTMS/ETCS level 3 case study. In M. Butler, A. Raschke, T. S. Hoang, and K. Reichl, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z, pages 251–261, Cham, 2018. Springer International Publishing.
[7] F. Houdek and A. Raschke. Adaptive exterior light and speed control system. In A. Raschke, D. Méry, and F. Houdek, editors, Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings, volume 12071 of Lecture Notes in Computer Science, pages 281–301. Springer, 2020.
[8] M. Leuschel. Prob: Harnessing the power of prolog to bring formal models and mathematics to life. In Prolog: The Next 50 Years, volume 13900 of Lecture Notes in Computer Science, pages 239–247. Springer, 2023.
[9] N. Leveson. Are you sure your software will not kill anyone? Commun. ACM, 63(2):25–28, jan 2020.
[10] A. Mashkoor. The hemodialysis machine case study. In M. Butler, K.-D. Schewe, A. Mashkoor, and M. Biro, editors, Abstract State Machines,