Archive for March 2025

New article: obituary of Niklaus Wirth

Bertrand Meyer: Obituary for Niklaus Wirth, in Formal Aspects of Computing, volume 37, issue 2, pages 1-11, published 3 March 2025, available here (publisher’s site).

Shortly after Niklaus Wirth — Turing Award winner for his many seminal contributions including Pascal, Algol W, Modula, virtual machines, Lilith/Ceres, railway diagrams, PL/360, seminal textbooks…  — passed away last year, I wrote a long blog article about him. Jim Woodcock, editor of Formal Aspects of Computing, asked me to adapt it for the journal. The result has just been published.

It is not a traditional eulogy; rather, a free-ranging discussion of Wirth’s achievements and my personal analysis of his ideas. Wirth’s career is well-documented elsewhere; my article does not replace encyclopedia entries (or the many talks by Wirth and interviews of him available for example on YouTube), but is more like one side (sadly) of a dialog on programming, languages, methods, tools and the evolution of our common discipline.

Its appearance in Formal Aspects of Computing is apposite: even though Wirth would probably not have characterized himself as a formal methods person, he did work with Tony Hoare on axiomatic language specifications, and all his work shows  the same kind of precision and rigor that characterizes formal methods work. I hope my account of his contributions will help make them better known and perpetuate his memory.

Reminder: my full annotated publication list is here.

VN:F [1.9.10_1130]
Rating: 0.0/10 (0 votes cast)
VN:F [1.9.10_1130]
Rating: 0 (from 0 votes)

New preprint: Lessons from Formally Deployed Software Systems

Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer and Yinling Liu, Lessons from Formally Verified Deployed Software Systems, submitted for publication (since March 2023), preprint available here for the full version (with detailed review of all 32 projects) and here for a shorter one (with same core content but only 11 detailed reviews, the others summarized in a table).

Formal methods of software construction, using mathematical techniques to ensure their correctness and (whenever possible) to prove it using automatic tools, now have a long history but they remain controversial. Questions linger, in particular, on their applicability in an industrial setting. This is the kind of question with opinions galore but limited published evidence. This article is a detailed survey of 32 formally-verified industrial systems, intended to provide firm data on the state of application of formal methods to industry —successes, challenges, limitations, lessons.

The paper resulted from an attempt to identify as many  such formally-verified systems actually deployed in industry as possible. Some of the projects were selected thanks to a questionnaire that we sent out to many forums; others were found through a variety of sources. Out of many initially identified projects the articles covers 32; other than interest and relevance, the criteria for selection included our ability to find detailed information about them and verify that information. Whenever possible we used published accounts, but for some of the most interesting systems deployed in industry little is available in the literature; we only retained those for which we could get and validate information from the projects themselves, over the course of many interactions.

The article is focused on facts and figures, not opinions. Although the authors are actively engaged in using formal methods, we have no axe to grind, if only because we know, from that very practice, what the challenges are. The article is neither for formal methods nor against formal methods; it helps readers form their own opinions by providing a wealth of carefully verified information about projects that have applied formal verification in an industrial setting. I can safely assert that there is no comparable body of work available anywhere; while there have been excellent surveys of formal methods and software verification before (the article has a dedicated section in which it reviews many of them), none has gone into the present study’s level of detailed study and analysis of actual projects, much of which not available anywhere else (particularly in the case of information gleaned from interacting with the project members themselves but not previously published).

I believe therefore that this study deserves to be known by anyone interested in software verification and formal methods. There are two versions: the long version contains the description of all selected 32 projects. The short one, cut to the page limit of the intended journal (see next) has these details for only 11 systems, chosen to be representative (typically, one example for each general category, e.g. compilers); the properties of the others are summarized in a table. The introduction, overview, general analysis, discussion and conclusions are the same, so if you just want to get an overall idea you can start with the short version.

Presenting the article as a “new preprint” is somewhat of a twist since its first version was available in March of 2023 and the current version is from last October. The paper has been under review for ACM Computing Surveys for over two years; this is not the right place to complain about the process, but let me politely say that we are a bit frustrated since on our side we did all that was requested. (I am thankful to Moshe Vardi who, alone of all people whom I solicited for help, managed to get something moving at some point.) Given the way things have been going and even though the authors did everything requested of them I would not bet that it will eventually be published; if nothing else, the more time passes the more self-fulfilling becomes the criticism of obsolescence. The study took a full year (2022), and the initial version was submitted in March 2023. All information on the selected projects was carefully checked and updated a year later (February 2024), but no new projects were added then. So the article is not meant to be the last word for eternity; rather, it presents of snapshot of the state of the art at one particular moment. In this role — and whether it ends up published or forever remains Samizdat — I hope it will be useful.

 

Reminder: my full annotated publication list is here.

VN:F [1.9.10_1130]
Rating: 0.0/10 (0 votes cast)
VN:F [1.9.10_1130]
Rating: 0 (from 0 votes)

New preprint: Seamless and Traceable Requirements

Maria Naumcheva, Sophie Ebersold, Jean-Michel Bruel and Bertrand Meyer, UOOR: Seamless and Traceable Requirements, submitted for publication, February 2025, preprint available on arXiv.

This article grew out of Maria Naumcheva’s PhD thesis defended on December 18 at the University of Toulouse (I will write separately about the thesis as a whole). It is part of a general effort at systematic requirements engineering, reflected in earlier articles by the some or all of the same group of authors (see my publication list) and in my requirements book. Here is a short version of the abstract for the article:

In industrial practice, requirements are an indispensable element of any serious software project. In the academic study of software engineering, requirements are one of the heavily researched subjects. And yet requirements engineering, as practiced in industry, makes shockingly sparse use of the concepts propounded in the requirements literature.

The present paper starts from an assumption about the causes for this situation and proposes a remedy to redress it. The posited explanation is that change is the major factor affecting the practical application of even the best-intentioned requirements techniques. No sooner has the ink dried on the specifications than the system environment and stakeholders’ views of the system begin to evolve.

The proposed solution is a requirements engineering method, called UOOR, which unifies many known requirements concepts and a few new ones in a framework entirely devised to accommodate and support seamless change throughout the project lifecycle. The method encompasses the commonly used requirements techniques such as scenarios, and integrates them into the seamless software development process. The work presented here introduces the notion of seamless requirements traceability, which relies on the propagation of traceability links, themselves based on formal properties of relations between project artifacts.

As a proof of concept, the paper presents a traceability tool to be integrated into a general-purpose IDE that provides the ability to link requirements to other software project artifacts, display notifications of changes in requirements, and trace those changes to the related project elements.

The UOOR approach is not just a theoretical proposal but has been designed for practical use and has been applied to a significant real-world case study: Roborace, a competition of autonomous racing cars.

Reminder: my full annotated publication list is here.

VN:F [1.9.10_1130]
Rating: 0.0/10 (0 votes cast)
VN:F [1.9.10_1130]
Rating: 0 (from 0 votes)