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

THE CADP NEWSLETTER - Nr. 10
January 18, 2018

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2017

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 2017, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2017. From version 2017-a to version 2018-a, 37 bugs have been fixed and 69 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.
CAESAR and CAESAR.ADT

A buffer overflow and two out-of-bound array accesses have been fixed in both CAESAR and CAESAR.ADT. Two memory allocation bugs have also been fixed in CAESAR.ADT. The latter tool now generates C code that gives better diagnostic when the evaluation of a constant fails at run time (e.g., when it triggers an exception signal, or exhausts the stack or heap memory).

For details, see HISTORY entries: #2290 #2298 #2299 #2326 #2355.

DEMOS

Demo_05 has been modified to use the new syntax of exceptions in the LNT language. The LOTOS and LNT specifications of demo_12 ("Message Authenticator Algorithm") have been entirely revised, based upon the fine knowledge acquired by modelling this cryptographic function as a term rewrite system [Garavel-Marsso-17]. The LNT specification has also been extended to incorporate the test vectors given in the International Standards ISO 8730 and 8731-2. The resulting specification, which was initially too large to be compiled, is now successfully handled after the enhancements brought to the LNT2LOTOS translator. Demo 19 ("Production Cell") has been simplified and is now fully documented in a recent publication [Garavel-Serwe-17].

For details, see HISTORY entries: #2284 #2285 #2287 #2294 #2318.

EXP

EXP.OPEN now has two new options "-prob" and "-rate" for handling probabilistic and stochastic transitions, respectively; without these options, probabilistic and stochastic transitions are considered as ordinary transitions (this enables EXP.OPEN to be used for implementing alternative semantics, such as Interactive Probabilistic Chains where probabilistic transitions are synchronized using a global clock). Consequently, the former "-ratebranching" option has been replaced by "-rate -branching".

Also, error messages about synchronization vectors have been made more precise and EXP.OPEN performs tighter checks about labels containing only blanks and unexpected synchronization of probabilistic or stochastic transitions. Two bug have been fixed in EXP.OPEN and style files have been added to bring support for the EXP format by mainstream text editors.

For details, see HISTORY entries: #2301 #2302 #2304 #2305 #2307 #2308 #2340 #2353.

LNT

The move towards "safer" LNT exceptions initiated in 2016 has been completed in 2017: the two concepts of gates and exceptions have been unified in both LNT processes and LNT functions. The static semantics of LNT no longer requires that variables and exceptions share the same name space.

LNT now permits simple loops (of the form "loop ... end loop", without loop label nor "while" condition) in LNT functions, as well as in LNT processes.

The pragma names "comparedby", "external", "implementedby", "iteratedby", "printedby", and "representedby" are no longer reserved LNT keywords, meaning that it is now permitted to declare LNT identifiers having these names. Two new type pragmas "!card" and "!bits" have been added to specify the maximum number of values and the number of bits to be used when storing the values of a given type in "hash-consing" tables.

The LNT2LOTOS Reference Manual, which contains the definition of the LNT language, has been revised, enriched, simplified in many ways. A recent publication [Garavel-Lang-Serwe-17] presents the historical background and motivation behind the definition of LNT.

In parallel, the LPP preprocessor and the LNT2LOTOS translator, which implement the LNT language, have been enhanced in many ways. In addition to 9 bug fixes, the following enhancements have been made:

  • LPP now implements LNT character strings more concisely.
  • LPP automatically adds the ".lnt" extension to input and output files if this extension is missing.
  • The algorithm that computes which LNT gates are used in each function or process has been made more precise, and LNT2LOTOS now warns about gates that are declared but never used.
  • LNT2LOTOS performs stricter compile-time checks that produce dedicated error messages, rather than generating invalid LOTOS code that was subsequently rejected by CAESAR and/or CAESAR.ADT. Also, several error messages displayed by LNT2LOTOS during its static-analysis phases have been enhanced.
  • The translation from LNT functions to LOTOS operations has been significantly improved by eliminating unreachable or redundant LOTOS equations, removing unused auxiliary LOTOS operations, simplifying the premises of certain LOTOS equations, factorizing identical assignments in "if-then-else" instructions, and optimizing long sequences of assignments intertwined with assertions. Thus, LNT2LOTOS is now faster, uses less memory, generates more compact LOTOS code, and can compile larger LNT specifications that could not be handled before.

For details, see HISTORY entries: #2276 #2278 #2279 #2281 #2283 #2286 #2288 #2289 #2291 #2292 #2295 #2300 #2310 #2314 #2317 #2319 #2321 #2322 #2323 #2325 #2327 #2332 #2342 #2343 #2346 #2347 #2350 #2352 #2354 #2361.

MCL and XTL

In addition to two bug fixes, the warning and error messages displayed by MCL_EXPAND and XTL_EXPAND have been made more precise and stringent. The XTL libraries "walk" and "walk_nice" have been modified not to trigger the extra warnings recently introduced.

For details, see HISTORY entries: #2348 #2365 #2366 #2368 #2371.

OPEN/CAESAR

The "caesar_standard" library was enriched with the new CAESAR_TYPE_FORMAT type and its associated primitives, and with two new functions CAESAR_SET_SIGNALS() and CAESAR_RESET_SIGNALS() for handling POSIX signals (including SIGSEGV, i.e., segmentation violation).

The "caesar_graph" interface, which remained stable for two decades, has been modified: its two functions CAESAR_FORMAT_STATE() and CAESAR_FORMAT_LABEL() became more powerful, while its two functions CAESAR_MAX_FORMAT_STATE() and CAESAR_MAX_FORMAT_LABEL() have been removed from the interface. The same changes apply as well to all other functions CAESAR_FORMAT_*() and CAESAR_MAX_FORMAT_*() of the OPEN/CAESAR libraries. All the OPEN/CAESAR compilers, application tools, and demo examples have been modified to reflect these changes.

For details, see HISTORY entries: #2296 #2297 #2320 #2329 #2330 #2331 #2334 #2344 #2345 #2358.

NETWORK

Many changes have been done to simplify the code of the "caesar_network_1" communication library, which is the backbone of the distributed verification tools of CADP, as well as the code of other tools such as BCG_MIN, but most of these changes are not directly observable by end users. In addition to two bug fixes in "caesar_network_1" and two other bug fixes in the BES_SOLVE tool, the error messages displayed by the various tools and the statistical information produced by the "-stat" option of BES_SOLVE have been made more concise and more informative.

For details, see HISTORY entries: #2277 #2280 #2282 #2306 #2328 #2333 #2359 #2372 #2373.

SVL

A new option "-v" has been added to set SVL variables from the command line (similar to "awk" or "make"). Debugging SVL scripts has been made easier: the "-debug" option of SVL now stops the execution as soon as a shell command (e.g., a CADP tool or a Unix command) terminates with a non-zero exit status, so that problems are detected as soon as they occur.

Also, SVL now performs tighter semantic checks, making sure that all partial-order reduction options passed to EXP.OPEN (namely, options explicitly set by the user and options automatically computed by SVL from the context of the EXP composition expression) are not contradictory.

For details, see HISTORY entries: #2309 #2311 #2312 #2315 #2336 #2364 #2374.

TGV

The test generation tool TGV has been revised. By default, TGV is now much less verbose and only displays the most important information, but the former behaviour can still be retained using option "-verbose". A new option "-monitor" allows to follow in real time how the test-case generation progresses. Many warning and error messages have been enhanced. Various bugs, especially buffer overflows, have been fixed, and memory allocation results is now strictly controlled.

For details, see HISTORY entries: #2337 #2338 #2339 #2341 #2349.

PORTS

Sustained effort has been made to ensure that CADP works properly on mainstream computing platforms. In particular, the RFL and TST scripts and the documentation have been continuously updated. Changes were brought to CADP to cope with recent C compilers (such as GCC 6 and Clang) and to work around problems with the "indent" command available on Solaris and macOS/Xcode.

On Linux, CADP was ported to the latest versions of Centos, Debian 9, and Ubuntu 17.04. The support for the various desktop environments (Gnome, KDE, Mate, etc.) available in Linux distributions has improved.

On macOS, support for obsolete versions (from Mac OS X 10.6 "Snow Leopard" to OS X 10.9 "Mavericks" included) was withdrawn. Support for macOS 10.13 "High Sierra" was added. Preliminary steps have been made to prepare a 64-bit version of CADP on macOS.

On Windows, support for obsolete versions (Windows XP and Vista) was dropped. Following changes in the Cygwin software (February 2017), CADP had to be adapted, as the behaviour of Cygwin pipes and related commands (such as "awk", "grep", and "sed") became different. Numerous changes were made to CADP so as to support the case where Cygwin is not installed in C:/ but in a different folder. Finally, preliminary steps have been made towards a 64-bit version of CADP for Windows.

For details, see HISTORY entries: #2293 #2303 #2313 #2316 #2324 #2335 #2351 #2356 #2357 #2360 #2362 #2363 #2367 #2369 #2370 #2375 #2376 #2377 #2379 #2380 #2381 #2382.

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