Published: 16th November 2021
DOI: 10.4204/EPTCS.349
ISSN: 2075-2180

EPTCS 349

Proceedings First Workshop on
Applicable Formal Methods
virtual, 23rd November 2021

Edited by: Mario Gleirscher, Jaco van de Pol and Jim Woodcock

Preface
Mario Gleirscher, Jaco van de Pol and Jim Woodcock
Invited Presentation: The Future of Modelling Languages in Industry – Why Practitioners Do Not Use Your Favourite Process Algebra
Jan Peleska
Invited Presentation: Adding Proof to the Continuous Integration Workflow
Yannick Moy
Is CADP an Applicable Formal Method?
Hubert Garavel, Frédéric Lang, Radu Mateescu and Wendelin Serwe
1
Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA
Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini and Elvinia Riccobene
13
A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems
Lorenzo Capra
31
F-IDEs with Features and VCs Designed to Assist Human Reasoning When Verification Fails
Yu-Shan Sun, Daniel Welch and Murali Sitaraman
51
Experience Report: Teaching Code Analysis and Verification Using Frama-C
Salwa Souaf and Frédéric Loulergue
69
Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda
Carolina Carreira, João F. Ferreira, Alexandra Mendes and Nicolas Christin
77

Preface

This volume of EPTCS contains the proceedings of the 1st International Workshop on Applicable Formal Methods (AppFM 2021), 23 November 2021, held online as part of the 24th International Symposium on Formal Methods (FM), organised by the Institute of Software of the Chinese Academy of Sciences in Beijing, China.

Formal methods are mathematically founded recipes, step-wise procedures, supporting engineers in critical tasks in the design of industrial systems and software engineering. The AppFM workshop aims at strengthening the community of researchers who improve and evaluate existing formal approaches and variants in practical contexts and support the transfer of these approaches to engineering practice.

All submissions were expected to contribute to the workshop objective by addressing several questions about the applicability of the formal approach(es) under examination, including questions about automation, integration, methodology, scalability, transfer, usefulness, ease of use, as well as the research method chosen for evaluating the workshop contribution itself.

There were two submission categories: Regular papers (up to 15 pages) focusing on method applications (e.g. case studies, conducted experiments) or comparative studies (e.g. detailed comparison of two methods by example); and short papers (up to 6 pages) focusing on research summaries, focused literature surveys, systematic maps, experience reports or success stories, opinions or positions, agendas or visions, or proposals of research designs (e.g. controlled method experiments in the field).

The first AppFM workshop program consisted of presentations of contributed papers, invited talks, and hosted an interactive discussion session. A highlight of the discussion session was the Manifesto for Applicable Formal Methods treated as a means to put forward principles underlying applicable formal methods and potential next steps to be made by the formal methods community.

The workshop program included two invited talks:

In the workshop program, the following submitted full-paper contributions were presented (listed in no specific order):

Furthermore, the following submitted short-paper contributions were presented (listed in no specific order):

This volume consists of the six selected papers: three regular papers and three short papers. The final contributions were selected from ten submitted papers. Each submission was thoroughly and constructively refereed by three members of the program committee (PC). The program chairs thank all the PC members and the additional reviewer for their invaluable service as well as the FM symposium organisers for their services as a host.

The members of the PC were Bernhard Aichernig, Maurice ter Beek, Jean-Louis Boulanger, Jonathan Bowen, John Fitzgerald, Hubert Garavel, Carlo Ghezzi, Stefania Gnesi, Anne Haxthausen, Connie Heitmeyer, Michael Hinchey, Michael Holloway, Gerwin Klein, Peter Gorm Larsen, Thierry Lecomte, Stefan Leue, Zhiming Liu, Colin O'Halloran, Jose Oliveira, Frank Ortmeier, Jan Peleska, Augusto Sampaio, Kenji Taguchi, and Willem Visser. Additional reviewer was Simon Thrane Hansen.

The PC chairs and volume editors,

Mario Gleirscher (University of Bremen, Germany)

Jaco van de Pol (Aarhus University, Denmark)

Jim Woodcock (University of York, United Kingdom)

References

Bombarda, Andrea, Silvia Bonfanti, Angelo Gargantini, and Elvinia Riccobene. 2021. "Developing a Prototype of a Mechanical Ventilator Controller from Requirements to Code with ASMETA." In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.

Capra, Lorenzo. 2021. "A Maude Implementation of Rewritable Petri Nets: A Feasible Model for Dynamically Reconfigurable Systems." In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.

Carreira, Carolina, Joao F. Ferreira, Alexandra Mendes, and Nicolas Christin. 2021. "Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda." In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.

Garavel, Hubert, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. 2021. "Is CADP an Applicable Formal Method?" In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.

Souaf, Salwa, and Frederic Loulergue. 2021. "Experience Report: Teaching Code Analysis and Verification Using Frama-C." In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.

Sun, Yu-Shan, Daniel Welch, and Murali Sitaraman. 2021. "F-IDEs with Features and VCs Designed to Assist Human Reasoning When Verification Fails." In Applicable Formal Methods (AppFM), 1st FM Workshop. EPTCS.


The Future of Modelling Languages in Industry – Why Practitioners Do Not Use Your Favourite Process Algebra

Jan Peleska (University of Bremen)

This presentation is meant to be provocative, and it may be the case that some statements are exaggerated. It is based, however, on 30 years of experience with the application of modelling languages in industry. Sometimes exaggeration is helpful to create insights. We review the formalisms actually used in industry and give reasons why your favourite fully formal modelling language is not among those practitioners use. Then it is described why industrial users are not really as happy with the formalisms they currently apply - at least not as happy as the commercial tool providers would like to make you believe. This leads to an interesting conclusion: it is time to invent a new modelling formalism with its associated methodology and supporting tool chain. We discuss the key elements of success and point out a current undertaking which is very promising.


Adding Proof to the Continuous Integration Workflow

Yannick Moy (AdaCore)

SPARK is a technology for mathematically proving that programs are correct, that has been adopted in various critical domains: defense, space, air traffic control, avionics, railway, automotive, networks, medical devices. Our focus is the development of tools usable by software engineers and applicable to industrial software. The "tools" here include a programming language, development and verification tools, and processes around these. As engineering practice in industry moves towards Continuous Integration supported by DevSecOps practices, program proof needs to adapt. In this talk, I will adopt the points of view of developers, certification and management, and show how SPARK fulfills (or not) their needs in a Continuous Integration Workflow.