Section: Dissemination

Promoting Scientific Activities

Scientific events organisation

Member of the organizing committees

• H. Garavel is a member of the model board of MCC'2015 (Model Checking Contest). In 2015, he verified the forms describing the benchmark models and enhanced the format of these forms by adding new model properties. He contributed to the formalization of the contest's rules and to the writing of the two contest calls (call for models and call for tools). He also participated in migrating the PetriWeb model base (developed at the Technical University of Eindhoven) to the format and conventions of the contest. A journal article describing the achievements of the 5th Model Checking Contest has been written and submitted for publication.

• G. Salaün was a member of the organizing committee of SEFM'2015 (13th International Conference on Software Engineering and Formal Methods), York, United Kingdom, September 7–11, 2015.

Scientific events selection

Chair of conference program committees

• G. Salaün was programme committee co-chair of SVT-SAC'2015 (the Software Verification Track of the Symposium on Applied Computing), Salamanca, Spain, April 13–17, 2015.

Member of the conference program committees

• H. Garavel was program committee member of TACAS'2015 (21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems), London, United Kingdom, April 11–19, 2015.

• G. Salaün and W. Serwe were program committee members of FSEN'2015 (6th International Conference on Fundamentals of Software Engineering), Tehran, Iran, April 22–24, 2015.

• H. Garavel was program committee member of DCDS'2015 (5th International Workshop on Dependable Control of Discrete Systems), Cancun, Mexico, May 27–29, 2015.

• G. Salaün was program committee member of ICE'2015 (8th Interaction and Concurrency Experience), Grenoble, France, June 4-5, 2015.

• F. Lang, R. Mateescu, and W. Serwe were program committee members of FMICS'2015 (20th International Workshop on Formal Methods for Industrial Critical Systems), Oslo, Norway, June 22–23, 2015.

• G. Salaün was program committee member of WWV'2015 (11th International Workshop on Automated Specification and Verification of Web Systems), Oslo, Norway, June 23, 2015.

• F. Lang was program committee member of ETR'2015 (École d'été Temps Réel), Rennes, France, August 24–28, 2015.

• H. Garavel and G. Salaün were program committee members of SEFM'2015 (13th International Conference on Software Engineering and Formal Methods), York, United Kingdom, September 7–11, 2015.

• G. Salaün was program committee member of SCART'2015 (1st International Workshop on the ART of Software Composition), York, United Kingdom, September 8, 2015.

• G. Salaün was program committee member of FACS'2015 (12th International conference on Formal Aspects of Component Software), Rio de Janeiro, Brazil, October 14–16, 2015.

• H. Garavel was program committee member of MARS'2015 (Workshop on Models for Formal Analysis of Real Systems), Suva, Fiji, November 23, 2015.

Reviewer

• H. Garavel was a reviewer for CONCUR'2015 (26th Conference on Concurrency Theory), Madrid, Spain, September 1–4, 2015.

• R. Mateescu was a reviewer for FORTE'2015 (35th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems), Grenoble, France, June 2–5, 2015.

• G. Salaün was a reviewer for SOCA'2015 (8th IEEE International Conference on Service Oriented Computing and Applications), Rome, Italy, October 19–21, 2015.

• W. Serwe was a reviewer for ATVA'2015 (13th International Symposium on Automated Technology for Verification and Analysis, October 12–15, 2015, Shanghai, China), MARS'2015, and TACAS'2016.

Journal

Member of the editorial boards

• H. Garavel is an editorial board member of STTT (Springer International Journal on Software Tools for Technology Transfer).

• G. Salaün is an editorial board member of SOCA (Springer International Journal on Service Oriented Computing and Applications).

Reviewer - Reviewing activities

• H. Garavel was a reviewer for the Mathematical Reviews (MathSciNet) of the American Mathematical Society.

• F. Lang was a reviewer for SOSYM (International Journal on Software and Systems Modeling).

• R. Mateescu was a reviewer for JISA (Journal of Internet Services and Applications), IEEE TSE (Transactions on Software Engineering), JLAMP (Journal of Logical and Algebraic Methods in Programming), FAoC (Formal Aspects of Computing), and STTT.

• G. Salaün was a reviewer for FAoC, JLAMP, JSS (Journal of Systems and Software), and MPE (Mathematical Problems in Engineering).

Software Dissemination and Internet Visibility

The CONVECS project-team distributes several software tools: the CADP toolbox (see §  6.1 ), the TRAIAN compiler, the PIC2LNT translator, and the PMC model checker (see §  6.2 ).

In 2015, the main facts are the following:

• We prepared and distributed twelve successive versions (2015-a to 2015-l) of CADP.

• We were requested to grant CADP licenses for 434 different computers in the world.

The CONVECS Web site (http://convecs.inria.fr ) was updated with scientific contents, announcements, publications, etc. Following a request from the computer staff of Inria Grenoble, we worked on the migration of the former Web site “http://www.inrialpes.fr/vasy ” to a more recent web infrastructure. This former site was split into three new, distinct Web sites “http://vasy.inria.fr ”, “http://cadp.inria.fr ”, and “http://fmics.inria.fr ”. Dedicated effort was made to properly redirect all former URLs so as not to create dead links.

By the end of December 2015, the CADP forum (http://cadp.inria.fr/forum.html ), opened in 2007 for discussions regarding the CADP toolbox, had over 350 registered users and over 1600 messages had been exchanged.

Also, for the 2015 edition of the Model Checking Contest, we provided two families of models (totalling 15 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:

• The Ocarina tool for analysing AADL descriptions  [58]

• The MIstRAL tool for middleware reconfiguration based on formal methods  [61]

• The DFTCalc tool for analysing dynamic fault trees  [49]

• The Vercors integrated environment for verifying and running distributed components  [52]

• The IMCReo tool for Interactive Markov Chains in Stochastic Reo  [60]

• The GROOVE tool for verification based on graph rewriting  [54]

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

• Improving design patterns finder precision using model checking  [34]

• Applying automata learning to embedded control software  [62]

• Testing autonomous systems using communicating extended finite-state machines  [32]

• Assisting refinement in system-on-chip design  [59]

• Formal verification of plastic user interfaces exploiting domain ontologies  [37]

• Action-based verification of a fire alarm system  [35]

Awards and Distinctions

H. Garavel is an invited professor at Saarland University (Germany) as a holder of the Gay-Lussac Humboldt Prize.

Invited talks

• G. Salaün gave a talk entitled “Reliable Deployment, Reconfiguration, and Control of Cloud Applications” on February 12, 2015 at the University of Málaga, Spain.

• H. Garavel gave a talk entitled “Nested-Unit Petri Nets: A Useful Concept for PseuCo?” on March 9, 2015 at Saarland University, Saarbrücken, Germany.

• W. Serwe gave a talk entitled “Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip” on March 19, 2015 at the Cadence Club Formal, Grenoble, France.

• R. Mateescu gave a talk entitled “Overview of MCL, a Data-Based Model Checking Language” on March 31, 2015 at Inria Grenoble — Rhône-Alpes, Montbonnot, France.

• G. Salaün gave a talk entitled “Reliable Deployment, Reconfiguration, and Control of Cloud Applications” on March 26, 2015 at LIRMM, Montpellier, France.

• G. Salaün gave a talk entitled “Reliable Deployment, Reconfiguration, and Control of Cloud Applications” on April 2, 2015 at LABRI, Bordeaux, France.

• G. Salaün gave a talk entitled “Verification of Asynchronously Communicating Systems” on April 9, 2015 at IRISA, Rennes, France.

• H. Garavel gave a talk entitled “Nested-Unit Petri Nets: Combining Hierarchy with Concurrency” on May 6, 2015 at LIP6, Université Pierre et Marie Curie, Paris, France.

• G. Salaün gave a talk entitled “Formal Modelling and Analysis of BPMN Processes” on July 9, 2015 at XEROX, Meylan, France.

• F. Lang gave two talks entitled “Vérification de systèmes concurrents asynchrones par des méthodes compositionnelles” and “CADP : une boîte à outils pour la construction et l'analyse de processus distribués” on August 25, 2015 at ETR (Ecole d'Été Temps Réel), Rennes, France. He also held a lab session on CADP.

• G. Salaün gave a talk entitled “Formal Modelling and Analysis of BPMN Processes” on October 27, 2015 at the University of Málaga, Spain.

• H. Garavel gave a talk entitled “Les aspects probabilistes dans CADP” on December 8, 2015 at the “Journées Inria” held at LIP6, Université Pierre et Marie Curie, Paris, France.