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

THE CADP NEWSLETTER - Nr. 8
January 17, 2016

This newsletter is available from the CADP Home page.


Contents

1. Progress of CADP during year 2015

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 2015, the development of CADP has steadily progressed. Following the monthly rolling-release model established in 2013, twelve versions of CADP have been released in 2015. From version 2015-a to version 2016-a, 61 bugs have been fixed and 104 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

A new major version 1.2 of the BCG format for storing Labelled Transition Systems was released as part of CADP 2015-a. Following this change, various minor residual bugs have been identified and fixed in 2015, and the type system of XTL has been modified to require fewer explicit type coercions.

For details, see HISTORY entries: #1993 #1994 #1996 #2004 #2008 #2016.

CAESAR

In addition to a few bug fixes, the "-root" option of the CAESAR compiler has been generalized to support process having value parameters; this makes compositional verification easier by removing the need for introducing extra processes having no value parameters. Also, the EXEC/CAESAR interface has been extended with two new primitives CAESAR_KERNEL_DELAY and CAESAR_KERNEL_EXIT().

For details, see HISTORY entries: #2009 #2014 #2033 #2035 #2065 #2085.

CAESAR.ADT

Optimizations have been introduced to generate shorter and simpler C code, and to make sure that this C code compiles without spurious warnings.

For details, see HISTORY entries: #2038 #2094 #2097.

CAESAR.BDD

The CAESAR.BDD tool that analyzes NUPN (Nested-Unit Petri Nets) models and serves to prepare the yearly Model Checking Contest has been enhanced in several ways. In addition to 7 bug fixes, 14 new command-line options have been added to CAESAR.BDD ("-arcs", "-bits", "-creator", "-density", "-encodings", "-height", "-hwb", "-multiple-arcs", "-multiple-initial-tokens", "-places", "-redundant-units", "-transitions", "-units", and "-width"). The output format produced by the "-exclusive-places" option has been revised. The "-mcc" option now computes the extended free choice property. A new option "-network nupn" was also added to EXP.OPEN to produce NUPN models from automata networks.

Particular efforts have been put into increasing the scalability of CAESAR.BDD for large models. Reading large NUPN files was made much faster. The "-exclusive-places" option of CAESAR.BDD was made faster too. The size of the largest data structure allocated by CAESAR.BDD has been divided by four. CAESAR.BDD has also been optimized to save memory when handling NUPN models having a simple hierarchical structure. Finally, user-specified timeouts are better supported.

For details, see HISTORY entries: #1991 #2000 #2054 #2055 #2056 #2057 #2058 #2059 #2061 #2062 #2063 #2068 #2069 #2073 #2077 #2078 #2081 #2083 #2089 #2091 #1941 #2093 #2102 #2104.

DEMOS

The demo examples, which are a showcase for CADP, have been improved by taking advantage of recent enhancements to CADP languages and tools. Five demos (16, 21, 22, 36, and 38) have been rewritten from LOTOS to LNT. A new demo 05 (airplane-ground communication protocol) has been added. The code of many demos was updated to use the latest features of LNT, such as "in var" parameters and "assert" statements. Demos 14 and 16 have been greatly simplified by inlining MCL and XTL temporal logic formulas in SVL scripts, using the "property" and "check" statements recently added to SVL. Nine demos (02, 08, 17, 20, 27, 28, 31, 33, and 36) have been simplified by using the new possibility to pass value parameters to LOTOS and LNT processes directly in SVL scripts. XTL formulas have been shortened in demos 23 and 27. Finally, demo 38 led to a publication at the MARS'15 workshop.

For details, see HISTORY entries: #1989 #1990 #1999 #2023 #2025 #2039 #2041 #2050 #2067 #2074 #2086 #2092 #2099 #2116 #2121 #2123 #2144 #2145 #2146 #2153.

DOC

Several manual pages of CADP have been made more readable by splitting each of them into two different manual pages: one describing a given computer language or file format (namely, EXP, GCF, NUPN, PBG, RBC, SVL, and XTL), and another one describing the tool(s) operating on this language or format. Also, PostScript files have been removed, making the CADP distribution 60-megabytes leaner.

For details, see HISTORY entries: #2019 #2095 #2107 #2125 #2128 #2135 #2136.

EXT

The connection to ext ernal software development tools has progressed. The support of the LOTOS and LNT languages in the Emacs/XEmacs, jEdit, and Vim editors has improved. More text editors are now supported, including Nano, Notepad++, and all the text editors compliant with GtkSourceView 3.0 (including the Gedit editor of Gnome). Pretty-printers such as a2ps and the LaTeX "listings" package are also supported. Configuration files for three CADP languages (MCL, SVL, and XTL) and three CADP formats (BES, NUPN, and RBC) have been added.

For details, see HISTORY entries: #2016 #2022 #2028 #2046 #2048 #2051 #2071 #2072 #2084 #2115 #2118 #2120 #2142 #2143 #2151.

LNT

Significant effort has been devoted to improve the LNT toolchain (namely, the LPP, LNT2LOTOS, LNT.OPEN, and LNT_CHECK tools). In addition to 22 bug fixes (incorrect error messages, undetected overflows, wrongly-generated LOTOS code, etc.), the LNT language has been enhanced in several aspects. The "case" construct now supports multiple (tuple-like) expressions and patterns. Better messages are emitted for "in" and "in out" parameters, and two new parameter-passing modes "in var" and "out var" have been introduced to allow finer data-flow analyses. Exceptions are better handled and a new "assert" statement was added to LNT. The "none" channel is now implicitly predefined. The "-root" option of LNT2LOTOS now accepts value parameters for LNT processes. Finally, the LNT reference manual has been extended and updated at many places.

For details, see HISTORY entries: #2007 #2012 #2018 #2024 #2026 #2032 #2034 #2036 #2043 #2045 #2047 #2049 #2053 #2060 #2064 #2066 #2070 #2075 #2076 #2088 #2098 #2100 #2103 #2109 #2110 #2111 #2112 #2113 #2117 #2119 #2122 #2124 #2126 #2129 #2131 #2132 #2134 #2138 #2139 #2140 #2141 #2147 #2149 #2150 #2152.

MCL

The CAESAR_SOLVE library was enriched with a new algorithm A9 optimized for the Boolean equation systems generated when model checking guarded mu-calculus formulas on acyclic Labelled Transition Systems. The EVALUATOR 3 and EVALUATOR 4 model checkers now take advantage of this new algorithm to reduce memory consumption when operating on such acyclic Labelled Transition Systems. The ACTL (Action-based Computation Tree Logic) library has been made more modular, and a new library was added to provide temporal logic operators adequate with respect to divergence-sensitive branching bisimulation.

For details, see HISTORY entries: #2005 #2006 #2015 #2020 #2148.

SVL

The SVL language was extended and made more regular in many respects. The "property" statement of SVL was generalized and made applicable to any statement. The "expected" statement can now be attached to any shell command. A new "result" statement allows to store in a shell variable the output of a verification statement. The diagnostic file was made optional in comparison, deadlock, and livelock statements. Translation from LNT to LOTOS can now be obtained directly using a simple SVL assignment. Hiding and renaming of labels now work compositionnally on automata networks, without generating the corresponding Labelled Transition Systems. SVL scripts for compositional verification can be much shorter as it is now possible to pass value parameters in the instantiations of LNT and LOTOS processes. Additionally, seven bugs in SVL have been fixed.

For details, see HISTORY entries: #1992 #1997 #1998 #2013 #2017 #2021 #2029 #2030 #2037 #2040 #2042 #2044 #2079 #2090 #2096 #2101 #2114.

MISC

In addition to bug fixes in various tools (e.g., CUNCTATOR, EUCALYPTUS, TST, XTL, etc.), the installation procedures of CADP have been revisited and updated; in particular, work is going on and many preliminary changes have been silently brought to ease installation of CADP on Windows.

For details, see HISTORY entries: #1995 #2001 #2002 #2003 #2010 #2011 #2027 #2031 #2052 #2080 #2082 #2087 #2105 #2108 #2127 #2130 #2133 #2137.

3. Acknowledgements

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

and all other persons we may forget.


Back to the CADP Home Page