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

THE CADP NEWSLETTER - Nr. 12
April 10, 2019

This newsletter is available from the CADP Home page.

Contents

Frédéric Lang and Franco Mazzanti Have Won the RERS 2019 Parallel Challenges

Frédéric Lang (CONVECS, Grenoble, France) and Franco Mazzanti (FMT, Pisa, Italy) recently won all the gold medals for the "Parallel CTL" and "Parallel LTL" tracks of the RERS 2019 challenge.

In 2019, the RERS (Rigorous Examination of Reactive Systems) challenge took place within ETAPS, the primary European forum for software science, as part of the TOOLympics series of software competitions organized to celebrate the 25th anniversary of the TACAS conference.

The goal of the "Parallel CTL" track was to verify 180 properties expressed in the branching-time temporal logic CTL. These properties had to be evaluated on various complex systems, having up to 70 concurrent processes and 234 synchronization actions.

Similarly, the goal of the "Parallel LTL" track was to verify, on the same complex systems, 180 properties expressed in the linear-time temporal logic LTL.

Participants were given a period of only three weeks, starting from the publication of the RERS problems on the RERS web site, to compute and submit their answers. The correct results were only known by the organizers of the RERS challenge.

To attack such difficult problems, Lang and Mazzanti, who had never met before, decided to join forces, and managed to evaluate all the 360 CTL and LTL properties correctly. This was done by designing new verification algorithms and by reusing the compositional verification techniques implemented in the CADP toolbox developed by CONVECS.

They also used additional software tools, such as SPOT for converting LTL formulas to Büchi automata, as well as KandISTI and nuXmv to cross-check some of the results provided by CADP.

Although the rules of the RERS challenge allow the participants to use all possible computing facilities, including supercomputers, the judicious use of compositional verification techniques by Lang and Mazzanti enabled all problems to be solved in about 10 hours on a standard Dell laptop.

The two winners received awards of 625 euros offered by Springer Nature.

The picture to the right was taken during the reward ceremony organized in Prague (Czech Republic) on April 6th, 2019. From left to right: Malte Mues, Franco Mazzanti, Frédéric Lang, Bernhard Steffen, and Falk Howar.

The work of Frédéric Lang has been partly supported by the SECURIOT-2 project.

About CADP

CADP is a software toolbox for the design of asynchronous concurrent systems, such as communication protocols, distributed systems, asynchronous circuits, multiprocessor architectures, etc. Developed since the late 80s, CADP is one of the two oldest model checkers that are still in use today. CADP is actively maintained and finds many applications, both in academia and industry. In March 2019, the 15,000th license of CADP was granted.

About CONVECS

CONVECS is a research project-team common between Inria Grenoble Rhône-Alpes and the LIG (Laboratoire d'Informatique de Grenoble, France), a joint research center between CNRS, Inria, Grenoble INP, and Univ. Grenoble Alpes. The activities of CONVECS focus on the formal modeling and verification of asynchronous concurrent systems, which find applications in many different domains. In particular, CONVECS develops and maintains the CADP toolbox.

About FMT

FMT (Formal Methods and Tools) is a research team of ISTI-CNR (Pisa, Italy). FMT is active in the fields of development and application of formal notations, methods, and software support tools for the specification, design, and verification of complex computer systems. These efforts are based mostly on the foundational concepts and techniques of process algebras, temporal logics, and model checking.

About RERS

The RERS (Rigorous Examination of Reactive Systems) challenge is an international software competition held every year since 2011. RERS 2019 is the 9th edition of the challenge and features several tracks covering sequential, parallel, and industrial problems. Each track provides a wealth of problems of increasing complexity, the most involved of which are expected to be beyond any individual state-of-the-art method or tool. The "Parallel CTL" track was created in 2018 and the "Parallel LTL" track in 2019.

About SECURIOT-2

SECURIOT-2 is a collaborative project funded by the French government's FUI (Fonds Unique Interministériel) and supported by four competitiveness clusters (Minalogic, SCS, Systematic, and DERBI). The goal of SECURIOT-2 is to develop a secure microcontroller that will bring to the IoT environment a high level of security, similar to the one of the secure transactions industry (banking cards and ePassports), in conformity with the requirements of Common Criteria certification. Started in September 2017 for three years and led by TIEMPO Secure, SECURIOT-2 builds upon the expertise of its partners. The main contributions of CONVECS in this project are the formal modeling and verification using CADP of the secure microcontroller developed in the project.

Back to the CADP Home Page