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

THE CADP NEWSLETTER - Nr. 7
January 29, 2015

This newsletter is available from the CADP Home page.

Contents

1. Progress of CADP during year 2014

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

This diagram highlights the effort put on the LNT language, which is a next-generation process calculus that progressively replaces LOTOS. Since 2010, all academic and industrial case studies done by the VASY and CONVECS teams have been modelled using LNT rather than LOTOS. In 2014, the LNT language was enhanced and its tools consolidated.

The SVL language was also significantly enriched with new operators that make SVL scripts more expressive and more readable. Many CADP demos have been upgraded to take advantage of these enhancements, and also to show value-passing temporal logic formulas in the MCL language supported by the EVALUATOR 4 model checker.

Also, the AUT and BCG formats, as well as the XTL language and compiler have been revised and extended to better support the data-type capabilities of the LNT language, in particular variable-length strings and user-defined data structures.

Finally, the CAESAR.BDD tool was significantly expanded as a means to strengthen the cooperation between the process-calculi and Petri-net communities.

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.
AUT

The AUT textual format for CADP for storing Labelled Transition Systems was extended to support recent languages (such as LNT, and the PseuCo language developed at Saarland University) that manipulate character-string values. The AUT format, which was defined in the late 80s, did not support such values. A new version 2014 of the AUT format has been defined, which solves this problem and maintains backward compatibility. All the CADP tools that read or write AUT files have been updated accordingly.

For details, see HISTORY entries: #1893 #1895 #1900.

BCG

The BCG format of CADP for storing Labelled Transition Systems has been upgraded with the advent of a new version 1.2, which replaces version 1.1 released in 2009. New predefined types have been added to BCG to express the difference between unsigned and signed integers, and between character strings and untyped raw-data values. The new version of the BCG format is also more compact and now uses variable-length encoding for strings. The rules for label parsing of the BCG_WRITE interface have been extended, and BCG_IO now supports version 2014 of the AUT format. The intrinsic difficulty of these changes was to preserve the backward compatibility with the BCG files generated over the last twenty years.

For details, see HISTORY entries: #1877 #1880 #1885 #1943 #1944 #1947 #1951 #1953 #1954 #1956 #1957 #1958 #1960 #1961 #1962 #1963 #1965 #1966 #1970 #1903.

BCG_CMP

The recent BCG_CMP tool for the efficient comparison of Labelled Transition Systems has been refined by fixing five residual issues.

For details, see HISTORY entries: #1782 #1827 #1868 #1896 #1898.

CAESAR

The CAESAR compiler has been modified to tolerate LOTOS specifications that would be normally rejected under the ISO/IEC 8807 standard definition of LOTOS. The first change extends the visibility scope of local definitions when the global definitions are empty. The second change uses the type information of process definitions to better resolve overloading ambiguities in expressions passed as actual parameters to process calls.

Conversely, CAESAR was made stricter by rejecting at compile-time LOTOS specifications containing out-of-bound constants, even if such constants are never used.

Performance has been increased by adding or strengthening a number of optimizations concerning, e.g., internal data structures, Boolean guards that can be statically evaluated, values belonging to singleton sorts, disconnected or otherwise unreachable Petri net places and transitions, etc.

For details, see HISTORY entries: #1774 #1779 #1789 #1803 #1875 #1890 #1907 #1909 #1911 #1914 #1917 #1920 #1924 #1933 #1935 #1937 #1986.

CAESAR.ADT

Version 5.4 of the compiler for LOTOS data types has an additional optimization to generate better C code.

For details, see HISTORY entry: #1775.

CAESAR.BDD

The CAESAR.BDD tool, which analyzes hierarchical Petri nets generated from higher-level specifications (e.g., LOTOS or LNT) has been significantly enhanced. The semantic model accepted by CAESAR.BDD has been made more general and given the new name of NUPN (Nested-Units Petri Nets). The definition and theoretical properties of NUPN have been formalized.

The textual syntax for NUPN has been extended with pragmas intended to retain useful properties of non-ordinary and/or non-safe Petri nets translated to NUPN. An XML syntax for NUPN (compatible with the ISO standard PNML for the representation of Petri nets) has been defined and adopted by the Model Checking Contest. A translator from PNML to NUPN has been developed at LIP6 (Paris, France).

The CAESAR.BDD tool has been updated accordingly, and extended to perform stricter checks and compute more structural and behavioural properties of NUPN models. CAESAR.BDD has been intensively used to correct the descriptions of the Model Checking Contest benchmarks: a first campaign (January-February 2014) detected 9 errors in structural properties and 8 errors in behavioural properties, and a second campaign (April 2014) revealed 23 more errors. CAESAR.BDD has also been used to automatically generate new benchmarks, together with their descriptions.

For details, see HISTORY entries: #1780 #1781 #1793 #1795 #1797 #1807 #1809 #1812 #1814 #1815 #1819 #1822 #1823 #1828 #1829 #1832 #1833 #1835 #1848 #1871 #1941 #1980.

DEMOS

The demo examples of CADP, which have been progressively accumulated since the origins of the toolbox, are a showcase for the multiple capabilities of CADP, as well as a test bed to assess the new features of the toolbox. The effort to maintain and enhance these demos has been pursued. The progressive migration to LNT has continued, by translating certain demos from LOTOS to LNT. Many demos have been enriched with value-passing temporal formulas that illustrate the conciseness and expressiveness of MCL and the capabilities of the EVALUATOR 4 model checker. Finally, many demos have been shortened and made more readable by using the new features of SVL, especially the "property" and "|=" statements that allow formulas to be gathered in a single SVL file rather than disseminated in a collection of MCL or XTL files.

For details, see HISTORY entries: #1840 #1855 #1860 #1873 #1874 #1879 #1928 #1932 #1934 #1976 #1987 #1988.

EXP

The warnings emitted by the EXP.OPEN tool have been enhanced, and the syntax of the EXP language was made closer to that of LNT, so that composition expressions (including comments, channel typing, etc.) can be directly copied from LNT programs to be pasted in SVL scripts while requiring as few syntactic changes as possible.

For details, see HISTORY entries: #1802 #1804 #1806 #1808 #1940.

EXT

The connection to ext ernal software development tools has progressed. To support the LNT language in the Emacs/XEmacs, jEdit, and Vim editors, configuration files have been added or updated, which provide for syntax highlighting/coloring, and enable autocompletion in Emacs using YASnippet.

For details, see HISTORY entries: #1905 #1910 #1912 #1942.

LNT

The translator from LNT to LOTOS was further improved. In addition to bug fixes and removal of incorrect warnings emitted by the translator itself or by the C compiler on the generated code, the following enhancements have been brought: the LNT language was extended with a "!representedby pragma for processes, and a "only if" statement to concisely express guarded commands; the translator now performs static analysis and warns about unused variables, unused "in" or "in out" parameters, useless (deterministic or nondeterministic) assignments to variables, "in out" parameters that are never assigned, and dubious synchronizations between processes; checks for underflow/overflow on natural and integer numbers are now activated by default. The translator also generates better LOTOS code, and the LNT reference manual was shortened and updated in many places.

For details, see HISTORY entries: #1776 #1777 #1778 #1784 #1786 #1787 #1788 #1790 #1792 #1794 #1796 #1798 #1799 #1800 #1805 #1810 #1811 #1813 #1824 #1825 #1826 #1830 #1831 #1834 #1836 #1837 #1839 #1843 #1845 #1846 #1847 #1850 #1851 #1852 #1853 #1854 #1856 #1857 #1858 #1859 #1861 #1862 #1865 #1878 #1881 #1887 #1939.

SVL

In addition to bug fixes and enhancements of error messages, the syntax of SVL language for comments, gate typing, and the "par", "hide", "rename", "cut", and "prio" operators was extended to be compatible with the syntax of LNT.

The "verify" operator has been generalized to give access to all three model checkers of CADP (EVALUATOR 3, EVALUATOR 4, and XTL). A new statement "|=" has been added to SVL, which enables MCL and XTL formulas to be directly written in an SVL script, rather than being stored in external files.

To provide for requirements expression and traceability in SVL, two new statements, "property" and "check", have been introduced. They increase the readability and good structure of SVL scripts by allowing to define and verify properties, each of which is given a name, instantiable parameters, an informal textual description, and (optionally) an expected truth value.

For details, see HISTORY entries: #1783 #1864 #1866 #1867 #1869 #1870 #1904 #1906 #1908 #1913 #1916 #1918 #1919 #1921 #1923 #1925 #1927 #1929 #1930 #1936 #1938 #1985.

TGV

The test-generation tool TGV has been streamlined by removing some obsolete options and replacing a large part of its code by calls to the standard CADP libraries. TGV has been made faster, it now supports the latest version of the AUT format, and ensures that test purposes provided in the BCG format are deterministic. The manual page has been updated and completed.

For details, see HISTORY entries: #1897 #1894 #1902.

TYPES

The ability to compile and verify formal specifications with complex, user-defined operations and data structures is a key feature of the CADP toolbox since its very origins. A long-run effort has been recently undertaken to ensure a uniform treatment of types, values, and functions across all the various CADP tools.

Convergence between the LOTOS, LNT, BCG, and XTL data-type libraries has been increased by defining common libraries for eight predefined types: Boolean, Natural, Integer, Real, Character, String, Raw, and Gate. These libraries gather in the same place definitions of types, constants, and functions that were previously disseminated across different tools. Additionally, systematic checks for underflows and overflows have been set for the Natural and Integer types. Also, unprintable characters and C-like escape sequences are now uniformly handled by the Character, String, and Raw types.

For details, see HISTORY entries: #1838 #1849 #1863 #1872 #1876 #1882 #1883 #1884 #1891 #1945 #1946 #1950 #1948 #1952 #1955.

XTL

In addition to many bug fixes, the XTL compiler and its XTL_EXPAND preprocessor have been strengthened to better detect and report potential mistakes in source XTL specifications. In particular, vacuity checks have been introduced, which warn the user when no label in a BCG graph has the right number of fields or the appropriate field types to satisfy an XTL label match expression (previously, this expression would silently evaluate to false).

The type checking system of XTL and its list of predefined functions have been extended to support the new Natural and Raw types of the BCG format, and to properly distinguish between Natural and Integer values, and Raw and String values, while achieving a high degree of backward compatibility. In particular, XTL now uses type information from the BCG labels to better solve overloading in label offers, so that certain XTL programs that were formerly invalid are now accepted. Finally, it is now possible to use the predefined types and functions of XTL when defining temporal operators directly using external C code.

For details, see HISTORY entries: #1791 #1931 #1949 #1959 #1964 #1967 #1968 #1969 #1971 #1972 #1973 #1974 #1975 #1977 #1978 #1979 #1982 #1983 #1984.

MISC

Other changes and fixes to the CADP tools have been made, which are too diverse to be described individually here.

For details, see HISTORY entries: #1772 #1773 #1785 #1801 #1816 #1817 #1818 #1820 #1821 #1841 #1842 #1844 #1886 #1888 #1889 #1892 #1899 #1901 #1915 #1922 #1926 #1931 #1981.

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