Construction and Analysis of Distributed Processes
Software Tools for Designing Reliable Protocols and Systems

THE CADP NEWSLETTER - Nr. 16
July 24, 2023

This newsletter is available from the CADP Home page.


Contents

1. ETAPS Test-Of-Time Tool Award

On April 26, 2023, the CADP team received the (first-ever) Test-of-Time Tool Award granted by ETAPS, the most important and visible annual European event related to software sciences.

Slides of the Award Lecture at ETAPS 2023.

A few academic links:

2. On The Long-Run Development of Formal Verification Tools

Interview of the CADP team by Marieke Huisman and Bettina Könighofer - Reprinted from the the ETAPS blog

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:

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:

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:

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:


Back to the CADP Home Page