Publications HAL de la structure 178330;1042444;1043323

2024

Conference papers

titre
Probabilistic Runtime Enforcement of Executable BPMN Processes
auteur
Yliès Falcone, Gwen Salaün, Ahang Zuo
article
FASE 2024 - 27th International Conference on Fundamental Approaches to Software Engineering, Apr 2024, Luxembourg City, Luxembourg. pp.1-21, ⟨10.1007/978-3-031-57259-3_3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04533195/file/Probabilistic%20Runtime%20Enforcement%20of%20Executable%20BPMN%20Processes.pdf BibTex
titre
Probabilistic Model Checking for IEC 61499: A Manufacturing Application
auteur
Irman Faqrizal, Tatiana Liakh, Midhun Xavier, Gwen Salaün, Valeriy Vyatkin
article
ICIT 2024 - 25th IEEE International Conference on Industrial Technology, IEEE, Mar 2024, Bristol, United Kingdom. pp.1-6
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04533520/file/final.pdf BibTex

2023

Journal articles

titre
A Toolchain to Compute Concurrent Places of Petri Nets
auteur
Nicolas Amat, Pierre Bouvier, Hubert Garavel
article
LNCS Transactions on Petri Nets and Other Models of Concurrency, 2023, Lecture Notes in Computer Science, 14150, pp.1-26. ⟨10.1007/978-3-662-68191-6_1⟩
Accès au bibtex
BibTex
titre
Compositional verification of priority systems using sharp bisimulation
auteur
Luca Di Stefano, Frédéric Lang
article
Formal Methods in System Design, 2023, ⟨10.1007/s10703-023-00422-1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04103681/file/DiStefano-Lang-23.pdf BibTex
titre
Verifying Collision Risk Estimation using Autonomous Driving Scenarios Derived from a Formal Model
auteur
Jean-Baptiste Horel, Philippe Ledent, Lina Marsso, Lucie Muller, Christian Laugier, Radu Mateescu, Anshul Paigwar, Alessandro Renzaglia, Wendelin Serwe
article
Journal of Intelligent and Robotic Systems, 2023, 107 (4), pp.1-45. ⟨10.1007/s10846-023-01808-3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04138579/file/jirs_2023.pdf BibTex

Conference papers

titre
Refactoring of Multi-instance BPMN Processes with Time and Resources
auteur
Quentin Nivon, Gwen Salaün
article
SEFM 2023 - International Conference on Software Engineering and Formal Methods, Nov 2023, Eindhoven, Netherlands. pp.226-245, ⟨10.1007/978-3-031-47115-5_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04278929/file/Refactoring_of_Multi-Instance-BPMN_Processes_with_Time_and_Resources.pdf BibTex
titre
A Navigation-Based Evaluation Metric for Probabilistic Occupancy Grids: Pathfinding Cost Mean Squared Error
auteur
Jean-Baptiste Horel, Robin Baruffa, Lukas Rummelhard, Alessandro Renzaglia, Christian Laugier
article
ITCS 2023 - 26th IEEE International Conference on Intelligent Transportation Systems, IEEE, Sep 2023, Bilbao, Spain, Spain. pp.1-6
Accès au texte intégral et bibtex
https://hal.science/hal-04211125/file/IEEE_ITSC_2023_final-4.pdf BibTex
titre
Compositional Verification of Stigmergic Collective Systems
auteur
Luca Di Stefano, Frederic Lang
article
VMCAI 2023 - 24th International Conference on Verification, Model Checking and Abstract Interpretation, Jan 2023, Boston, United States. pp.1-22, ⟨10.1007/978-3-031-24950-1_8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03869922/file/DiStefano-Lang-23.pdf BibTex

Special issue

titre
Editorial for FACS 2021 special section (SoSyM)
auteur
Gwen Salaün
article
Software and Systems Modeling, 22 (2), pp.471-472, 2023, ⟨10.1007/s10270-023-01088-3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04310133/file/preface-sosym-facs21.pdf BibTex

Reports

titre
Rapport d’évaluation de l’unité FEMTO-ST – Franche-Comté Électronique, Mécanique, Thermique et Optiques - Sciences et Technologies
auteur
Eric Tournié, Jean-Marc Allain, Mathieu Arnoux, Nathalie Bardou, Skandar Basrour, Jean-Marc. Bassat, Christian Bergaud, Xavier Brun, Nathalie Destouches, Aurelian Fatu, David Folio, Antoine Grall, Luca Guidoni, Alexandre Guitton, Pierre-Yves Joubert, Arnaud Landragin, Daniel Racoceanu, Christine Restoin, Gwen Salaün, Roger Serra, Didier Trichet
article
C2023-EV-0251215K-DER-PUR230023102-RF, Hcéres. 2023, pp.1-51
Accès au texte intégral et bibtex
https://hal.science/hal-04505233/file/C2023-EV-0251215K-DER-PUR230023102-RF.pdf BibTex

Theses

titre
Systèmes concurrents hiérarchiques : équivalence, analyse et structuration
auteur
Pierre Bouvier
article
Calcul parallèle, distribué et partagé [cs.DC]. Université Grenoble Alpes [2020-..], 2023. Français. ⟨NNT : 2023GRALM045⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-04412686/file/BOUVIER_2023_archivage.pdf BibTex

2022

Journal articles

titre
Models and analysis for user-driven reconfiguration of rule-based IoT applications
auteur
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
article
Internet of Things, 2022, 19, pp.100515. ⟨10.1016/j.iot.2022.100515⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03781473/file/main.pdf BibTex
titre
Design and Deployment of Expressive and Correct Web of Things Applications
auteur
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
article
ACM Transactions on Internet of Things, 2022, 3, pp.1 - 30. ⟨10.1145/3475964⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03495593/file/main-acm-iot.pdf BibTex
titre
Verification of Distributed Systems via Sequential Emulation
auteur
Luca Di Stefano, Rocco de Nicola, Omar Inverso
article
ACM Transactions on Software Engineering and Methodology, 2022, 31 (3), pp.1-41. ⟨10.1145/3490387⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03549925/file/Di%20Stefano%20at%20al%20-%20Verification%20of%20Distributed%20Systems%20via%20Sequential%20Emulation%20-%20to%20appear%20TOSEM.pdf BibTex

Conference papers

titre
Quantifying the Similarity of BPMN Processes
auteur
Gwen Salaün
article
APSEC 2022 - 29th Asia-Pacific Software Engineering Conference, Dec 2022, Virtual, Japan. pp.1-10
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03890531/file/main.pdf BibTex
titre
Optimization of BPMN Processes via Automated Refactoring
auteur
Francisco Durán, Gwen Salaün
article
ICSOC 2022 - 20th International Conference on Service-Oriented Computing, Nov 2022, Sevilla, Spain. pp.1-15, ⟨10.1007/978-3-031-20984-0_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03883829/file/main.pdf BibTex
titre
Debugging of BPMN Processes Using Coloring Techniques
auteur
Quentin Nivon, Gwen Salaün
article
FACS, Nov 2022, Oslo, Norway. ⟨10.1007/978-3-031-20872-0_6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03847267/file/manuscript.pdf BibTex
titre
WEASY: A Tool for Modelling Optimised BPMN Processes
auteur
Angel Contreras, Yliès Falcone, Gwen Salaün, Ahang Zuo
article
FACS 2022 - 18th International Conference on Formal Aspects of Component Software, Nov 2022, Oslo / Online, Norway. ⟨10.1007/978-3-031-20872-0_7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03848350/file/WEASY%20A%20Tool%20for%20Modelling%20Optimised%20BPMN.pdf BibTex
titre
Probabilistic Analysis of Industrial IoT Applications
auteur
Yliès Falcone, Irman Faqrizal, Gwen Salaün
article
IoT 2022 -The 12th International Conference on the Internet of Things, Nov 2022, Delft, Netherlands. ⟨10.1145/3567445.3567461⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03848674/file/main%20%281%29.pdf BibTex
titre
Runtime Enforcement for IEC 61499 Applications
auteur
Yliès Falcone, Gwen Salaün, Irman Faqrizal
article
SEFM 2022 - 20th International Conference on Software Engineering and Formal Methods, Sep 2022, Berlin, Germany. pp.1-17, ⟨10.1007/978-3-031-17108-6_22⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03766095/file/main.pdf BibTex
titre
Probabilistic Model Checking of BPMN Processes at Runtime
auteur
Yliès Falcone, Gwen Salaün, Ahang Zuo
article
iFM 2022 - International Conference on integrated Formal Methods, Jun 2022, Lugano, Switzerland. pp.1-17, ⟨10.1007/978-3-031-07727-2_11⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03665305/file/Probabilistic%20Model%20Checking%20of%20BPMN%20Processes%20at%20Runtime.pdf BibTex
titre
Counting Bugs in Behavioural Models using Counterexample Analysis
auteur
Irman Faqrizal, Gwen Salaün
article
FormaliSE 2022 - International Conference on Formal Methods in Software Engineering, May 2022, Pittsburgh, United States. pp.1-11, ⟨10.1145/3524482.3527647⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03665317/file/main.pdf BibTex
titre
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
auteur
Lina Marsso, Radu Mateescu, Lucie Muller, Wendelin Serwe
article
Mars 2022 - 5th Workshop on Models for Formal Analysis of Real Systems, Apr 2022, Munich, Germany. pp.60-117, ⟨10.4204/EPTCS.355.5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03623521/file/Marsso-Mateescu-Muller-Serwe-22.pdf BibTex
titre
From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes
auteur
Francisco Durán, Yliès Falcone, Camilo Rocha, Gwen Salaün, Ahang Zuo
article
WRLA 2022 - 14th International Workshop on Rewriting Logic and its Applications, Apr 2022, Munich, Germany. pp.1-18, ⟨10.1007/978-3-031-12441-9_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03766148/file/From%20Static%20to%20Dynamic%20Analysis%20and%20Allocation%20of%20Resources%20for%20BPMN%20Processes.pdf BibTex
titre
Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles
auteur
Jean-Baptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, Wendelin Serwe
article
DATE/ASD 2022 - Design, Automation and Test in Europe - Autonomous Systems Design, Mar 2022, Antwerp, Belgium. pp.532-537, ⟨10.23919/DATE54114.2022.9774581⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03516799/file/paper_DATE_ADS_22.pdf BibTex

Book sections

titre
Equivalence Checking 40 Years After: A Review of Bisimulation Tools
auteur
Hubert Garavel, Frédéric Lang
article
A Journey from Process Algebra via Timed Automata to Model Learning, 13560, Springer Nature Switzerland; Springer Nature Switzerland, pp.213-265, 2022, Lecture Notes in Computer Science, ⟨10.1007/978-3-031-15629-8_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03920338/file/Garavel-Lang-22.pdf BibTex

Reports

titre
Compositional Verification of Priority Systems using Sharp Bisimulation
auteur
Luca Di Stefano, Frédéric Lang
article
[Research Report] INRIA. 2022, pp.1-32
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03640683/file/DiStefano-Lang-22-RR.pdf BibTex

2021

Journal articles

titre
Resource Provisioning Strategies for BPMN Processes: Specification and Analysis using Maude
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
Journal of Logical and Algebraic Methods in Programming, 2021, pp.1-50. ⟨10.1016/j.jlamp.2021.100711⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03487960/file/main.pdf BibTex
titre
Debugging of Behavioural Models using Counterexample Analysis
auteur
Gianluca Barbon, Vincent Leroy, Gwen Salaün
article
IEEE Transactions on Software Engineering, 2021, 47 (6), pp.1184-1197. ⟨10.1109/TSE.2019.2915303⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02145610/file/tse.pdf BibTex
titre
Compositional Verification of Concurrent Systems by Combining Bisimulations
auteur
Frederic Lang, Radu Mateescu, Franco Mazzanti
article
Formal Methods in System Design, 2021, ⟨10.1007/s10703-021-00360-w⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03159616/file/Lang-Mateescu-Mazzanti-21.pdf BibTex
titre
Quantifying the Similarity of Non-bisimilar Labelled Transition Systems
auteur
Gwen Salaün
article
Science of Computer Programming, 2021, 202, ⟨10.1016/j.scico.2020.102580⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03017666/file/main.pdf BibTex

Conference papers

titre
Runtime Enforcement with Reordering, Healing, and Suppression
auteur
Yliès Falcone, Gwen Salaün
article
SEFM 2021 - 19th IEEE International Conference on Software Engineering and Formal Methods, Dec 2021, Virtual, United Kingdom. pp.1-20
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03484045/file/main.pdf BibTex
titre
Is CADP an Applicable Formal Method?
auteur
Hubert Garavel, Frederic Lang, Radu Mateescu, Wendelin Serwe
article
AppFM 2021 - 1st International Workshop on Applicable Formal Methods, Nov 2021, Bejing, China. ⟨10.48550/arXiv.2111.08203⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03485114/file/main.pdf BibTex
titre
Business Process Models for Analysis of Industrial IoT Applications
auteur
Ajay Krishna, Gwen Salaün
article
IoT 2021 - 11th International Conference on the Internet of Things, Nov 2021, St. Gallen, Switzerland. pp.1-8, ⟨10.1145/3494322.3494336⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03484052/file/main.pdf BibTex
titre
Verifying Temporal Properties of Stigmergic Collective Systems Using CADP
auteur
Luca Di Stefano, Frédéric Lang
article
ISoLA 2021 - 10th International Symposium on Leveraging Applications of Formal Methods, Oct 2021, Rhodes, Greece. pp.473-489, ⟨10.1007/978-3-030-89159-6_29⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03385131/file/main.pdf BibTex
titre
Semi-automated Modelling of Optimized BPMN Processes
auteur
Yliès Falcone, Gwen Salaün, Ahang Zuo
article
SCC 2021 - IEEE International Conference on Services Computing, Sep 2021, CHICAGO / Virtual, United States. pp.1-6
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03330330/file/Semi-automated%20Modelling%20of%20Optimized%20BPMN.pdf BibTex
titre
Consistent Substitution of Object in Rule-based IoT Applications
auteur
Gwen Salaün
article
COMPSAC 2021 - Computer Software and Applications Conference, Jul 2021, Virtual, United States. pp.1-9
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03484028/file/main.pdf BibTex
titre
Efficient Algorithms for Three Reachability Problems in Safe Petri Nets
auteur
Pierre Bouvier, Hubert Garavel
article
PETRI NETS 2021 - 42nd International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2021, Paris, France. pp.339-359, ⟨10.1007/978-3-030-76983-3_17⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03286069/file/Bouvier-Garavel-21-a.pdf BibTex
titre
R-MOZART: A Reconfiguration Tool for WebThings Applications
auteur
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
article
2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), May 2021, Madrid / Virtual, Spain. pp.41-44, ⟨10.1109/ICSE-Companion52605.2021.00031⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03157158/file/main.pdf BibTex
titre
Seamless Reconfiguration of Rule-Based IoT Applications
auteur
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, Gwen Salaün
article
SEAMS 2021 - 16th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, May 2021, Madrid / Virtual, Spain. pp.142-148
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03254192/file/main-seams21.pdf BibTex

Special issue

titre
Preface: Special issue on Software Engineering and Formal Methods
auteur
Peter Csaba C Ölveczky, Gwen Salaün
article
Software and Systems Modeling, 20 (2), pp.291-292, 2021, ⟨10.1007/s10270-021-00874-1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03507829/file/preface_sosym_sefm_2019.pdf BibTex

Books

titre
Formal Aspects of Component Software
auteur
Gwen Salaün, Anton Wijs
article
Springer International Publishing, 13077, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-90636-8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03507856/file/preface_facs_2021.pdf BibTex

Reports

titre
The VLSAT-3 Benchmark Suite
auteur
Pierre Bouvier
article
[Research Report] RT-0516, INRIA Grenoble Rhône-Alpes. 2021, pp.1-20
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03468625/file/RT-0516.pdf BibTex
titre
The VLSAT-2 Benchmark Suite
auteur
Pierre Bouvier, Hubert Garavel
article
[Technical Report] RT-0514, INRIA Grenoble Rhône-Alpes. 2021, pp.1-8
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03337115/file/RT-0514.pdf BibTex

2020

Journal articles

titre
F 3 ARIoT: A Framework for Autonomic Resilience of IoT Applications in the Fog
auteur
Umar Ozeer, Loic Letondeur, Gwen Salaün, François-Gaël Ottogalli, Jean-Marc Vincent
article
Internet of Things, 2020, pp.1-54. ⟨10.1016/j.iot.2020.100275⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02933365/file/main.pdf BibTex
titre
Compositional model checking with divergence preserving branching bisimilarity is lively
auteur
Sander de Putter, Frédéric Lang, Anton Wijs
article
Science of Computer Programming, 2020, 196, pp.102493. ⟨10.1016/j.scico.2020.102493⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02890800/file/Compositional_Model_Checking_Is_Lively.pdf BibTex
titre
So, what exactly is a qualitative calculus?
auteur
Armen Inants, Jérôme Euzenat
article
Artificial Intelligence, 2020, 289, pp.103385. ⟨10.1016/j.artint.2020.103385⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02942947/file/inants2020a.pdf BibTex

Conference papers

titre
Automated Transition Coverage in Behavioural Conformance Testing
auteur
Lina Marsso, Radu Mateescu, Wendelin Serwe
article
ICTSS 2020 - 32nd IFIP International Conference on Testing Software and Systems, Dec 2020, Napoli, Italy. pp.219-235, ⟨10.1007/978-3-030-64881-7_14⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03038050/file/paper.pdf BibTex
titre
Clusters of Faulty States for Debugging Behavioural Models
auteur
Irman Faqrizal, Gwen Salaün
article
APSEC 2020 - 27th Asia-Pacific Software Engineering Conference, Dec 2020, Singapore, Singapore. pp.1-9
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03035539/file/main.pdf BibTex
titre
The 2020 Expert Survey on Formal Methods
auteur
Hubert Garavel, Maurice ter Beek, Jaco van de Pol
article
FMICS 2020 - 25th International Conference on Formal Methods for Industrial Critical Systems, Sep 2020, Vienna, Austria. pp.3-69, ⟨10.1007/978-3-030-58298-2_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03082818/file/Garavel-terBeek-vandePol-20.pdf BibTex
titre
Verification of a Failure Management Protocol for Stateful IoT Applications
auteur
Umar Ozeer, Gwen Salaün, Loic Letondeur, François-Gaël Ottogalli, Jean-Marc Vincent
article
Proc. of FMICS'20, Sep 2020, Vienne, Austria. ⟨10.1007/978-3-030-58298-2_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02930872/file/main.pdf BibTex
titre
Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account
auteur
Pierre Bouvier, Hubert Garavel, Hernan Ponce de León
article
PETRI NETS 2020 - 41st International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2020, Paris, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02875957/file/Bouvier-Garavel-PonceDeLeon-20.pdf BibTex
titre
Combining SLiVER with CADP to Analyze Multi-agent Systems
auteur
Luca Di Stefano, Frédéric Lang, Wendelin Serwe
article
COORDINATION 2020 - 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages, Jun 2020, La Valetta, Malta. pp.370-385, ⟨10.1007/978-3-030-50029-0_23⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02890401/file/coordination2020.pdf BibTex
titre
Specifying a Cryptographical Protocol in Lustre and SCADE
auteur
Lina Marsso
article
MARS 2020 - 4th Workshop on Models for Formal Analysis of Real Systems, Apr 2020, Dublin, Ireland. pp.149-199, ⟨10.4204/EPTCS.316.7⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02556856/file/Marsso-20.pdf BibTex
titre
Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
auteur
Frédéric Lang, Radu Mateescu, Franco Mazzanti
article
TACAS 2020 - Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, Dublin, Ireland. pp.57-76, ⟨10.1007/978-3-030-45237-7_4⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02555692/file/Lang-Mateescu-Mazzanti-20.pdf BibTex
titre
Analysis of the Runtime Resource Provisioning of BPMN Processes using Maude
auteur
Francisco Duran, Camilo Rocha, Gwen Salaün
article
WRLA 2020 - 13th International Workshop on Rewriting Logic and its Applications, Apr 2020, Dublin, Ireland. pp.1-16
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02931077/file/main-11.pdf BibTex
titre
MOZART: Design and Deployment of Advanced IoT Applications
auteur
Ajay Krishna, Michel Le Pallec, Alejandro Martinez, Radu Mateescu, Gwen Salaün
article
WWW 2020 - International World Wide Web Conference, Apr 2020, Taipei, Taiwan. pp.1-4, ⟨10.1145/3366424.3383532⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02554029/file/main-web-preprint.pdf BibTex
titre
Using Model Checking to Identify Timing Interferences on Multicore Processors
auteur
Viet Anh Nguyen, Eric Jenn, Wendelin Serwe, Frederic Lang, Radu Mateescu
article
ERTS 2020 - 10th European Congress on Embedded Real Time Software and Systems, Jan 2020, Toulouse, France. pp.1-10
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02462085/file/ERTS2020_paper_36.pdf BibTex
titre
Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks
auteur
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, Marc Renaudin
article
MARS 2020 - 4th Workshop on Models for Formal Analysis of Real Systems, 2020, Dublin, Ireland. pp.200-239, ⟨10.4204/EPTCS.316.8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02559125/file/Mateescu-Serwe-Bouzafour-Renaudin-20.pdf BibTex

Reports

titre
Proposal for Adding Useful Features to Petri-Net Model Checkers
auteur
Hubert Garavel
article
[Research Report] Inria Grenoble - Rhône-Alpes. 2020
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03087421/file/Garavel-20.pdf BibTex
titre
The VLSAT-1 Benchmark Suite
auteur
Pierre Bouvier, Hubert Garavel
article
[Technical Report] RT-0510, INRIA Grenoble Rhône-Alpes. 2020, pp.6
Accès au texte intégral et bibtex
https://hal.science/hal-03007233/file/RT-0510.pdf BibTex

Theses

titre
Models and Verification for Composition and Reconfiguration of Web of Things Applications
auteur
Ajay Krishna Muroor Nadumane
article
Other [cs.OH]. Université Grenoble Alpes [2020-..], 2020. English. ⟨NNT : 2020GRALM067⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-03188299/file/MUROOR_NADUMANE_2020_archivage.pdf BibTex

2019

Journal articles

titre
A Rewriting Logic Approach to Resource Allocation Analysis in Business Process Models
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
Science of Computer Programming, 2019, 183, pp.1-32. ⟨10.1016/j.scico.2019.102303⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02345895/file/main.pdf BibTex
titre
Nested-unit Petri nets
auteur
Hubert Garavel
article
Journal of Logical and Algebraic Methods in Programming, 2019, 104, pp.60-85. ⟨10.1016/j.jlamp.2018.11.005⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02072190/file/Garavel-19.pdf BibTex
titre
Checking Business Process Evolution
auteur
Ajay Krishna, Pascal Poizat, Gwen Salaün
article
Science of Computer Programming, 2019, 170, pp.1-26. ⟨10.1016/j.scico.2018.09.007⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01920273/file/main_SCP_FACS.pdf BibTex

Conference papers

titre
Asynchronous Testing of Synchronous Components in GALS Systems
auteur
Lina Marsso, Radu Mateescu, Ioannis Parissis, Wendelin Serwe
article
IFM'2019 - 15th International Conference on Integrated Formal Methods, Dec 2019, Bergen, Norway. pp.360-378, ⟨10.1007/978-3-030-34968-4_20⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02394989/file/Marsso-Mateescu-Parissis-Serwe-09.pdf BibTex
titre
Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving
auteur
Philippe Ledent, Anshul Paigwar, Alessandro Renzaglia, Radu Mateescu, Christian Laugier
article
CIS-RAM 2019 - 9th IEEE International Conference on Cybernetics and Intelligent Systems (CIS) Robotics, Automation and Mechatronics (RAM), Nov 2019, Bangkok, Thailand. pp.1-6
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02355551/file/FormalValidation_cmcdot_CISRAM19.pdf BibTex
titre
Analysis of Resource Allocation of BPMN Processes
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
ICSOC 2019 - 17th International Conference on Service-Oriented Computing, Oct 2019, Toulouse, France. pp.452-457, ⟨10.1007/978-3-030-33702-5_35⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02345879/file/main.pdf BibTex
titre
Automated Composition, Analysis and Deployment of IoT Applications
auteur
Francisco Durán, Gwen Salaün, Ajay Krishna
article
TOOLS 2019 - 51st International Conference on Software Technology: Methods and Tools, Oct 2019, Innopolis, Russia. pp.252-268, ⟨10.1007/978-3-030-29852-4_21⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02345865/file/main.pdf BibTex
titre
Compositional Verification of Concurrent Systems by Combining Bisimulations
auteur
Frédéric Lang, Radu Mateescu, Franco Mazzanti
article
FM 2019 - 23rd International Conference on Formal Methods, Oct 2019, Porto, Portugal. pp.196-213, ⟨10.1007/978-3-030-30942-8_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02295459/file/main.pdf BibTex
titre
Quantifying the Similarity of Non-bisimilar Labelled Transition Systems
auteur
Gwen Salaün
article
FOCLASA 2019 - 17th International Workshop on Coordination and Self-adaptativeness of Software Applications, Sep 2019, Oslo, Norway. pp.1-14
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02933345/file/main.pdf BibTex
titre
Rigorous Design and Deployment of IoT Applications
auteur
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, Gwen Salaün
article
FormaliSE 2019 - 7th International Conference on Formal Methods in Software Engineering, May 2019, Montreal, Canada. pp.21-30, ⟨10.1109/FormaliSE.2019.00011⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02146553/file/formalise-main.pdf BibTex
titre
IoT Composer: Composition and Deployment of IoT Applications
auteur
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, Gwen Salaün
article
ICSE 2019 - IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings, May 2019, Montreal, Canada. pp.19-22, ⟨10.1109/ICSE-Companion.2019.00028⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02146569/file/main.pdf BibTex
titre
Visual Debugging of Behavioural Models
auteur
Gianluca Barbon, Vincent Leroy, Gwen Salaün, Emmanuel Yah
article
ICSE 2019 - IEEE/ACM 41st International Conference on Software Engineering: Companion Proceedings, May 2019, Montreal, Canada. pp.107-110, ⟨10.1109/ICSE-Companion.2019.00050⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02145535/file/main.pdf BibTex
titre
Debugging of Behavioural Models with CLEAR
auteur
Gianluca Barbon, Vincent Leroy, Gwen Salaün
article
TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2019, Prague, Czech Republic. pp.386-392, ⟨10.1007/978-3-030-17462-0_26⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02121180/file/Barbon2019_Chapter_DebuggingOfBehaviouralModelsWi.pdf BibTex
titre
TOOLympics 2019: An Overview of Competitions in Formal Methods
auteur
Ezio Bartocci, Dirk Beyer, Paul Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
article
25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Apr 2019, Prague, Czech Republic. pp.3-24, ⟨10.1007/978-3-030-17502-3_1⟩
Accès au bibtex
BibTex
titre
The Rewrite Engines Competitions: A RECtrospective
auteur
Francisco Durán, Hubert Garavel
article
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Part III: TOOLympics, Apr 2019, Prague, Czech Republic. pp.1-9, ⟨10.1007/978-3-030-17502-3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02133649/file/Duran-Garavel-19.pdf BibTex
titre
Designing and Implementing Resilient IoT Applications in the Fog: A Smart Home Use Case
auteur
Umar Ozeer, Loïc Letondeur, François-Gaël Ottogalli, Gwen Salaün, Jean-Marc Vincent
article
ICIN 2019 - 22nd Conference on Innovation in Clouds, Internet and Networks, Feb 2019, Paris, France. pp.230-232, ⟨10.1109/ICIN.2019.8685909⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01979686/file/PID5743869.pdf BibTex

Book sections

titre
Hunting Superfluous Locks with Model Checking
auteur
Viet-Anh Nguyen, Wendelin Serwe, Radu Mateescu, Eric Jenn
article
From Software Engineering to Formal Methods and Tools, and Back, 11865, Springer Verlag, pp.416-432, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-30985-5_24⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02314088/file/Nguyen-Serwe-Mateescu-Jenn-19.pdf BibTex
titre
Reflections on Bernhard Steffen’s Physics of Software Tools
auteur
Hubert Garavel, Radu Mateescu
article
Models, Mindsets, Meta: The What, the How, and the Why Not?, Springer Verlag, pp.186-207, 2019, ⟨10.1007/978-3-030-22348-9_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02394588/file/Garavel-Mateescu-18.pdf BibTex

Theses

titre
Autonomic resilience of distributed IoT applications in the Fog
auteur
Umar Ibn Zaid Ozeer
article
Databases [cs.DB]. Université Grenoble Alpes, 2019. English. ⟨NNT : 2019GREAM054⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-02570825/file/OZEER_2019_archivage.pdf BibTex
titre
On Model-based Testing of GALS Systems
auteur
Lina Marsso
article
Formal Languages and Automata Theory [cs.FL]. Université Grenoble Alpes, 2019. English. ⟨NNT : 2019GREAM078⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-02948083/file/MARSSO_2019_diffusion.pdf BibTex

2018

Journal articles

titre
Stochastic Analysis of BPMN with Time in Rewriting Logic
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
Science of Computer Programming, 2018, 168, pp.1-17. ⟨10.1016/j.scico.2018.08.007⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01866289/file/main.pdf BibTex
titre
On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
auteur
Radu Mateescu, José Ignacio Requeno
article
International Journal on Software Tools for Technology Transfer, 2018, 20 (5), pp.563-587. ⟨10.1007/s10009-018-0499-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01862754/file/mateescu_requeno_prob.pdf BibTex
titre
Automated verification of automata communicating via FIFO and bag buffers
auteur
Lakhdar Akroun, Gwen Salaün
article
Formal Methods in System Design, 2018, 52 (3), pp.260 - 276. ⟨10.1007/s10703-017-0285-8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01898159/file/main-fmsd.pdf BibTex

Conference papers

titre
Resilience of Stateful IoT Applications in a Dynamic Fog Environment
auteur
Umar Ozeer, Xavier Etchevers, Loic Letondeur, François-Gaël Ottogalli, Gwen Salaün, Jean-Marc Vincent
article
EAI International Conference on Mobile and Ubiquitous Systems: Networking and Services (MobiQuitous '18), Nov 2018, New York, United States. pp.1-10, ⟨10.1145/3286978.3287007⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01927286/file/ResIoT.pdf BibTex
titre
Compositional Verification in Action
auteur
Hubert Garavel, Frédéric Lang, Laurent Mounier
article
FMICS 2018 - 23rd International Conference on Formal Methods for Industrial Critical Systems, Sep 2018, Maynooth, Ireland. pp.189-210, ⟨10.1007/978-3-030-00244-2_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01890246/file/Garavel-Lang-Mounier-18.pdf BibTex
titre
Using LNT Formal Descriptions for Model-Based Diagnosis
auteur
Birgit Hofer, Radu Mateescu, Wendelin Serwe, Franz Wotawa
article
DX 2018 - 29th International Workshop on Principles of Diagnosis, Aug 2018, Warsaw, Poland. pp.1-8
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01877693/file/diag_with_fm.pdf BibTex
titre
Counterexample Simplification for Liveness Property Violation
auteur
Gianluca Barbon, Vincent Leroy, Gwen Salaün
article
SEFM 2018 - 16th International Conference on Software Engineering and Formal Methods, Jun 2018, Toulouse, France. pp.173-188, ⟨10.1007/978-3-319-92970-5_11⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01818790/file/sefm18_rev.pdf BibTex
titre
Computing the Parallelism Degree of Timed BPMN Processes
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
FOCLASA 2018 - 16th International Workshop on Foundations of Coordination Languages and Self-Adaptative Systems, Jun 2018, Toulouse, France. pp.1-16, ⟨10.1007/978-3-030-04771-9_24⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01961952/file/main.pdf BibTex
titre
Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits
auteur
Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, Wendelin Serwe
article
ASYNC'18 - 24th IEEE International Symposium on Asynchronous Circuits and Systems , May 2018, Vienne, Austria
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01777093/file/Bouzafour-Renaudin-Garavel-et-al-18.pdf BibTex
titre
A Formal TLS Handshake Model in LNT
auteur
Josip Bozic, Lina Marsso, Radu Mateescu, Franz Wotawa
article
MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. pp.1 - 40, ⟨10.4204/EPTCS.268.1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01779151/file/Bozic-Marsso-Mateescu-Wotawa-18.pdf BibTex
titre
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
auteur
Hubert Garavel, Lina Marsso
article
MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. pp.41 - 87, ⟨10.4204/EPTCS.268.2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01775332/file/Garavel-Marsso-18.pdf BibTex
titre
Symbolic Specification and Verification of Data-aware BPMN Processes using Rewriting Modulo SMT
auteur
Francisco Durán, Camilo Rocha, Gwen Salaün
article
WRLA 2018 : 12th International Workshop on Rewriting Logic and its Applications, Apr 2018, Thessaloniki, Greece. pp.1-20
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01866268/file/main.pdf BibTex
titre
TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
auteur
Lina Marsso, Radu Mateescu, Wendelin Serwe
article
TACAS 2018 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2018, Thessaloniki, Greece. pp.211-228, ⟨10.1007/978-3-319-89963-3_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01777861/file/Marsso-Mateescu-Serwe-18.pdf BibTex
titre
Automated Analysis of Industrial Workflow-based Models
auteur
Mario Cortes-Cornax, Ajay Krishna, Adrian Mos, Gwen Salaün
article
SAC 2018 - 33rd Annual ACM Symposium on Applied Computing, ACM, Apr 2018, Pau, France. pp.120-127, ⟨10.1145/3167132.3167142⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01781315/file/main-SAC18.pdf BibTex
titre
Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages - The 4th Rewrite Engines Competition
auteur
Hubert Garavel, Mohammad-Ali Tabikh, Imad-Seddik Arrada
article
Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA'18), 2018, Thessaloniki, Greece
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01883212/file/Garavel-Tabikh-Arrada-18.pdf BibTex

Special issue

titre
Preface: Special issue on Foundations of Coordination Languages and Self-adaptive Systems
auteur
Carlos Canal, Gwen Salaün
article
Science of Computer Programming, 168, pp.169 - 170, 2018, ⟨10.1016/j.scico.2018.09.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01898179/file/preface_scp_foclasa_17.pdf BibTex
titre
Recent advances in interactive and automated analysis
auteur
Radu Mateescu
article
France. International Journal on Software Tools for Technology Transfer, 20 (2), pp.119 - 123, 2018, ⟨10.1007/s10009-017-0477-y⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01766570/file/preface_sttt_tacas_16.pdf BibTex

Proceedings

titre
MCC’2017 - The Seventh Model Checking Contest
auteur
Fabrice Kordon, Hubert Garavel, Lom Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, Francis Hulin-Hubard, Elvio Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter Gjøl Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jiří Srba, Yann Thierry-Mieg, Jaco van de Pol, Karsten Wolf
article
LNCS Transactions on Petri Nets and Other Models of Concurrency, 11090, pp.181-209, 2018, Lecture Notes in Computer Science, ⟨10.1007/978-3-662-58381-4_9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01917492/file/ToPNoC-mcc2017.pdf BibTex
titre
Software Technologies: Applications and Foundations (STAF 2018)
auteur
Manuel Mazzara, Iulian Ober, Gwen Salaün
article
Mazzara, Manuel; Ober, Iulian; Salaun, Gwen. STAF 2018 - Federation of International Conferences on Software Technologies: Applications and Foundations, Jun 2018, Toulouse, France. 11176, Springer, XXI, 658 p., 2018, Programming and Software Engineering book series, 978-3030047702. ⟨10.1007/978-3-030-04771-9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01961961/file/preface-staf18-workshops-v2.pdf BibTex

Theses

titre
Debugging of Behavioural Models using Counterexample Analysis
auteur
Gianluca Barbon
article
Systems and Control [cs.SY]. Université Grenoble Alpes, 2018. English. ⟨NNT : 2018GREAM077⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-02191544/file/BARBON_2018_archivage.pdf BibTex

2017

Journal articles

titre
Asynchronous synthesis techniques for coordinating autonomic managers in the cloud
auteur
Rim Abid, Gwen Salaün, Noël de Palma
article
Science of Computer Programming, 2017, 146, pp.87 - 103. ⟨10.1016/j.scico.2017.05.005⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01630717/file/main_SCP_FACS.pdf BibTex
titre
Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous
auteur
Hugues Evrard, Frédéric Lang
article
Journal of Logical and Algebraic Methods in Programming, 2017, 88, pp.33. ⟨10.1016/j.jlamp.2016.09.002⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01412911/file/Evrard-Lang-16-auteur.pdf BibTex
titre
Reliable Self-deployment of Distributed Cloud Applications
auteur
Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma
article
Software: Practice and Experience, 2017, 47 (1), pp.3-20. ⟨10.1002/spe.2400⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01290465/file/main-SPE-2015.pdf BibTex

Conference papers

titre
On the Most Suitable Axiomatization of Signed Integers
auteur
Hubert Garavel
article
23th International Workshop on Algebraic Development Techniques (WADT), Sep 2017, Gregynog, Wales, UK, United Kingdom. pp.120-134, ⟨10.1007/978-3-319-72044-9_9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01667321/file/Garavel-17.pdf BibTex
titre
VBPMN: Automated Verification of BPMN Processes
auteur
Ajay Krishna, Pascal Poizat, Gwen Salaün
article
13th International Conference on integrated Formal Methods (iFM 2017), Sep 2017, Turin, Italy
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01591665/file/main.pdf BibTex
titre
The ContextAct@A4H real-life dataset of daily-living activities Activity recognition using model checking
auteur
Paula Lago, Frederic Lang, Claudia Roncancio, Claudia Jiménez-Guarín, Radu Mateescu, Nicolas Bonnefond
article
10th International and Interdisciplinary Conference - CONTEXT 2017, Jun 2017, Paris, France. pp.175-188, ⟨10.1007/978-3-319-57837-8_14⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01551418/file/Lago-Lang-Roncancio-et-al-17.pdf BibTex
titre
Verifying Timed BPMN Processes Using Maude
auteur
Francisco Durán, Gwen Salaün
article
19th International Conference on Coordination Languages and Models (COORDINATION), Jun 2017, Neuchâtel, Switzerland. pp.219-236, ⟨10.1007/978-3-319-59746-1_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01538104/file/main.pdf BibTex
titre
The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark
auteur
Hubert Garavel, Wendelin Serwe
article
2nd Workshop on Models for Formal Analysis of Real Systems, Apr 2017, Uppsala, Sweden. pp.230 - 270, ⟨10.4204/EPTCS.244.10⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01511847/file/Garavel-Serwe-17.pdf BibTex
titre
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
auteur
Hubert Garavel, Lina Marsso
article
2nd Workshop on Models for Formal Analysis of Real Systems, Apr 2017, Uppsala, Sweden. pp.129 - 183, ⟨10.4204/EPTCS.244.6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01511859/file/Garavel-Marsso-17.pdf BibTex
titre
Debugging of Concurrent Systems using Counterexample Analysis
auteur
Gianluca Barbon, Vincent Leroy, Gwen Salaün
article
7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Tehran, Iran. pp.20-34, ⟨10.1007/978-3-319-68972-2_2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01533401/file/fsen17_rev.pdf BibTex

Book sections

titre
From LOTOS to LNT
auteur
Hubert Garavel, Frédéric Lang, Wendelin Serwe
article
Joost-Pieter Katoen; Rom Langerak; Arend Rensink. ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, 10500, Springer, pp.3-26, 2017, Lecture Notes in Computer Science, 978-3-319-68270-9. ⟨10.1007/978-3-319-68270-9_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01621670/file/Garavel-Lang-Serwe-17.pdf BibTex

Special issue

titre
Preface: Special issue on software verification and testing
auteur
Mercedes Merayo, Gwen Salaün
article
Journal of Systems and Software, 132, pp.317 - 318, 2017, ⟨10.1016/j.jss.2017.07.025⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01869106/file/Merayo-Salaun-17.pdf BibTex

2016

Journal articles

titre
VerChor: A Framework for the Design and Verification of Choreographies
auteur
Matthias Güdemann, Pascal Poizat, Gwen Salaün, Lina Ye
article
IEEE Transactions on Services Computing, 2016, 9 (4), pp.647-660. ⟨10.1109/TSC.2015.2413401⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01198918/file/TSC-2013-12-0224-author.pdf BibTex
titre
Formal Modelling and Verification of GALS Systems Using GRL and CADP
auteur
Fatma Jebali, Frédéric Lang, Radu Mateescu
article
Formal Aspects of Computing, 2016, 28 (5), pp.767-804. ⟨10.1007/s00165-016-0373-3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01290449/file/fac2egui-crc.pdf BibTex
titre
Verification of EB3 specifications using CADP
auteur
Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu
article
Formal Aspects of Computing, 2016, 28 (1), pp.145-178. ⟨10.1007/s00165-016-0362-6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01290460/file/FAOC.pdf BibTex
titre
An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysis
auteur
Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, Chris Myers
article
Science of Computer Programming, 2016, ⟨10.1016/j.scico.2016.01.002⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01261234/file/scp_fmics2014.pdf BibTex
titre
Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications
auteur
Rim Abid, Gwen Salaün, Noel de Palma
article
Science of Computer Programming, 2016, 117, pp.1-16. ⟨10.1016/j.scico.2015.12.001⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01246152/file/main-scp13.pdf BibTex
titre
Taking Arduino to the Internet of Things: the ASIP programming model
auteur
Gianluca Barbon, Michael Margolis, Filippo Palumbo, Franco Raimondi, Nick Weldin
article
Computer Communications, 2016, 00, pp.1 - 15. ⟨10.1016/j.comcom.2016.03.016⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01416490/file/comcom16.pdf BibTex
titre
MCC’2015 – The Fifth Model Checking Contest
auteur
Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, César Rodríguez, Francis Hulin-Hubard
article
LNCS Transactions on Petri Nets and Other Models of Concurrency, 2016, Lecture Notes in Computer Science, 9930, pp.262-273. ⟨10.1007/978-3-662-53401-4_12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01361274/file/main.pdf BibTex
titre
Robust and reliable reconfiguration of cloud applications
auteur
Francisco Durán, Gwen Salaün
article
Journal of Systems and Software, 2016, 122, pp.524-537. ⟨10.1016/j.jss.2015.09.020⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01245555/file/main.pdf BibTex

Conference papers

titre
Checking Business Process Evolution
auteur
Pascal Poizat, Gwen Salaün, Ajay Krishna
article
13th International Conference on Formal Aspects of Component Software (FACS), Oct 2016, Besançon, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01366641/file/main.pdf BibTex
titre
DAPA: Degradation-Aware Privacy Analysis of Android Apps
auteur
Gianluca Barbon, Agostino Cortesi, Pietro Ferrara, Enrico Steffinlongo
article
STM 2016 - 12th International Workshop on Security and Trust Management, Sep 2016, Heraklion, Greece. pp.32 - 46, ⟨10.1007/978-3-319-46598-2_3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01416504/file/dapa_preprint.pdf BibTex
titre
Stability-Based Adaptation of Asynchronously Communicating Software
auteur
Carlos Canal, Gwen Salaün
article
14th International Conference on Software Engineering and Formal Methods, Jul 2016, Vienne, Austria. ⟨10.1007/978-3-319-41591-8_22⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01359044/file/main.pdf BibTex
titre
Automated Analysis of Asynchronously Communicating Systems
auteur
Lakhdar Akroun, Gwen Salaün, Lina Ye
article
23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. ⟨10.1007/978-3-319-32582-8_1⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01280164/file/Akroun-Salaun-Ye-16.pdf BibTex
titre
On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
auteur
Radu Mateescu, José Ignacio Requeno
article
23rd International SPIN symposium on Model Checking of Software, Apr 2016, Eindhoven, Netherlands. ⟨10.1007/978-3-319-32582-8_13⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01280129/file/Mateescu-Requeno-16.pdf BibTex
titre
DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
auteur
Hugues Evrard
article
TACAS'2016, Apr 2016, Eindhoven, Netherlands. ⟨10.1007/978-3-662-49674-9_34⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01250925/file/Evrard_TACAS_2016.pdf BibTex
titre
Using formal models to cross check an implementation
auteur
Raquel Oliveira, Sophie Dupuy-Chessa, Gaëlle Calvary, Danièle Dadolle
article
Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing System EICS 2016, 2016, Brussels, Belgium, Belgium. pp.126-137, ⟨10.1145/2933242.2933257⟩
Accès au bibtex
BibTex

Special issue

titre
Preface to the Special issue on Formal Methods for Industrial Critical Systems (FMICS'2014)
auteur
Frédéric Lang, Francesco Flammini
article
France. Science of Computer Programming, 118, pp.1-2, 2016, Special Issue on Formal Methods for Industrial Critical Systems (FMICS'2014), ⟨10.1016/j.scico.2016.01.004⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01271895/file/Lang-Flammini-16.pdf BibTex

Books

titre
Preface: Special Issue on Software Verification and Testing (Selected Papers from SAC-SVT'15)
auteur
Gwen Salaün, Mariëlle Stoelinga
article
ACM, 2016, ⟨10.1016/j.scico.2016.10.001⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01419302/file/preface-2.pdf BibTex
titre
Special Issue of the Formal Aspects of Computing Journal on Software Engineering and Formal Methods (SEFM'14)
auteur
Dimitra Giannakopoulou, Gwen Salaün, Michael Butler
article
Springer, 2016, ⟨10.1007/s00165-016-0368-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01419890/file/editorial-sefm14.pdf BibTex

Theses

titre
Formal framework for modelling and verifying globally asynchronous locally synchronous systems
auteur
Fatma Jebali
article
Computation and Language [cs.CL]. Université Grenoble Alpes, 2016. English. ⟨NNT : 2016GREAM036⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-01679311/file/JEBALI_2016_archivage.pdf BibTex

2015

Journal articles

titre
Verification of Plastic Interactive Systems
auteur
Raquel Oliveira, Sophie Dupuy-Chessa, Gaëlle Calvary
article
i-com, 2015, 14 (3), pp.192-204. ⟨10.1515/icom-2015-0036⟩
Accès au bibtex
BibTex
titre
Compositional Verification of Asynchronous Concurrent Systems using CADP
auteur
Hubert Garavel, Frédéric Lang, Radu Mateescu
article
Acta Informatica, 2015, 52 (4), pp.56. ⟨10.1007/s00236-015-0226-1⟩
Accès au bibtex
BibTex
titre
Revisiting sequential composition in process calculi
auteur
Hubert Garavel
article
Journal of Logical and Algebraic Methods in Programming, 2015, ⟨10.1016/j.jlamp.2015.08.001⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01247770/file/main.pdf BibTex

Conference papers

titre
Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
auteur
Wendelin Serwe
article
Proceedings of the first Workshop on Models for Formal Analysis of Real Systems (MARS 2015), Nov 2015, Suva, Fiji. ⟨10.4204/EPTCS.196.6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01227999/file/main.pdf BibTex
titre
Asynchronous Coordination of Stateful Autonomic Managers in the Cloud
auteur
Rim Abid, Gwen Salaün, Noel de Palma, Soguy Mak-Karé Gueye
article
12th International Symposium on Formal Aspects of Components and Systems FACS'2015, Oct 2015, Niterói, Rio de Janeiro, Brazil
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01245754/file/mainFACS.pdf BibTex
titre
Equivalence Checking for Comparing User Interfaces
auteur
Raquel Oliveira, Sophie Dupuy-Chessa, Gaëlle Calvary
article
7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'2015, Jun 2015, Duisburg, Germany. ⟨10.1145/2774225.2774844⟩
Accès au bibtex
BibTex
titre
Plasticity of User Interfaces: Formal Verification of Consistency
auteur
Raquel Oliveira, Sophie Dupuy-Chessa, Gaëlle Calvary
article
7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'2015, Jun 2015, Duisburg, Germany. ⟨10.1145/2774225.2775078⟩
Accès au bibtex
BibTex
titre
Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets
auteur
Hubert Garavel
article
36th International Conference on Application and Theory of Petri Nets and Concurrency PETRI NETS'2015, Jun 2015, Brussels, Belgium. ⟨10.1007/978-3-319-19488-2_9⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01142198/file/main.pdf BibTex
titre
Reasoning in description logics with variables: preliminary results regarding the EL logic.
auteur
Lakhdar Akroun, Lhouari Nourine, Farouk Toumani
article
28th International Workshop on Description Logics, Jun 2015, Athenes, Greece. pp.12
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01163342/file/Akroun-Nourine-Toumani-15.pdf BibTex
titre
Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
auteur
Abderahman Kriouile, Wendelin Serwe
article
21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2015, London, UK, France. pp.708--722, ⟨10.1007/978-3-662-46681-0_62⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01104747/file/main.pdf BibTex
titre
Model-Based Adaptation of Software Communicating via FIFO Buffers
auteur
Carlos Canal, Gwen Salaün
article
18th International Conference on Fundamental Approaches to Software Engineering (FASE 2015), Apr 2015, Londres, United Kingdom. ⟨10.1007/978-3-662-46675-9_17⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01150353/file/main.pdf BibTex
titre
Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes
auteur
Hugues Evrard, Frédéric Lang
article
23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), Mar 2015, Turku, Finland
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01086522/file/EvrardLang14.pdf BibTex
titre
Debugging Process Algebra Specifications
auteur
Gwen Salaün, Lina Ye
article
VMCAI 2015, Jan 2015, Mumbai, India. pp.18, ⟨10.1007/978-3-662-46081-8_14⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01087505/file/main-VMCAI.pdf BibTex

Reports

titre
Compositional Verification of Asynchronous Concurrent Systems using CADP (extended version)
auteur
Hubert Garavel, Frédéric Lang, Radu Mateescu
article
[Research Report] RR-8708, INRIA Grenoble - Rhône-Alpes. 2015
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01138749/file/RR-8708.pdf BibTex

Theses

titre
Formal Specification and Verification of Interactive Systems with Plasticity : Applications to Nuclear-Plant Supervision
auteur
Raquel Araùjo De Oliveira
article
Computation and Language [cs.CL]. Université Grenoble Alpes, 2015. English. ⟨NNT : 2015GREAM025⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-01253619/file/OLIVEIRA_2015_archivage.pdf BibTex
titre
Formal Methods for Functional Verification of Cache-Coherent System-on-Chip
auteur
Abderahman Kriouile
article
Logic in Computer Science [cs.LO]. Université Grenoble Alpes, 2015. English. ⟨NNT : ⟩
Accès au texte intégral et bibtex
https://inria.hal.science/tel-01258784/file/Abderahman_KRIOUILE_PhD_Thesis.pdf BibTex
titre
Méthodes Formelles pour la vérification fonctionnelle des systèmes sur puce cache cohérent
auteur
Abderahman Kriouile
article
Micro and nanotechnologies/Microelectronics. Université Grenoble Alpes, 2015. English. ⟨NNT : 2015GREAM041⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-01280455/file/KRIOUILE_2015_archivage.pdf BibTex
titre
Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones
auteur
Hugues Evrard
article
Génie logiciel [cs.SE]. Université Grenoble Alpes, 2015. Français. ⟨NNT : 2015GREAM020⟩
Accès au texte intégral et bibtex
https://inria.hal.science/tel-01215634/file/Evrard_These.pdf BibTex

2014

Journal articles

titre
Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity
auteur
Radu Mateescu, Anton Wijs
article
Science of Computer Programming, 2014, ⟨10.1016/j.scico.2014.04.004⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01016922/file/Mateescu-Wijs-14.pdf BibTex
titre
Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP
auteur
Etienne Lantreibecq, Wendelin Serwe
article
Science of Computer Programming, 2014, 80, pp.130-149. ⟨10.1016/j.scico.2013.01.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00782069/file/main.pdf BibTex

Conference papers

titre
GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems
auteur
Fatma Jebali, Frédéric Lang, Radu Mateescu
article
Proceedings of the 16th International Conference on Formal Engineering Methods (ICFEM’14), Nov 2014, Luxembourg, Luxembourg. pp.219-234, ⟨10.1007/978-3-319-11737-9_15⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01082348/file/jebali-lang-mateescu-14.pdf BibTex
titre
Adaptation of Asynchronously Communicating Software
auteur
Carlos Canal, Gwen Salaün
article
12th International Conference on Service Oriented Computing (ICSOC 2014), Nov 2014, Paris, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01053682/file/canal_salaun.pdf BibTex
titre
Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip
auteur
Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, Chris Myers
article
19th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2014, Sep 2014, Florence, Italy. pp.48-62, ⟨10.1007/978-3-319-10702-8_4⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01064829/file/fmics2014.pdf BibTex
titre
Quantifying the Parallelism in BPMN Processes using Model Checking
auteur
Radu Mateescu, Gwen Salaün, Lina Ye
article
The 17th International ACM Sigsoft Symposium on Component-Based Software Engineering (CBSE 2014), Jun 2014, Lille, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01016412/file/main.pdf BibTex
titre
Robust Reconfiguration of Cloud Applications
auteur
Francisco Durán, Gwen Salaün
article
The 17th International ACM Sigsoft Symposium on Component-Based Software Engineering (CBSE 2014), Jun 2014, Lille, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01016401/file/cbse80s-salaun-main.pdf BibTex
titre
Formal verification of UI using the power of a recent tool suite
auteur
Raquel Oliveira, Sophie Dupuy-Chessa, Calvary Gaëlle
article
EICS 2014 : Proceedings of the 2014 ACM SIGCHI symposium on Engineering Interactive Computing Systems, Jun 2014, Florence, Italy. pp.235-240, ⟨10.1145/2607023.2610280⟩
Accès au bibtex
BibTex
titre
Modélisation et validation formelle de systèmes globalement asynchrones et localement synchrones
auteur
Fatma Jebali, Mouna Tka Mnad, Christophe Deleuze, Frédéric Lang, Radu Mateescu, Ioannis Parissis
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2014, Paris, France. pp.97--102
Accès au texte intégral et bibtex
https://hal.univ-grenoble-alpes.fr/hal-01007674/file/bluesky.pdf BibTex
titre
A Model-Based Certification Framework for the EnergyBus Standard
auteur
Alexander Graf-Brill, Holger Hermanns, Hubert Garavel
article
34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. pp.84-99, ⟨10.1007/978-3-662-43613-4_6⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01098360/file/main.pdf BibTex
titre
Comparator: A Tool for Quantifying Behavioural Compatibility
auteur
Meriem Ouederni, Gwen Salaün, Javier Cámara, Ernesto Pimentel
article
FASE 2014 - 17th International Conference on Fundamental Approaches to Software Engineering, Apr 2014, Grenoble, France. pp.306-309, ⟨10.1007/978-3-642-54804-8_21⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00934057/file/OSPC-FASE_14.pdf BibTex
titre
Reliable Self-Deployment of Cloud Applications
auteur
Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma
article
SAC 2014 - 29th ACM Symposium on Applied Computing, Mar 2014, Gyeongju, South Korea
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00934042/file/main-SAC14.pdf BibTex

Books

titre
Special Issue on Formal Aspects of Component Software (Selected Papers from FACS'12)
auteur
Corina Pasareanu, Gwen Salaün
article
Corina Pasareanu and Gwen Salaün. Elsevier, pp.3, 2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01016471/file/preface.pdf BibTex
titre
Special Section on Formal Methods for Industrial Critical Systems (Selected Papers from FMICS'11)
auteur
Gwen Salaün, Bernhard Schätz
article
Gwen Salaün; Bernhard Schätz. Elsevier, 80(A), 2014, Science of Computer Programming, ⟨10.1016/j.scico.2013.01.008⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00919803/file/preface_scp_fmics11.pdf BibTex
titre
Special Section on Foundations of Coordination Languages and Software Architectures (Selected Papers from FOCLASA'10)
auteur
Mohammad Reza Mousavi, Gwen Salaün
article
Mousavi, Mohammad Reza; Salaün, Gwen. Elsevier, 80(A), 2014, Science of Computer Programming, ⟨10.1016/j.scico.2012.03.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00919799/file/preface_scp_foclasa10.pdf BibTex
titre
Software Engineering and Formal Methods
auteur
Gwen Salaün, Dimitra Giannakopoulou
article
2014, ⟨10.1007/978-3-319-10431-7⟩
Accès au bibtex
BibTex
titre
Formal Methods for Industrial Critical Systems
auteur
Frédéric Lang, Francesco Flammini
article
2014
Accès au bibtex
BibTex

Reports

titre
Stability of Asynchronously Communicating Systems
auteur
Gwen Salaün, Lina Ye
article
[Research Report] RR-8561, INRIA. 2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01020777/file/RR-8561%20%281%29.pdf https://inria.hal.science/hal-01020777/file/RR-8561.pdf BibTex
titre
GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems (Syntax and Formal Semantics)
auteur
Fatma Jebali, Frédéric Lang, Radu Mateescu
article
[Research Report] RR-8527, INRIA. 2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00983711/file/RR-v34.pdf BibTex
titre
Flooding-Based Algorithm for Behavioural Compatibility Measuring
auteur
Meriem Ouederni, Uli Fahrenberg, Axel Legay, Gwen Salaün
article
[Research Report] Inria Rennes. 2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01088157/file/fase.pdf BibTex

Preprints, Working Papers, ...

titre
Formal Modeling and Verification of GALS Systems Using GRL and CADP
auteur
Fatma Jebali, Frédéric Lang, Eric Léo, Radu Mateescu
article
2014
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01082950/file/etaps-2015.pdf BibTex

2013

Journal articles

titre
Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
auteur
Frederic Lang, Radu Mateescu
article
Logical Methods in Computer Science, 2013, 9 (4)
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00872181/file/Lang-Mateescu-13-final.pdf BibTex
titre
An Experience Report on the Verification of Autonomic Protocols in the Cloud
auteur
Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma, Xavier Etchevers, Olivier Gruber
article
Innovations in Systems and Software Engineering, 2013, ⟨10.1007/s11334-013-0204-0⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00808565/file/main-isse.pdf BibTex
titre
Efficient Optimization of Large Probabilistic Models
auteur
Simon Struck, Matthias Güdemann, Frank Ortmeier
article
Journal of Systems and Software, 2013, ⟨10.1016/j.jss.2013.03.078⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00816636/file/Struck-Gudemann-Ortmeier-13.pdf BibTex
titre
Composition and abstraction of logical regulatory modules: application to multicellular systems
auteur
Nuno D Mendes, Frédéric Lang, Yves-Stan Le Cornec, Radu Mateescu, Grégory Batt, Claudine Chaouiya
article
Bioinformatics, 2013, 29 (6), pp.749-757. ⟨10.1093/bioinformatics/btt033⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00785564/file/Mendes2013.pdf BibTex
titre
CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes
auteur
Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe
article
International Journal on Software Tools for Technology Transfer, 2013, 15 (2), pp.89-107. ⟨10.1007/s10009-012-0244-z⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00715056/file/main.pdf BibTex

Conference papers

titre
Predictability Analysis of Distributed Discrete Event Systems
auteur
Lina Ye, Philippe Dague, Farid Nouioua
article
52nd IEEE Conference on Decision and Control, Dec 2013, Florence, Italy. pp.5009-5015
Accès au texte intégral et bibtex
https://hal.science/hal-00919434/file/sample.pdf BibTex
titre
Compatibility Checking for Asynchronously Communicating Software
auteur
Meriem Ouederni, Gwen Salaün, Tevfik Bultan
article
FACS 2013, Oct 2013, Nanchang, China
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00913665/file/main-facs13.pdf BibTex
titre
Verification of a Dynamic Management Protocol for Cloud Applications
auteur
Rim Abid, Gwen Salaün, Francesco Bongiovanni, Noël de Palma
article
11th International Symposium, ATVA 2013, Dang Van Hung and Mizuhito Ogawa, Oct 2013, Hanoi, Vietnam. pp.178-192, ⟨10.1007/978-3-319-02444-8_14⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00863262/file/main.pdf BibTex
titre
Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip
auteur
Abderahman Kriouile, Wendelin Serwe
article
FMICS - 18th International Workshop on Formal Methods for Industrial Critical Systems, ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS), Sep 2013, Madrid, Spain. pp.108-122
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00858521/file/FMICS_2013_final.pdf BibTex
titre
Analyse formelle du protocole ACE : cohérence de caches des systèmes sur puce
auteur
Abderahman Kriouile, Wendelin Serwe
article
École d'été Temps-Réel 2013, Aug 2013, Toulouse, France. pp.130-133
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00876665/file/main.pdf BibTex
titre
Verification of EB3 Specifications Using CADP
auteur
Dimitris Vekris, Frédéric Lang, Catalin Dima, Radu Mateescu
article
iFM 2013 - 10th International Conference on integrated Formal Methods, Jun 2013, Turku, Finland. ⟨10.1007/978-3-642-38613-8_5⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00768310/file/paper3.pdf BibTex
titre
Formal Verification of Distributed Branching Multiway Synchronization Protocols
auteur
Hugues Evrard, Frédéric Lang
article
15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2013, Florence, Italy. pp.146-160
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00818788/file/Evrard-Lang-13.pdf BibTex
titre
VerChor: A Framework for Verifying Choreographies
auteur
Matthias Güdemann, Pascal Poizat, Gwen Salaün, Alexandre Dumont
article
Fundamental Approaches to Software Engineering 2013, Mar 2013, Rome, Italy. pp.226-230, ⟨10.1007/978-3-642-37057-1_16⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00806788/file/main-fase13.pdf BibTex
titre
PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus
auteur
Radu Mateescu, Gwen Salaün
article
TACAS - 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - 2013, Mar 2013, Rome, Italy. pp.192-198, ⟨10.1007/978-3-642-36742-7_14⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00805533/file/Mateescu-Salaun-13.pdf BibTex
titre
Génération et manipulation d'espaces d'états distribués avec CADP : expériences sur Grid'5000
auteur
Hubert Garavel, Radu Mateescu, Wendelin Serwe
article
Conférence en Parallélisme, Architecture et Système ComPAS'2013, Jan 2013, Grenoble, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00777110/file/main.pdf BibTex

Book sections

titre
Verification of a Self-configuration Protocol for Distributed Applications in the Cloud
auteur
Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, Thierry Coupaye
article
Camara, Javier and de Lemos, Rogerio and Ghezzi, Carlo and Lopes, Antonia. Assurances for Self-Adaptive Systems, Springer, 2013, ⟨10.1007/978-3-642-36249-1_3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00806914/file/main-asas.pdf BibTex

Books

titre
Formal Aspects of Component Software
auteur
Gwen Salaün, Corina Pasareanu
article
2013, ⟨10.1007/978-3-642-35861-6⟩
Accès au bibtex
BibTex

2012

Journal articles

titre
La fiabilité des systèmes devient un défi majeur
auteur
Hubert Garavel, Isabelle Bellin
article
Collection "20 ans d'avancées et de perspectives en sciences du numérique", 2012, 3 p
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00812770/file/La_fiabilitA_des_systA_mes_devient_un_dA_fi_majeur.pdf BibTex
titre
Structural Reconfiguration of Systems under Behavioral Adaptation
auteur
Carlos Canal, Javier Cámara, Gwen Salaün
article
Science of Computer Programming, 2012, 78 (1), pp.46-64
Accès au texte intégral et bibtex
https://hal.science/hal-00734057/file/facs09scp.pdf BibTex
titre
Realizability of Choreographies using Process Algebra Encodings
auteur
Gwen Salaün, Tevfik Bultan, Nima Roohi
article
IEEE Transactions on Services Computing, 2012, 5 (3), pp.290-304
Accès au texte intégral et bibtex
https://hal.science/hal-00726448/file/SBR-TSC-2010.pdf BibTex
titre
On Explicit Substitution with Names
auteur
Kristoffer H. Rose, Roel Bloo, Frederic Lang
article
Journal of Automated Reasoning, 2012, Special Issue: Theory and Applications of Abstraction, Substitution and Naming, 49 (2), pp.275-300. ⟨10.1007/s10817-011-9222-5⟩
Accès au bibtex
BibTex
titre
Interactive specification and verification of behavioral adaptation contracts
auteur
Javier Cámara, Gwen Salaün, Carlos Canal, Meriem Ouederni
article
Information and Software Technology, 2012, 54 (7), pp.701-723
Accès au texte intégral et bibtex
https://hal.science/hal-00694516/file/CSCO-IST3-1.pdf BibTex
titre
A generic framework for n-protocol compatibility checking
auteur
Francisco Durán, Meriem Ouederni, Gwen Salaün
article
Science of Computer Programming, 2012, 77 (7-8), pp.870-886
Accès au texte intégral et bibtex
https://hal.science/hal-00694561/file/DOS-scp09.pdf BibTex
titre
Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols
auteur
Radu Mateescu, Wendelin Serwe
article
Science of Computer Programming, 2012, 78 (7), pp.843-861. ⟨10.1016/j.scico.2012.01.003⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00671321/file/Mateescu-Serwe-12.pdf BibTex
titre
Sequential and distributed on-the-fly computation of weak tau-confluence
auteur
Radu Mateescu, Anton Wijs
article
Science of Computer Programming, 2012, 77 (10-11), pp.1075-1094. ⟨10.1016/j.scico.2011.07.004⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00676451/file/Mateescu-Wijs-12.pdf BibTex
titre
Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques
auteur
Radu Mateescu, Pascal Poizat, Gwen Salaün
article
IEEE Transactions on Software Engineering, 2012, ⟨10.1109/TSE.2011.62⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00717252/file/MPS-TSE-2011.pdf BibTex

Conference papers

titre
Multi-Objective Optimization of Formal Specifications
auteur
Simon Struck, Michael Lipaczewski, Frank Ortmeier, Matthias Güdemann
article
HASE 2012 - 14th High Assurance System Engineering Symposium, Oct 2012, Omaha, United States. pp.201-208, ⟨10.1109/HASE.2012.21⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00735640/file/HASE.pdf BibTex
titre
Counterexample Guided Synthesis of Monitors for Realizability Enforcement
auteur
Matthias Güdemann, Gwen Salaün, Meriem Ouederni
article
Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Oct 2012, Thiruvananthapuram, India. pp.238-253, ⟨10.1007/978-3-642-33386-6_20⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00742159/file/paper.pdf BibTex
titre
Large-Scale Distributed Verification using CADP: Beyond Clusters to Grids
auteur
Hubert Garavel, Radu Mateescu, Wendelin Serwe
article
11th International Workshop on Parallel and Distributed Methods in verifiCation, Sep 2012, London, United Kingdom
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00730668/file/main.pdf BibTex
titre
Trajectory Description Conception for Industrial Robots
auteur
Sergey Alatartsev, Matthias Güdemann, Frank Ortmeier
article
ROBOTIK 2012 - 7th German Conference on Robotics, May 2012, Munich, Germany. pp.365-370
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00727303/file/Robotik2012.pdf BibTex
titre
Verification of a Self-configuration Protocol for Distributed Applications in the Cloud
auteur
Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, Thierry Coupaye
article
27th Symposium On Applied Computing (SAC 2012), Mar 2012, Italy. pp.1278-1283
Accès au texte intégral et bibtex
https://hal.science/hal-00685394/file/SEBCP-SAC12.pdf BibTex
titre
Checking the Realizability of BPMN 2.0 Choreographies
auteur
Pascal Poizat, Gwen Salaün
article
27th Symposium On Applied Computing (SAC 2012), Mar 2012, Italy. pp.1927-1934
Accès au texte intégral et bibtex
https://hal.science/hal-00685393/file/PS-SAC12.pdf BibTex
titre
Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
auteur
Frédéric Lang, Radu Mateescu
article
Tools and Algorithms for the Construction and Analysis of Systems, Mar 2012, Tallinn, Estonia
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00684471/file/Lang-Mateescu-12.pdf BibTex
titre
Unifying Probabilistic and Traditional Formal Model Based Analysis
auteur
Matthias Güdemann, Michael Lipaczewski, Simon Struck, Frank Ortmeier
article
8. Dagstuhl-Workshop MBEES 2012 - Model-Based Development of Embedded Systems, Feb 2012, Dagstuhl, Germany
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00665607/file/Gudemann-Lipaczewski-Struck-et-al-12.pdf BibTex

Books

titre
Preface: Special issue on Foundations of Coordination Languages and Software Architectures (selected papers from FOCLASA'09)
auteur
Gwen Salaün, Marjan Sirjani
article
Gwen Salaün and Marjan Sirjani. Elsevier, 77, pp.3, 2012, ⟨10.1016/j.scico.2011.09.006⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01016438/file/preface_scp_foclasa09.pdf BibTex

Documents associated with scientific events

titre
CADP: A Toolbox for the Construction and Analysis of Distributed Processes
auteur
Hubert Garavel, Frédéric Lang, Radu Mateescu, Gwen Salaün, Wendelin Serwe
article
FM - 18th International Symposium on Formal Methods - 2012, Aug 2012, Paris, France
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00764932/file/Garavel-Lang-Mateescu-et-al-12-b.pdf BibTex
titre
CADP : une boîte à outils pour la conception et l'analyse de systèmes distribués
auteur
Hubert Garavel, Frédéric Lang, Radu Mateescu, Gwen Salaün, Wendelin Serwe
article
Approches Formelles dans l'Assistance au Développement de Logiciels, Jan 2012, Grenoble, France. 2012
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00667288/file/Garavel-Lang-Mateescu-et-al-12.pdf BibTex