THE CADP NEWSLETTER - Nr. 16
July 24, 2023
This newsletter is available from the CADP Home page.
Contents
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:
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:
-
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.
Back to the CADP Home Page
