On The Long-Run Development of Formal Verification Tools

The ETAPS Test-of-Time Tool Award has been established in 2023 to recognize outstanding tools, older than five years and connected to ETAPS.

For the first edition of this award, the competition was tough, with not less than twelve nominated candidates. It was attributed to Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe, all working at INRIA (Grenoble, France) for the development of the CADP tools. The award was presented at the ETAPS 2023 banquet in Paris.

Following a talk about CADP given at ETAPS on April 27, 2023, we arranged an interview with the four winners to know more about their work and motivation.

Can you introduce yourself and present the CADP software, past and present?

We are four scientists holding permanent full-time research positions at INRIA and working together in the CONVECS team located in Grenoble. Our background combines theory and software engineering.

CADP stands for “Construction and Analysis of Distributed Processes”. It is a long-term project that started in the 1980s and has steadily expanded since then. At present, CADP is a comprehensive toolbox gathering 50 tools and 17 software libraries. It is used for modelling and verifying asynchronous concurrent systems: communication protocols, software systems, hardware circuits, etc.

Based upon the sound concepts of concurrency theory (process calculi, bisimulations, modal mu-calculus, communicating automata, nested-unit Petri nets, etc.), CADP provides a wealth of features, including compilation and rapid prototyping, interactive and guided simulation, model checking, equivalence checking, test-case generation, and performance evaluation.

By whom is CADP used, and for which applications?

CADP is distributed worldwide and, so far, more than 15,000 licences have been granted. There are three main types of usage:

• Lecturers use CADP to support their university courses, e.g. to set up lab exercises that teach students how the theoretical concepts of process calculi, bisimulations, model checking, and compositional verification can be deployed in practice.

• Academic researchers use CADP as a set of software components to quickly develop new formal-methods tools or implement new languages (e.g., domain-specific modelling languages) by translation to LNT or LOTOS. So far, more than 100 research tools have been built on top of CADP.

• CADP is also used to formally describe and verify many kinds of concurrent problems commonly found in telecommunication systems, software programs, and hardware circuits. Because CADP is built on generic concepts, its palette of applications is quite diverse, encompassing communication protocols, distributed algorithms, cloud and fog computing, internet of things, systems and networks on a chip, or even cognition processes in the human brain. More than 200 case studies using CADP have been published, a number of which carried out in industry with companies such as Google, Nokia Bell Labs, Orange Labs, STMicroelectronics, Tiempo, etc.

How would you compare CADP to other model checkers?

The development of CADP was undertaken in the 80s. CADP is, together with SPIN, one of the two oldest model checkers still used today. CADP is based on the concepts of the European school of concurrency theory: process calculi, mu-calculus, bisimulations, etc. Therefore, it differs from conventional model checkers in at least three points:

• To describe concurrent systems, CADP does not use some ad hoc input language specifically tailored for model checking. Instead, it supports three high-level modelling languages derived from the seminal works of Tony Hoare and Robin Milner on process calculi: LOTOS (the ISO international standard 8807), FSP (a language designed at Imperial College for teaching concurrency to university students), and LNT. The latter, based upon the ideas of E-LOTOS (the ISO international standard 15437) and Occam, blends functional and imperative programming languages with process calculi. For each of these three languages, CADP provides compilers and translators that go far beyond the usual needs of model checking. For instance, many compilers present in CADP, including the LNT translators themselves, are written in LNT, which is both a modelling and a programming language.

• To represent the state spaces of concurrent systems, CADP uses labelled transition systems and nested-unit Petri nets. These models are action-based (as opposed to state-based), in the sense that only the transitions and their labels can be observed, while the contents of states (e.g., state variables) are not visible, unless explicitly displayed on transitions. Action-based models have many advantages: in particular, they naturally preserve properties when models are translated from one action-based modelling language to another. Also, state spaces (i.e., labelled transition systems) can be stored in computer files and abstracted away using various transformations.

• To express the expected properties of concurrent systems, CADP does not use the conventional temporal logics CTL or LTL, but provides a rich language named MCL, which is an action-based, branching-time property language (contrary to, e.g., SPIN which is state-based and linear-time). MCL relies on the (alternation-free) modal mu-calculus extended, on the one hand, with regular expressions (which allow to describe execution sequences concisely, and are well understood by hardware and software engineers) and, on the other hand, with a data language (which enables useful properties to be expressed, such as the fact that message sequence numbers are strictly increasing on any execution sequence).

Beyond model checking, CADP also supports equivalence checking (i.e., bisimulations and behavioural preorders) for verifying whether two state spaces are equivalent or contained one in the other. The joint use of process calculi, action-based models, and bisimulations paves the way for compositional verification, an effective divide-and-conquer strategy for fighting state-space explosion. To this aim, CADP provides a scripting language named SVL, which allows to easily express complex scenarios of compositional verification in the large.

Additionally, CADP also supports many verification techniques, including explicit, on-the-fly, and distributed generation of state spaces, property-dependent reductions, partial model checking, etc., which can be used separately or in combination. Such unique features enable CADP to scale up and tackle complex problems that are out of reach for conventional model checkers. For instance, CADP won six gold medals at the RERS 2019 challenge of ETAPS (by correctly evaluating 100% of 360 CTL and LTL formulas on large networks of concurrent automata) and 3 gold medals at the RERS 2020 challenge (by correctly evaluating 88% of 90 CTL formulas and giving don’t know answers for 11 formulas only).

CADP is not monolithic software, but a collection of many tools and libraries organized with a modular structure and well-defined programming interfaces. Finally, CADP does more than verification, as it also supports interactive simulation, rapid prototyping, and test generation.

Are there recipes to develop software with impact?

Rather than stating general laws valid for any kind of software, we can make, based on our experience with CADP, a few remarks concerning formal methods.

Formal verification tools are clearly useful for the design of safe and secure systems, the complexity of which often exceeds human capabilities. However, such tools are themselves complex, and require expertise and skills from their users. At present, the industry seems reluctant to invest enough resources in such tools, leaving plenty of space to academic research.

We believe that software development should not be driven by the desire to obtain academic recognition; instead, it should be based on the conviction of providing effective solutions to relevant problems, for which practical approaches are lacking.

In formal methods, most low-hanging fruits have already been picked: further progress requires hard work and tenacity, shifting from early prototypes to advanced tools that can scale to large, industrial applications. This does not come fast and easy: one must undertake long-term software development with many time-consuming auxiliary duties, such as porting software to continuously evolving processors and operating systems, writing extensive documentation, fixing bugs reported by users, building and maintaining large test suites, creating and managing a website, etc.

Unfortunately, these mandatory activities may have an adverse impact on academic career. Indeed, most of them are “invisible”, in the sense that they are not suitable for publication. Also, dedicating efforts to large, long-term software makes it less easy to adopt new research goals, embrace the most recent “hot topics”, and follow the latest trends from funding agencies. Developing software to promote certain key ideas often comes with a price to pay, be it slower career evolution or reduced resources.

Finally, even if the development of formal verification tools is a long-run enterprise, this should not prevent these tools to be regularly challenged against realistic problems, such as industrial case studies or benchmarks from software competitions.

How do you manage to maintain such a large software?

There is a fundamental difference between publication and software: once a scientific paper has been published, work is done; once a research tool has been released, heavy-duty maintenance work starts.

Maintaining scientific software on the long run is a difficult problem, already addressed by Reiner Hähnle in his striking interview of April 2023 on the ETAPS blog. In the particular case of CADP, we address this problem in six combined ways:

• Developers: a crucial aspect for the long-term survival of research tools is the presence of a permanent team who takes maintenance in charge. Formal verification tools require different expertises, i.e., being good at understanding and advancing theory vs being good at implementing complex algorithms efficiently. This usually leads to division of work (e.g., researchers vs engineers, professors vs students, etc.), often with loss of knowledge when non-permanent people leave. Instead, CADP benefits from INRIA’s full-time research positions, with permanent researchers capable of maintaining and evolving all the CADP tools.

• User community: the multiple uses of CADP for teaching, developing research software, and tackling case studies provides useful feedback that is exploited to fix bugs and enhance the languages and tools of CADP. The time that we do not spend on teaching commitments enables fruitful interactions with many colleagues and students all around the world.

• Simplicity: to lower maintenance costs, drastic choices have been made. CADP was built using stable languages (C, Bourne shell, Tcl/Tk), which are portable and change slowly, rather than using fancy, fast-evolving technologies. CADP has simple graphical user interfaces, to avoid the high costs of sophisticated interfaces. The web site of CADP only uses static pages to avoid the frequent updates and security issues of web frameworks. We also ask users to upgrade their version of CADP at least once a year to avoid spending time on reports of bugs that were solved long ago.

• Stability: CADP progressively grew over years, passing from 2 to 50 tools. As much as possible, we favour perennial interfaces and avoid breaking compatibility. Users who learnt CADP years ago can still find the tools they know working in the same way as before. When incompatible changes are required, we seek to provide migration solutions, e.g., by replacing deprecated tools with shell scripts that offer the same functionalities but invoke newer tools under the hood, or by providing scripts that update user programs automatically to reflect changes in the languages supported by CADP.

• Quality: we try to follow the principles of software engineering and rigorous development, by designing robust components that can be used over the years with limited changes. We pay great attention to code quality: the CADP tools written in C compile without warning using various compilers under stringent analysis options; the CADP tools written in LNT also compile without any warning from both the LNT and C compilers.

• Validation: the most critical parts of CADP have been developed using peer programming or proofread during code reviews. We also perform intensive non-regression testing. Every night, all CADP demo examples are executed and checked on various operating systems. For each CADP tool, we maintain large test suites (totalling several hundreds of thousands of models and millions lines of code) which serve to check new versions of the tool.

What are the next challenges ahead for you?

We are grateful to ETAPS for distinguishing our work: the Test-of-Time Tool Award is a strong incentive to pursue our research. At the moment, we see at least three major challenges:

• Continue developing languages and tools that can be used by non-experts. Our native LNT compiler is already a significant step in this direction. We will then consider convergence between LNT and MCL, i.e., the imperative language for modelling concurrent systems and the declarative language for expressing system properties. We are also seeking to increase automation, e.g., by assisting users for compositional verification.

• Exploit the capabilities of modern processors to deliver greater performance. This is the goal of parallel and distributed verification tools, which take advantage of many-core processors and of clusters of machines. This is a challenging task: sequential verification algorithms are already quite involved, but making them parallel or distributed adds another dimension to their complexity.

• Bridge the gap between model checking and theorem proving. The LNT language is already equipped with assertions, pre- and post-conditions in both sequential and parallel code. Many of these could be passed to SAT solvers and theorem provers for checking their correctness. Given that the most recent tools of CADP are written in LNT (“self-hosted”), this paves the way for formal-methods tools themselves developed using formal methods.