5.1.1 CADP

• Name:
  Construction and Analysis of Distributed Processes
• Keywords:
  Formal methods, Verification
• Functional Description:

  CADP (Construction and Analysis of Distributed Processes – formerly known as CAESAR/ALDEBARAN Development Package) 4 is a toolbox for protocols and distributed systems engineering.

  In this toolbox, we develop and maintain the following tools:

  • CAESAR.ADT  34 is a compiler that translates LOTOS abstract data types into C types and C functions. The translation involves pattern-matching compiling techniques and automatic recognition of usual types (integers, enumerations, tuples, etc.), which are implemented optimally.
  • CAESAR  40, 39 is a compiler that translates LOTOS processes into either C code (for rapid prototyping and testing purposes) or finite graphs (for verification purposes). The translation is done using several intermediate steps, among which the construction of a Petri net extended with typed variables, data handling features, and atomic transitions.

  • OPEN/CAESAR  38 is a generic software environment for developing tools that explore graphs on the fly (for instance, simulation, verification, and test generation tools). Such tools can be developed independently of any particular high level language. In this respect, OPEN/CAESAR plays a central role in CADP by connecting language-oriented tools with model-oriented tools. OPEN/CAESAR consists of a set of 16 code libraries with their programming interfaces, such as:

    • CAESAR  GRAPH, which provides the programming interface for graph exploration,
    • CAESAR  HASH, which contains several hash functions,
    • CAESAR  SOLVE, which resolves Boolean equation systems on the fly,
    • CAESAR  STACK, which implements stacks for depth-first search exploration, and
    • CAESAR  TABLE, which handles tables of states, transitions, labels, etc.

    A number of on-the-fly analysis tools have been developed within the OPEN/CAESAR environment, among which:

    • BISIMULATOR, which checks bisimulation equivalences and preorders,
    • CUNCTATOR, which performs steady-state simulation of continuous-time Markov chains,
    • DETERMINATOR, which eliminates stochastic nondeterminism in normal, probabilistic, or stochastic systems,
    • DISTRIBUTOR, which generates the graph of reachable states using several machines,
    • EVALUATOR, which evaluates MCL formulas,
    • EXECUTOR, which performs random execution,
    • EXHIBITOR, which searches for execution sequences matching a given regular expression,
    • GENERATOR, which constructs the graph of reachable states,
    • PROJECTOR, which computes abstractions of communicating systems,
    • REDUCTOR, which constructs and minimizes the graph of reachable states modulo various equivalence relations,
    • SIMULATOR, XSIMULATOR, and OCIS, which enable interactive simulation, and
    • TERMINATOR, which searches for deadlock states.
  • BCG (Binary Coded Graphs) is both a file format for storing very large graphs on disk (using efficient compression techniques) and a software environment for handling this format. BCG also plays a key role in CADP as many tools rely on this format for their inputs/outputs. The BCG environment consists of various libraries with their programming interfaces, and of several tools, such as:
    • BCG  CMP, which compares two graphs,
    • BCG  DRAW, which builds a two-dimensional view of a graph,
    • BCG  EDIT, which allows the graph layout produced by BCG  DRAW to be modified interactively,
    • BCG  GRAPH, which generates various forms of practically useful graphs,
    • BCG  INFO, which displays various statistical information about a graph,
    • BCG  IO, which performs conversions between BCG and many other graph formats,
    • BCG  LABELS, which hides and/or renames (using regular expressions) the transition labels of a graph,
    • BCG  MIN, which minimizes a graph modulo strong or branching equivalences (and can also deal with probabilistic and stochastic systems),
    • BCG  STEADY, which performs steady-state numerical analysis of (extended) continuous-time Markov chains,
    • BCG  TRANSIENT, which performs transient numerical analysis of (extended) continuous-time Markov chains, and

    • XTL (eXecutable Temporal Language), which is a high level, functional language for programming exploration algorithms on BCG graphs. XTL provides primitives to handle states, transitions, labels, successor and predecessor functions, etc.

      For instance, one can define recursive functions on sets of states, which allow evaluation and diagnostic generation fixed point algorithms for usual temporal logics (such as HML  41, CTL 30, ACTL 32, etc.) to be defined in XTL.

  • PBG (Partitioned BCG Graph) is a file format implementing the theoretical concept of Partitioned LTS  37 and providing a unified access to a graph partitioned in fragments distributed over a set of remote machines, possibly located in different countries. The PBG format is supported by several tools, such as:
    • PBG  CP, PBG  MV, and PBG  RM, which facilitate standard operations (copying, moving, and removing) on PBG files, maintaining consistency during these operations,
    • PBG  MERGE (formerly known as BCG  MERGE), which transforms a distributed graph into a monolithic one represented in BCG format,
    • PBG  INFO, which displays various statistical information about a distributed graph.
  • The connection between explicit models (such as BCG graphs) and implicit models (explored on the fly) is ensured by OPEN/CAESAR-compliant compilers, e.g.:
    • BCG  OPEN, for models represented as BCG graphs,
    • CAESAR.OPEN, for models expressed as LOTOS descriptions,
    • EXP.OPEN, for models expressed as communicating automata,
    • FSP.OPEN, for models expressed as FSP  42 descriptions,
    • LNT.OPEN, for models expressed as LNT descriptions, and
    • SEQ.OPEN, for models represented as sets of execution traces.

  The CADP toolbox also includes TGV (Test Generation based on Verification), which has been developed by the VERIMAG laboratory (Grenoble) and Inria Rennes – Bretagne-Atlantique.

  The CADP tools are well-integrated and can be accessed easily using either the EUCALYPTUS graphical interface or the SVL  36 scripting language. Both EUCALYPTUS and SVL provide users with an easy and uniform access to the CADP tools by performing file format conversions automatically whenever needed and by supplying appropriate command-line options as the tools are invoked.

• URL:
  http://­cadp.­inria.­fr/
• Contact:
  Hubert Garavel
• Participants:
  Hubert Garavel, Frederic Lang, Radu Mateescu, Wendelin Serwe

5.1.2 TRAIAN

• Keywords:
  Compilation, LOTOS NT
• Functional Description:

  TRAIAN is a compiler for translating LOTOS NT descriptions into C programs, which will be used for simulation, rapid prototyping, verification, and testing.

  The current version of TRAIAN, which handles LOTOS NT types and functions only, has useful applications in compiler construction  35, being used in all recent compilers developed by CONVECS.

• URL:
  http://­convecs.­inria.­fr/­software/­traian/
• Contact:
  Hubert Garavel
• Participants:
  Hubert Garavel, Frederic Lang, Wendelin Serwe

6.1.1 LNT Specification Language

Participants: Hubert Garavel, Frédéric Lang, Wendelin Serwe.

LNT 529 is a next-generation formal description language for asynchronous concurrent systems. The design of LNT at CONVECS is the continuation of the efforts undertaken in the 80s to define sound languages for concurrency theory and, indeed, LNT is derived from the ISO standards LOTOS (1989) and E-LOTOS (2001). In a nutshell, LNT attempts to combine the best features of imperative programming languages, functional languages, and value-passing process calculi.

LNT is not a frozen language: its definition started in 2005, as part of an industrial project. Since 2010, LNT has been systematically used by CONVECS for numerous case studies (many of which being industrial applications — see § 6.5). LNT is also used as a back-end by other research teams who implement various languages by translation to LNT. It is taught in university courses, e.g., at University Grenoble Alpes and ENSIMAG, where it is positively accepted by students and industry engineers. Based on the feedback acquired by CONVECS, LNT is continuously improved.

In 2022, the LNT language has continued to evolve, mainly to become a better language and to achieve convergence with the LOTOS NT language supported by the TRAIAN compiler (see § 6.1.2):

• The syntax of natural numbers (binary, octal, hexadecimal) and floating-point numbers was brought closer to mainstream programming languages. The “while” and “for” loops were equipped with an optional label that can be used in “break” statements. Function calls were simplified by making the “eval” keyword optional, and output offers in synchronizations were simplified by forbidding the “!” symbol. Set types were equipped with a predefined operation “subset” checking for set inclusion, and the usage of the “{}” constructor was made clearer. The pragmas related to the translation of LNT types and functions in the C language were improved by enforcing the usage of valid C identifiers, and two new pragmas “!pointer” and “!nopointer” were introduced to indicate whether the designated LNT types are implemented as pointer types in C or not.
• The LNT2LOTOS Reference Manual and the LNT tools have been updated to document and implement these changes of LNT, and the CADP demo examples have been upgraded to the latest version of LNT. Four new CADP demo examples have been translated from LOTOS to LNT. The “upc” shell script was extended to ease the migration of LNT programs, in particular the over $15,000$ LNT examples used for non-regression testing of LNT2LOTOS. A new tool named LNT_MERGE was added, which transforms a (possibly multi-module) LNT program into a single-module LNT program (also merging the external C code, if any). This tool enables to package multi-module LNT programs into non-regression test suites.
• Also, in addition to seven bug fixes, the LNT2LOTOS compiler was enhanced in several manners. Various sanity checks on pragmas were added, as well as warnings regarding dead code and unsafe usage of process parameters in infinite loops. The generation of LOTOS code was improved to avoid warnings of GCC for certain exhaustive LNT patterns, and warnings about deprecated LNT syntactic features were enhanced with source-code line numbers.

6.1.2 LOTOS NT Specification Language

Participants: Hubert Garavel, Frédéric Lang, Wendelin Serwe.

We continued working on the TRAIAN compiler for the LOTOS NT language (a predecessor of LNT), which is used for the construction of most CADP compilers and translators. Since TRAIAN 3.0, the lexer and parser of TRAIAN are built using the SYNTAX compiler-generation system developed at Inria Paris and the abstract syntax tree of LOTOS NT, the library of predefined LOTOS NT types and functions, the static semantics checking (identifier binding, type checking, dataflow analysis, etc.), and the C code generation are implemented in LOTOS NT itself, so that TRAIAN is capable of bootstrapping itself.

In 2022, our efforts led to the release of three new major versions of TRAIAN, which introduce various changes to the LOTOS NT language in order to further align it with the LNT language supported by the CADP toolbox:

• TRAIAN 3.6 brings twenty-four language changes, mostly to extend the syntax of types, processes, expressions, and patterns (including their type-checking), as well as twelve library and code-generation changes that improve the predefined LOTOS NT libraries and the generated C code. Five bugs were fixed.
• TRAIAN 3.7 brings four language changes introducing array manipulation features and improving pragmas, four library changes notably simplifying exception handling, ten static-semantics changes, notably introducing dataflow analysis for processes, and five code-generation changes accomodating the new features. Nineteen bugs were fixed.
• TRAIAN 3.8 brings thirteen language changes that improve the handling of exceptions and function parameters, as well as the syntax of processes, synchronizations, and modules, nine static-semantics changes improving the type-checking of arrays, loops, and function parameters, two compiler changes to fine-tune the code generation, and six release changes for porting TRAIAN on 64-bit Windows and improving the demo examples. Six bugs were fixed.

In all versions of TRAIAN, the “traian_upc” conversion tool was extended to ease the upgrade of existing LOTOS NT source code whenever possible, and the user manual of TRAIAN, as well as the demo examples, were constantly updated.

6.1.3 Formal Modeling and Analysis of BPMN

Participants: Angel Contreras, Quentin Nivon, Gwen Salaün [correspondent], Ahang Zuo.

Business Process Model and Notation (BPMN) is a workflow-based notation that has been published as an ISO standard and has become the main language for business process modeling. However, specifying processes with BPMN is not an easy task for non-experts and this is still an issue to make BPMN widely used in any company around the world. Process mining techniques are helpful to automatically infer processes from execution logs, but this is not a solution to make users more at ease with BPMN. Also, optimizing a BPMN process is difficult, especially for non-expert users, due to the lack of design time support for BPMN.

In 2022, we considered the modeling and analysis of BPMN processes along three research directions:

• Semi-automation of BPMN modeling.
  In the context of the MOAP project (see § 8.5.1), in collaboration with Yliès Falcone (CORSE project-team), we continued the work on our approach for modelling business processes in a semi-automated way  33. The approach focuses on a timed version of BPMN, where each task is annotated with its minimum and maximum execution duration. The user starts by defining the tasks involved in the process, possibly indicating a partial order between some of these tasks. The approach proceeds in three steps: (i) generation of an abstract graph (simplified version of the process) from the task definitions; (ii) computation of the minimum and maximum time for executing the whole graph, followed by a manual refinement of the graph based on this information; (iii) synthesis of the final BPMN process from that graph. We implemented this approach in the WEASY lightweight modelling tool, which is available as an open-source Web application and led to a publication in an international conference 12.
• Debugging of BPMN Processes.
  Designing business processes using BPMN can be error-prone. Recent works have proposed verification techniques for analyzing processes and for detecting possible issues. In particular, model checking is an established technique for automatically verifying that a model (e.g., a BPMN process) satisfies a given temporal property. When the model does not satisfy a safety property, the model checker returns as counterexample a sequence of actions leading to a state where the property does not hold. Understanding this counterexample for debugging the BPMN process is not an easy task, especially if the counterexample is not expressed using the BPMN notation. To simplify the debugging, we propose an approach for transforming counterexamples back to the original BPMN process by means of coloring techniques. The approach, which involves three steps (matching analysis, unfolding, and folding), was fully automated using several tools in conjunction with CADP, and was validated on many examples. This work led to a publication in an international conference 22.
• Optimization of BPMN processes.

  Business process optimization is a strategic activity in organizations because of its potential to increase profit margins and reduce operational costs. One of the main challenges in this activity is concerned with the problem of optimizing allocation and sharing of resources. In collaboration with Francisco Durán (University of Málaga, Spain) and Camilo Rocha (Universidad Pontificia Javeriana, Cali, Colombia), we proposed two approaches in terms of moving from static to dynamic analysis and allocation of resources for BPMN processes. We considered the BPMN notation extended with an explicit description of execution time and resources associated with tasks, that can be concurrently executed multiple times. First, we proposed a simulation-based approach for computing certain metrics of interest, such as average execution time or resource usage. This approach applies off-line and is static in the sense that the number of resources does not evolve during simulation. Secondly, we proposed an alternative approach, which works online, thus requiring the instrumentation of an existing platform to retrieve relevant information during the execution of processes. This second approach is dynamic, because the number of resource replicas is updated during execution. We studied both approaches, stressing their advantages and drawbacks, and showing their complementarity. This work led to a publication in an international workshop 14.

  We also proposed another kind of optimization, which operates on the structure of a BPMN process involving time and resources. This optimization consists of a refactoring procedure whose final goal is to reduce the total execution time of the BPMN process given as input. This procedure relies on refactoring operations that reorganize the tasks in the process by taking into account the resources used by those tasks. This process refactoring technique was fully automated by the ROP tool that we implemented and applied on several examples for validation purposes. This work led to a publication in an international conference 15.

6.1.4 Other language developments

Participants: Hubert Garavel, Frédéric Lang, Wendelin Serwe.

In 2022, various compilers of CADP have been improved as follows:

• In addition to a bug fix in the X_BIT library, the CAESAR and CAESAR.ADT compilers for LOTOS have been enhanced to generate C code with less warnings from GCC and from the Sparse and Splint code checkers.
• All the CADP tools are now built using the latest version of the SYNTAX compiler generator and the most recent version of TRAIAN (see § 6.1.2). Also, the garbage collector invoked by CAESAR was upgraded from version 7.6.4 to version 8.2.2.

6.2.1 Counting Bugs in Behavioural Models using Counterexample Analysis

Participants: Irman Faqrizal, Gwen Salaün.

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking is an established technique for automatically finding bugs by verifying that a model (e.g., a Labelled Transition System obtained from a higher-level specification) satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is (for safety properties) a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification or program is a complicated task, because the counterexample gives only a partial view of the source of the problem, and because there is usually little support beyond that counterexample to identify the source of the problem.

In 2022, we proposed some techniques for simplifying the debugging of these models. These techniques first extract the part of the behavioural model that does not satisfy the given property. In that model, we then detect specific states (called faulty states) where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. Based on this model, we proposed some techniques to count the number of bugs in the original specification. The core idea of the approach is to change the specification for some specific actions that may cause the property violation, and compare the model before and after modification to detect whether this potential bug is real or not. This approach is fully automated by a tool we implemented and applied on several examples for validation purposes. This work led to a publication in an international conference 19.

6.2.2 Verification of Emergent Properties in Multi-agent Systems

Participants: Frédéric Lang, Luca Di Stefano.

Multi-agent systems are collections of autonomous components that interact with each other and with their shared environment. These systems may display collective properties that arise from the interplay between agents. Reasoning about these properties turns out to be hard, due to the very large state space that these systems usually exhibit. Therefore, automatic procedures to formally guarantee the emergence of such properties may prove helpful in the design of reliable artificial multi-agent systems.

In 2022, we adapted the existing translation procedure from LAbS specifications  47 to LNT programs, so that agents are now represented by networks of LNT processes combined using parallel composition operators, whereas the previous procedure emulated the concurrent execution of agents using only sequential operators (basically sequential composition and choice). This allowed us to apply compositional verification to verify properties on the generated LNT programs. We combined compositional verification with a static value analysis to prune the state space of individual agents and demonstrated the effectiveness of our approach by verifying a collection of representative systems. These results led to a paper, which has been accepted for publication in an international conference 13.

6.3.1 Probabilistic Analysis of Industrial IoT Applications

Participants: Irman Faqrizal, Gwen Salaün.

Industrial automation is a complex process involving various stakeholders. The international standard IEC 61499 helps to specify distributed automation using a generic architectural model, targeting the technical development of the automation. However, analysing the correctness of IEC 61499 models remains challenging because of their informal semantics and distributed logic.

In 2022, in the context of the DIIoT project (see § 8.5.2), in collaboration with Yliès Falcone (CORSE project-team), we introduced new verification techniques for IEC 61499 applications that combine a design-time analysis for computing a formal model of the application with a runtime analysis for extracting additional information during the execution. Firstly, at design time, all possible executions of the application are captured using a Labelled Transition System (LTS), obtained by translating the IEC 61499 application into an LNT specification and applying the LNT compilers of CADP. Next, the application is instrumented by inserting a monitor function block, which allows executing a monitored version of the verified system with the existing IEC 61499 runtime environments. Then, the LTS model is enriched with probabilistic values computed from the execution traces collected by the monitor. Finally, the probabilistic version of the EVALUATOR model checker is used to verify certain requirements of the application, described as probabilistic temporal logic properties. The approach is automated using several tools and was validated on a realistic IEC 61499 application. This work led to a publication in an international conference 18.

6.3.2 Probabilistic Model Checking of BPMN Processes

Participants: Gwen Salaün, Ahang Zuo.

Business Process Model and Notation (BPMN) is a standard business process modelling language that allows users to describe a set of structured tasks, which results in a service or product. Before running a BPMN process, the user often has no clear idea of the probability of executing some task or specific combination of tasks. This is, however, of prime importance for adjusting resources associated with tasks and thus optimizing costs.

In 2022, in the context of the MOAP project (see § 8.5.1), in collaboration with Yliès Falcone (CORSE project-team), we defined an approach to perform probabilistic model checking of BPMN models at runtime. Our approach consists of three steps: (i) transformation of the BPMN model into a Labelled Transition System (LTS) by translating the BPMN model into an LNT specification and applying the LNT compilers of CADP; (ii) conversion of the LTS into a Probabilistic Transition System (PTS) by running multiple instances of the process and analyzing the execution traces; (iii) probabilistic model checking for verifying that the PTS model satisfies a given probabilistic property. The steps (ii) and (iii) are applied periodically to update the results according to the execution of the process instances. The overall approach was implemented in a tool chain, which was applied successfully to several realistic BPMN processes. This work led to a publication in an international conference 18.

6.4.1 Compositional Verification

Participants: Frédéric Lang, Luca Di Stefano.

The CADP toolbox contains various tools dedicated to compositional verification, among which EXP.OPEN, BCG_MIN, BCG_CMP, and SVL play a central role. EXP.OPEN explores on the fly the graph corresponding to a network of communicating automata (represented as a set of BCG files). BCG_MIN and BCG_CMP respectively minimize and compare behavior graphs modulo strong or branching bisimulation and their stochastic extensions. SVL (Script Verification Language) is both a high-level language for expressing complex verification scenarios and a compiler dedicated to this language.

In 2022, we published a research report  25, where:

• We describe the signature-based algorithm implemented in BCG_MIN and BCG_CMP to compute equivalence with respect to sharp bisimulation.
• We show that, under some conditions on strong actions, sharp bisimulation equivalence is a congruence for the priority operator implemented in EXP.OPEN. This makes sharp bisimulation appropriate to verify priority systems compositionally.
• We compare sharp bisimulation with orthogonal bisimulation  28, whose equivalence is also a congruence for priority. We show that compositional minimization using sharp bisimulation may yield LTSs that are several orders of magnitude smaller than using orthogonal bisimulation.

These results have also been submitted to an international journal.

6.4.2 On-the-fly Resolution of Boolean Equation Systems

Participants: Radu Mateescu.

OPEN/CAESAR is an extensible, modular, language-independent software framework for exploring implicit graphs (i.e., defined by their post function, which enumerates the transitions going out of each vertex). This key component of CADP is used to build simulation, execution, verification, and test generation tools.

CAESAR_SOLVE_1 is a generic software library, based on OPEN/CAESAR, for solving Boolean equation systems of alternation depth 1 (i.e., without mutual recursion between minimal and maximal fixed point equations) on the fly. This library is at the core of several CADP verification tools, namely the equivalence checker BISIMULATOR, the minimization tool REDUCTOR, and the model checker EVALUATOR. The resolution method is based on boolean graphs, which provide an intuitive representation of dependencies between boolean variables, and which are handled implicitly, in a way similar to the OPEN/CAESAR interface  38.

In 2022, we enhanced the CAESAR_SOLVE_1 library with two new on-the-fly resolution algorithms, named A10 and A11. These algorithms are based on a nested depth-first search (DFS) of the dependency graph between boolean variables, similar to the algorithms used for detecting accepting cycles in Büchi automata  31. Algorithm A10 (resp. A11) is specialized for solving disjunctive (resp. conjunctive) equation blocks of minimal (resp. maximal) fixed point sign, in the case where a single invocation of the algorithm is requested on the block. Algorithms A10 and A11 consume less memory then their counterparts A3 and A4, which are based on a DFS traversal with computation of strongly connected components and allow multiple invocations on the same equation block. The CAESAR_SOLVE_1 manual page, the OPEN/CAESAR Reference Manual, and the BES_SOLVE tool were updated to take into account the two new algorithms.

6.4.3 Runtime Enforcement for IEC 61499 Applications

Participants: Irman Faqrizal, Gwen Salaün.

The ever-increasing demands from stakeholders in the industry for frameworks that can help maximizing the efficiency and productivity encourage innovations in industrial automation. As a result, the international standard IEC 61499 was proposed by researchers in this domain. The standard has been gaining popularity in the past few years particularly because of its distributed paradigm and vendor independent format. The technicality of IEC 61499, such as its syntax, is well-defined; however, it comes only with informal semantics described using natural language. In this regard, the verification is not straightforward, while it is known that the correctness of high-stakes industrial systems is crucial.

In 2022, in the context of the DIIoT project (see § 8.5.2), in collaboration with Yliès Falcone (CORSE project-team), we proposed new verification techniques for IEC 61499 applications. These techniques rely on the concept of runtime enforcement, which can be applied to systems for preventing bad behaviours from happening. The main idea of our approach is to integrate an enforcer in the application for allowing it to respect specific properties when executing. The techniques begin with the definition of a property. The language of this property supports features such as discarding and replacing events. Next, this property is used to synthesize an enforcer in the form of a function block. Finally, the synthesized enforcer is integrated into the application. Our approach was validated on a realistic example and fully automated. This work led to a publication in an international conference 17.

6.4.4 Other Component Developments

Participants: Hubert Garavel, Frédéric Lang, Wendelin Serwe.

In 2022, several components of CADP have been improved as follows:

• Besides a bug fix in the BCG_READ manual page, the vocabulary and option names concerning divergence-preserving branching bisimulation and sharp bisimulation in BCG_CMP, BCG_MIN, and SVL were clarified.
• The CAESAR.BDD tool was upgraded to version 3.1.0 of the CUDD library, and extended with four new options: “-arcs-pt”, “-arcs-tp”, “-signature”, and “-signature-multiple” (the two latter options display a NUPN checksum that is invariant by any permutation of places, transitions, and/or units). The existing options “-place-order” and “-unit-order” were enhanced to be faster and produce shorter, yet more discriminative results, and the “-concurrent-places” option was made faster.
• The ergonomy of CADP was enhanced by pre-selecting the MAIN process of LNT files in the EUCALYPTUS graphical user interface (thereby saving user clicks). Also, the style files for GNOME text editors (Gedit, Pluma, etc.) were upgraded to Gtk5, and new style files for the Sublime Text editor have been added for the various languages and file formats supported by CADP.
• In addition to six bug fixes, the CADP tools received specific enhancements targeted to various processors and operating systems. CADP was ported to macOS 13 “Ventura”, and was adapted to support Apple machines with an ARM processor. Support for the 32-bit executables on Solaris and OpenIndiana has been discontinued, since the 64-bit executables are deemed to be sufficient. The installation and usage of CADP on Windows/Cygwin were simplified, and preliminary changes to support 64-bit Windows executables have been undertaken.

6.5.1 Autonomous Car

Participants: Jean-Baptiste Horel, Radu Mateescu [correspondent], Philippe Ledent, Lucie Muller, Wendelin Serwe.

A common practice to evaluate autonomous vehicles is simulation, which requires to specify realistic scenarios, in particular critical ones, occurring rarely and potentially dangerous to reproduce on the road. Such scenarios may be either generated randomly, or specified manually. Randomly generating scenarios is easy, but their relevance might be difficult to assess. Manually specified scenarios can focus on a given feature, but their design might be difficult and time-consuming, especially to achieve satisfactory coverage.

In the framework of the ArchitectECA2030 (see § 8.3.1) and PRISSMA (see § 8.4.1) projects and in collaboration with Lina Marsso (University of Toronto, Canada), Christian Laugier, Anshul Paigwar, and Alessandro Renzaglia (CHROMA project-team), we proposed an automatic approach to generate a large number of relevant critical scenarios for autonomous driving simulators. The approach relies on the generation of behavioral conformance tests using the TESTOR tool  43, from an LNT model (specifying the ground truth configuration with the range of vehicle behaviors) and a test purpose (specifying the critical feature under analysis). The obtained test cases (which cover all possible executions exercising a given feature) are automatically translated into the inputs of autonomous driving simulators. Using this approach, we generated thousands of behavior trees for the CARLA simulator for several realistic configurations. This work led to a publication in an international conference 20.

In 2022, we finalized the LNT model describing the scene configuration and the behaviour of the actors (autonomous car and mobile obstacles), and compared it with a previous model focused on the decision component of the car. The two models were made publicly available and led to a publication in an international workshop 21. We also extended our scenario generation approach by executing the scenarios in the CARLA simulator to produce execution traces, which we analyzed using a combination of model checking and statistical analysis to assess the collision-risk estimation of the perception component equipping the autonomous car. This work led to an article accepted for publication in an international journal.

In the context of the ArchitectECA2030 project, we considered a thermal controller for a high-voltage car battery. Based on an informal specification using four mode automata and a list of requirements, both provided by AVL, we developed a formal model in LNT (about 1000 lines) and expressed the relevant requirements as 26 MCL formulas. This formalization discovered several small issues, such as inconsistent naming of variables, mix between temperature units (Kelvin and Celsius), and nondeterministic behavior. After ensuring that the LNT model satisfies all requirements, we started investigating the use of the model for runtime monitoring of the thermal controller, by taking real simulation traces provided by AVL and checking whether an appropriate abstraction of these traces (rounding the floating-point temperature values to the discrete intervals considered in the model) is included in the model, enabling to distinguish between correct and faulty traces.

Still within the ArchitectECA2030 project, we also considered a combined hardware/software aging monitor, provided by NXP (hardware part) and DATASOFT (software part). We started the development of a formal LNT model, based on the initial descriptions provided by our partners, illustrating the feasibility of the modelling and validation approach.

7.2.1 Nokia Bell Labs

Participants: Gwen Salaün [correspondent].

The collaboration with Nokia Bell Labs (Nozay) in the framework of the ADR Sapiens, started in 2017, ended in 2022. The CONVECS project-team was involved in the formal modeling and analysis of IoT applications. The latest results of the collaboration are presented in two publications in international journals 10, 11.

7.2.2 ST Microelectronics

Participants: Philippe Ledent, Radu Mateescu [correspondent], Wendelin Serwe.

Ph. Ledent is supported by a CIFRE PhD grant (from October 2020 to September 2023) from ST Microelectronics (Grenoble) on the formal validation of security requirements for Systems-on-Chip, under the supervision of Hajer Ferjani (ST Microelectronics), Radu Mateescu (CONVECS), and Wendelin Serwe (CONVECS).

8.1.1 Other international collaborations

In 2022, we had scientific relations with several universities and institutes abroad, including:

• University of Málaga, Spain (Francisco Durán),
• Saarland University, Germany (Holger Hermanns),
• University of Cali, Colombia (Camilo Rocha),
• University of Toronto, Canada (Lina Marsso),
• Chalmers University, Sweden (Luca Di Stefano).

8.2.1 Visits of international scientists

• Francisco Durán (University of Málaga, Spain) visited us from May 4 to May 6, 2022. He participated at the workshop on formal modelling, analysis, and optimization of BPMN processes organized by G. Salaün at Inria Grenoble on May 4, 2022. He gave a seminar entitled “Machine Learning for the Dynamic Provisioning of Resources”.

8.2.2 Visits to international teams

8.3.1 H2020 projects

8.3.2 Other european programs/initiatives

The CONVECS project-team is member of the FMICS (Formal Methods for Industrial Critical Systems) working group of ERCIM. H. Garavel and R. Mateescu are members of the FMICS board, H. Garavel being in charge of dissemination actions.

8.4.1 Fonds pour l'innovation et l'industrie

8.4.2 Other national collaborations

We had sustained scientific relations with the following researchers:

• Fabrice Kordon and Lom Messan Hillah (LIP6, Paris),
• Nicolas Amat and Silvano Dal Zilio (LAAS-CNRS, Toulouse),
• Michel Le Pallec (Nokia Bell Labs).

8.5.1 Pack ambition recherche région Auvergne-Rhône-Alpes

8.5.2 Persyval labex

9.1.1 Scientific events: organisation

9.1.2 Scientific events: selection

9.1.3 Journal

9.1.4 Software dissemination and Internet visibility

The CONVECS project-team distributes several software tools, among which the CADP toolbox.

In 2022, the main facts are the following:

• We prepared and distributed twelve successive versions (2022-a to 2022-l) of CADP.
• We granted CADP licenses for 208 different computers in the world.

The CONVECS Web site was updated with scientific contents, announcements, publications, etc.

By the end of December 2022, the CADP forum, opened in 2007 for discussions regarding the CADP toolbox, had over 470 registered users and over 1972 messages had been exchanged.

Also, for the 2022 edition of the Model Checking Contest, we provided 3 families of models (totalling 60 Nested-Unit Petri Nets) derived from our LNT models.

Other research teams took advantage of the software components provided by CADP (e.g., the BCG and OPEN/CAESAR environments) to build their own research software. We can mention the following developments:

• Kong verification tool for Petri nets  27
• Tomte tool for learning automata  48
• Alvis verification tool for concurrent systems  49

Other teams also used the CADP toolbox for various case studies:

• 4SECURail case study on train handover protocols  46, 45
• Integration of ubiquitous specifications in object systems design  26

9.1.5 Invited talks

• I. Faqrizal gave a talk entitled “Runtime Enforcement for IEC 61499 Applications” at the 3rd meeting of the YODA working group of the GDR GPL, held virtually on December 16, 2022.
• Q. Nivon gave a talk entitled “Debugging of BPMN Processes using Coloring Technique” at the 3rd YODA meeting, held virtually on December 16, 2022.
• G. Salaün gave a keynote talk entitled “Modelling and Quantitative Analysis of BPMN Processes using Maude” at the 14th International Workshop on Rewriting Logic and its Applications (WRLA'2022), Munich, Germany on April 2-3, 2022.
• G. Salaün gave an invited talk entitled “Modelling, Analysis and Optimization of BPMN Processes” at the Journées du GDR GPL, Vannes on June 7-10, 2022.
• G. Salaün gave an invited talk entitled “Modelling, Analysis and Optimization of BPMN Processes” at the 17th International Summer School on Training And Research On Testing (TAROT'2022), Avila, Spain on July 5-8, 2022.
• G. Salaün gave an invited talk entitled “Models and Verification for Composition and Reconfiguration of Web of Things Applications” at the 1st French-German Workshop SeReCo, Lyon on May 23-24, 2022.

9.1.6 Research administration

• F. Lang is chair of the “Commission du développement technologique”, which is in charge of selecting R&D projects for Inria Grenoble, and giving an advice on the recruitment of temporary engineers.
• R. Mateescu is the scientific correspondent of the International Partnerships for Inria Grenoble.
• R. Mateescu is a member of the “Comité d'Orientation Scientifique” for Inria Grenoble. In 2022, he also participated to the recruitment jury for CRCN (Chargé de Recherche de Classe Normale) and ISFP (Inria Starting Faculty Positions) at Inria Grenoble.
• R. Mateescu is representative of Inria Grenoble at the International Relations and Outreach of Université Grenoble Alpes (UGA).
• R. Mateescu is member of the council of the Mathematics, Information and Communication Sciences (MSTIC) research department of UGA.
• G. Salaün is a member of the administration council of the IUT1/UGA.
• G. Salaün is the head of the Métiers du Multimédia et de l'Internet (MMI) department at IUT1/UGA since September 2022.
• G. Salaün is a member of the Scientific Committee of the PCS (Pervasive Computing Systems) action of the PERSYVAL Labex.
• G. Salaün is a member of the council of the LIG laboratory.
• W. Serwe is correspondent in charge of the 2022 Inria activity reports at Inria Grenoble.
• W. Serwe is a member of the “Comité de Centre” at Inria Grenoble.

9.2.1 Teaching

CONVECS is a host team for the computer science master MOSIG (Master of Science in Informatics at Grenoble), common to Grenoble INP and UGA.

In 2022, we carried out the following teaching activities:

• I. Faqrizal gave a course on “Introduction to Node.js” (32 hours “équivalent TD”) to L3 students of IUT1/UGA.
• F. Gallay taught a course on “Langages et automates” (27 hours “équivalent TD”) to L2 (Licence MIN) students of UGA.
• H. Garavel participated to a course on “Embedded Systems: From High-Confidence Design to Safe Execution” (12 hours “équivalent TD” on probabilistic/stochastic models and fault trees) to second year students of the MOSIG.
• F. Lang gave a course on “Formal Software Development Methods” (7.5 hours “équivalent TD”) in the framework of the “Software Engineering” lecture given to 1st year students of the MOSIG.
• F. Lang and R. Mateescu gave a lecture on “Modeling and Analysis of Concurrent Systems: Models and Languages for Model Checking” (27 hours “équivalent TD”) to 3rd year students of ENSIMAG and second year students of the MOSIG.
• L. Muller gave a course on “Système et environnement de programmation” (32 hours “équivalent TD”) to L1 students of UGA.
• G. Salaün taught about 240 hours of classes (algorithmics, Web development, object-oriented programming) at the MMI department of IUT1/UGA. He is also headmaster of the “Services Mobiles et Interface Nomade” (SMIN) professional licence (third year of university) at IUT1/UGA, and co-headmaster of the “alternance” (apprenticeship) at the MMI department.
• W. Serwe supervised a group of six teams in the context of the “projet Génie Logiciel” (55 hours “équivalent TD”, consisting in 13.5 hours of lectures, plus supervision and evaluation), ENSIMAG, January 2022.
• A. Zuo gave a course on “Introduction to Java/Android programming” (30 hours “équivalent TD”) to L2 students of IUT1/UGA during the spring 2022.
• A. Zuo gave a course on “Data Extraction” (21 hours “équivalent TD”) to L3 (Licence Pro) students of IUT2/UGA during the winter 2022.

9.2.2 Supervision

• PhD in progress: P. Bouvier, “Implémentation et vérification des langages concurrents de nouvelle génération”, Université Grenoble Alpes, since October 2019, H. Garavel and R. Mateescu
• PhD in progress: I. Faqrizal, “Monitoring and Deployment of IIoT Applications”, Université Grenoble Alpes, since October 2021, G. Salaün and Yliès Falcone
• PhD in progress: F. Gallay, “Decentralized Runtime Enforcement of Timed Properties”, Université Grenoble Alpes, since October 2022, R. Mateescu and Y. Falcone
• PhD in progress: J-B. Horel, “Validation des composants de perception basés sur l'IA dans les véhicules autonomes”, Université Grenoble Alpes, since April 2021, R. Mateescu, Alessandro Renzaglia, and Christian Laugier
• PhD in progress: P. Ledent, “Formal Validation of Security Requirements for a System-on-Chip Architecture”, Université Grenoble Alpes, since October 2020, R. Mateescu, W. Serwe, and Hajer Ferjani
• PhD in progress: L. Muller, “Formal Modelling and Validation for Electric, Connected, and Automated Vehicles”, Université Grenoble Alpes, since September 2020, R. Mateescu and W. Serwe
• PhD in progress: Q. Nivon, “Analyse, optimisation et debugging de processus BPMN”, Université Grenoble Alpes, since October 2022, G. Salaün
• PhD in progress: Choukri Soueidi, “Instrumentation expressive et correcte de programmes distribués et vérification à l’exécution”, Université Grenoble Alpes, since October 2020, G. Salaün and Y. Falcone
• PhD in progress: A. Zuo, “Modelling, Optimization and Predictive Analysis of Business Processes”, Université Grenoble Alpes, since October 2020, G. Salaün and Y. Falcone

9.2.3 Juries

• R. Mateescu was reviewer of Soren Enevoldsen's PhD thesis, entitled “Abstract Dependency Graphs for Model Verification”, defended at University of Aalborg (Denmark) on December 15, 2022.
• G. Salaün was reviewer of Abdul Majith Noordheen's PhD thesis, entitled “Automated Verification and Synthesis of Distributed Systems”, defended at Université de Rennes on June 7, 2022.

International journals

• 9 articleL.Luca Di Stefano, R.Rocco de Nicola and O.Omar Inverso. Verification of Distributed Systems via Sequential Emulation.ACM Transactions on Software Engineering and Methodology3132022, 1-41
  HALDOI
• 10 articleF.Francisco Durán, A.Ajay Krishna, M.Michel Le Pallec, R.Radu Mateescu and G.Gwen Salaün. Models and analysis for user-driven reconfiguration of rule-based IoT applications.Internet of Things19August 2022, 100515
  HALDOIback to text
• 11 articleA.Ajay Krishna, M.Michel Le Pallec, R.Radu Mateescu and G.Gwen Salaün. Design and Deployment of Expressive and Correct Web of Things Applications.ACM Transactions on Internet of Things3February 2022, 1 - 30
  HALDOIback to text

International peer-reviewed conferences

• 12 inproceedingsA.Angel Contreras, Y.Yliès Falcone, G.Gwen Salaün and A.Ahang Zuo. WEASY: A Tool for Modelling Optimised BPMN Processes.FACS 2022 - 18th International Conference on Formal Aspects of Component SoftwareOslo / Online, NorwayNovember 2022
  HALDOIback to text
• 13 inproceedingsL.Luca Di Stefano and F.Frederic Lang. Compositional Verification of Stigmergic Collective Systems.24th International Conference on Verification, Model Checking , and Abstract Interpretation (VMCAI'2023)Boston, United StatesJanuary 2023
  HALback to text
• 14 inproceedingsF.Francisco Durán, Y.Yliès Falcone, C.Camilo Rocha, G.Gwen Salaün and A.Ahang Zuo. From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes.WRLA 2022 - 14th International Workshop on Rewriting Logic and its ApplicationsMunich, GermanyApril 2022, 1-18
  HALDOIback to text
• 15 inproceedingsF.Francisco Durán and G.Gwen Salaün. Optimization of BPMN Processes via Automated Refactoring.ICSOC 2022 - 20th International Conference on Service-Oriented ComputingSevilla, SpainNovember 2022, 1-15
  HALDOIback to text
• 16 inproceedingsY.Yliès Falcone, I.Irman Faqrizal and G.Gwen Salaün. Probabilistic Analysis of Industrial IoT Applications.IoT 2022 -The 12th International Conference on the Internet of ThingsDelft, NetherlandsNovember 2022
  HAL
• 17 inproceedingsY.Yliès Falcone, I.Irman Faqrizal and G.Gwen Salaün. Runtime Enforcement for IEC 61499 Applications.SEFM 2022 - 20th International Conference on Software Engineering and Formal MethodsBerlin, GermanySeptember 2022, 1-17
  HALDOIback to text
• 18 inproceedingsY.Yliès Falcone, G.Gwen Salaün and A.Ahang Zuo. Probabilistic Model Checking of BPMN Processes at Runtime.iFM 2022 - International Conference on integrated Formal MethodsLugano, SwitzerlandJune 2022, 1-17
  HALDOIback to textback to text
• 19 inproceedingsI.Irman Faqrizal and G.Gwen Salaün. Counting Bugs in Behavioural Models using Counterexample Analysis.FormaliSE 2022 - International Conference on Formal Methods in Software EngineeringPittsburgh, United StatesMay 2022, 1-11
  HALDOIback to text
• 20 inproceedingsJ.-B.Jean-Baptiste Horel, C.Christian Laugier, L.Lina Marsso, R.Radu Mateescu, L.Lucie Muller, A.Anshul Paigwar, A.Alessandro Renzaglia and W.Wendelin Serwe. Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles.DATE/ASD 2022 - Design, Automation and Test in Europe - Autonomous Systems DesignAntwerp, BelgiumIEEEMarch 2022, 532-537
  HALDOIback to text
• 21 inproceedingsL.Lina Marsso, R.Radu Mateescu, L.Lucie Muller and W.Wendelin Serwe. Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing.Mars 2022 - 5th Workshop on Models for Formal Analysis of Real Systems355Electronic Proceedings in Theoretical Computer ScienceMunich, GermanyMarch 2022, 60-117
  HALDOIback to text
• 22 inproceedingsQ.Quentin Nivon and G.Gwen Salaün. Debugging of BPMN Processes Using Coloring Techniques.Lecture Notes in Computer ScienceFACS 2022 - 18th International Conference on Formal Aspects of Component SoftwareLNCS-13712Formal Aspects of Component SoftwareOslo / Virtual, NorwaySpringer International PublishingNovember 2022, 90-109
  HALDOIback to text
• 23 inproceedingsG.Gwen Salaün. Quantifying the Similarity of BPMN Processes.APSEC 2022 - 29th Asia-Pacific Software Engineering ConferenceVirtual, JapanDecember 2022, 1-10
  HAL

Scientific book chapters

• 24 inbookH.Hubert Garavel and F.Frédéric Lang. Equivalence Checking 40 Years After: A Review of Bisimulation Tools.13560A Journey from Process Algebra via Timed Automata to Model LearningLecture Notes in Computer ScienceSpringer Nature Switzerland; Springer Nature SwitzerlandSeptember 2022, 213-265
  HALDOI

Reports & preprints

• 25 reportL.Luca Di Stefano and F.Frédéric Lang. Compositional Verification of Priority Systems using Sharp Bisimulation.INRIAApril 2022, 1-32
  HALback to text