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

THE CADP NEWSLETTER - Nr. 11
January 17, 2019

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2018

This page summarizes the recent evolution of the CADP toolbox from the point of view of its community of users and software developers. Other results, including scientific advances, publications, applications of CADP to industrial problems, and new prototype tools built on top of CADP can be found in the yearly activity report of the CONVECS team.

In 2018, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2018. From version 2018-a to version 2019-a, 28 bugs have been fixed and 68 improvements have been brought.

The diagram to the right gives the repartition of efforts between the various components of CADP. Effort was not measured in time but in the number of lines of the HISTORY file, based on the reasonable assumption that the more involved a change, the more lines needed to describe it.

2. Overview of main enhancements

This section summarizes the main enhancements in the various components of CADP. For more details, please refer to the CADP change list and to the HISTORY file provided in the CADP distribution.
BCG

In 2018, the work focused on the usability of the BCG_STEADY and BCG_TRANSIENT tools for probabilistic/stochastic systems. The command-line options of BCG_STEADY and BCG_TRANSIENT have been simplified, and warning messages are issued if the input BCG graphs do not contain any stochastic transitions. A bug was fixed, and diagnostic messages no longer mix state numbers and matrix indexes. The tools have been extended to accept single-state Markov chains and to forbid probabilistic self-loops, as was already the case for longer circuits of probabilistic transitions, since both represent similar "timelock" situations.

For details, see HISTORY entries: #2383 #2389 #2391 #2393 #2395 #2396.

DEMOS

Two new demo examples have been added: demo_06 (Transport Layer Security v1.3 handshake protocol specified in LNT), and demo_11 (a hardware block implementing a Dynamic Task Dispatcher). The demo_12 (Message Authenticator Algorithm) is now documented in a publication [Garavel-Marsso-18]. The demo_17 (distributed leader election protocol) has converted from LOTOS to LNT. Finally, most existing demo examples have been updated to reflect the evolution of the MCL v3 and SVL languages.

For details, see HISTORY entries: #2411 #2422 #2425 #2434 #2435 #2438 #2439 #2441 #2448 .

DOC

Two manual pages ("bes" and "seq") have been added, which provide standalone definitions of CADP's BES format for Boolean Equation Systems and SEQ format for execution traces. A new publication [Garavel-Lang-Mounier-18] has been added, which provides a tutorial and a survey on compositional verification. The description of shell variables in the SVL manual page has been enhanced. The OPEN/CAESAR manual pages have been enhanced to give full prototypes for function parameters and to reflect prior changes related to the type CAESAR_TYPE_FORMAT.

For details, see HISTORY entries: #2386 #2449 #2451 #2459 #2475 #2476.

LNT

In 2018, a significant effort was devoted to the TRAIAN 3.0 native compiler for LNT, which is developed in parallel with CADP, and to enhancements of the SYNTAX compiler-generation system used by many CADP tools. The LNT tools of CADP benefited from this effort: for instance, in the warning and error messages emitted by LNT2LOTOS, line numbers have been made more precise. In addition to a bug fix, the LNT_DEPEND tool, which computes dependencies between LNT modules has been entirely rewritten and made much faster. Also, the LNT language has been simplified by removing "!external" pragmas for constructors, as "!external" pragmas for types are sufficient.

For details, see HISTORY entries: #2390 #2450 #2462 #2478.

LOTOS

In addition to three bug fixes, the CAESAR and CAESAR.ADT compilers for LOTOS now enjoy a new option "-depend", which displays the list of library files transitively included in a LOTOS specification.

For details, see HISTORY entries: #2406 #2428 #2430 #2431.

MCL

The MCL v3 language was modified and aligned on the MCL v4 language by removing syntactic differences that existed between both languages concerning the infinite repetition operator ("@") and the respective precedences of the concatenation (".") and choice ("|") operators in regular expressions. MCL v3 has also been enriched with the option operator ("?") on regular formulas already present in MCL v4.

Following such changes, the two versions of MCL_EXPAND for MCL v3 and MCL v4 have been unified in one single tool, which is now invoked by both EVALUATOR 3 and EVALUATOR 4. The corresponding manual pages have been simplified accordingly, with the introduction of two overarching manual pages ("mcl" and "evaluator"). Two new options have been added to these tools: "-depend", which displays the libraries transitively included in an MCL file, and "-source", which is used by SVL to display correct file names and line numbers for MCL formulas embedded in SVL scripts.

In addition to five bug fixes, the memory footprint of MCL_EXPAND has been reduced. MCL_EXPAND, EVALUATOR 3, and EVALUATOR 4 now display error messages in which line numbers are those of the source ".mcl" files, rather than the intermediate ".xm" files generated by XTL_EXPAND. Also, better error messages are produced for MCL formulas of alternation depth greater than one, and for MCL v3 input files containing a correct formula written in MCL v4.

For details, see HISTORY entries: #2388 #2392 #2394 #2398 #2407 #2408 #2409 #2412 #2413 #2414 #2415 #2416 #2417 #2420 #2423 #2424 #2427 #2432.

MISC

In addition to one bug fix in SVL, the "property" statement of SVL has been made more general. A new shell macro SVL_COMMAND_FOR_CLEAN() has been added to the SVL library. SVL now invokes EVALUATOR 3, EVALUATOR 4, and XTL with their new "-source" option to get error and warning messages in which file names and line numbers are those of the SVL scripts containing temporal logic formulas.

In addition to two bug fixes, INSTALLATOR now displays better messages about stable/beta versions and the CADP installator web page has been improved. The EUCALYPTUS graphical user interface has also been enhanced in various ways.

For details, see HISTORY entries: #2384 #2385 #2401 #2410 #2418 #2437 #2443 #2445 #2447 #2472 #2479.

NUPN

The CAESAR.BDD tool for NUPNs (Nested-Unit Petri Nets) has been extended with 12 new options, and the meaning of its "-redundant-units" option has changed. A new tool named NUPN_INFO has been added to the CADP toolbox to perform three normalizing transformations of NUPNs. Two bugs have been fixed, and various corrections and enhancements have been brought to the CAESAR.BDD manual page.

For details, see HISTORY entries: #2404 #2452 #2453 #2457 #2458 #2460 #2463 #2466 #2473.

OPEN/CAESAR

The CADP toolbox now contains a new tool named SCRUTATOR for pruning Labelled Transition Systems on the fly. The OPEN/CAESAR environment was enriched with a new SOLVE_2 library for solving linear equation systems on the fly. In addition to a bug fix in EXP2C, a new option "-depend" has been added to EXP2C and EXP.OPEN for displaying all files transitively included in an EXP file. A bug was fixed in TGV and a new option "-self" has been added to suppress warnings about *-transitions automatically inserted in output-incomplete test purposes. DISTRIBUTOR now triggers distributed termination of all computing nodes as soon as a state table overflows on one node; also, the ".log" files generated by DISTRIBUTOR now follow the same naming conventions as the ".bcg" fragments also generated by DISTRIBUTOR.

For details, see HISTORY entries: #2397 #2399 #2426 #2429 #2433 #2436 #2467 #2477.

PORTS

The CADP toolbox has been ported to Solaris 11 and to SunOS 5.11 OpenIndiana "Hipster". The GC garbage collector library (invoked by the "-gc" option of CAESAR) was upgraded to version 7.6.4 to avoid issues observed on Solaris, and recent versions of GNU indent are now supported.

CADP has also been ported to macOS 10.14 "Mojave" and a 64-bit version of CADP is now available for macOS. An error in the installation directives for macOS has been corrected.

On Windows, two bugs have been fixed; the "cadp_cygwin.com" performs additional checks and OCIS has been simplified.

Globally, error and warning messages of most CADP compilers have been unified. The creation of temporary files and directories was made safer by the introduction of a new script named CADP_TEMPORARY. Finally, the TST script was enhanced to detect two new situations in which CADP is not properly installed.

For details, see HISTORY entries: #2387 #2400 #2402 #2403 #2405 #2419 #2421 #2440 #2454 #2455 #2456 #2461 #2465 #2464 #2469 #2471 #2474.

XTL

In addition to four bug fixes, the XTL model checker has been extended with two new options: "-depend", which lists the files transitively included by an XTL specification, and "-source", which is used by SVL to display correct file names and line numbers for those XTL formulas embedded in an SVL scenario. Also, the XTL compiler now performs consistency checks on the C identifiers specified by the pragmas "!implementedby", "!comparedby", "!enumeratedby", and "!printedby".

For details, see HISTORY entries: #2408 #2442 #2444 #2446 #2468 #2470.

3. Acknowledgements

We are extremely grateful to the following scientists, who provided us with valuable feedback and advice about the use of CADP:

and all other persons we may forget.

Back to the CADP Home Page