Publications HAL du labo/EPI LAAS-VERTICS

2023

Journal articles

titre
Leveraging polyhedral reductions for solving Petri net reachability problems
auteur
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
article
International Journal on Software Tools for Technology Transfer, 2023, 25, pp.95-114. ⟨10.1007/s10009-022-00694-8⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03973463/file/paper.pdf BibTex
titre
A formal toolchain for offline and run-time verification of robotic systems
auteur
Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet
article
Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03683044/file/main_rob.pdf BibTex

Conference papers

titre
Automated Polyhedral Abstraction Proving
auteur
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
article
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023), Jun 2023, Lisbon, Portugal. pp.324-345, ⟨10.1007/978-3-031-33620-1_18⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-04115006/file/paper.pdf BibTex
titre
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
auteur
Nicolas Amat, Silvano Dal Zilio
article
25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.445-453, ⟨10.1007/978-3-031-27481-7_25⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-04007410/file/paper.pdf BibTex

2022

Journal articles

titre
A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking
auteur
Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio
article
Fundamenta Informaticae, 2022, 187 (2-4), pp.103-138. ⟨10.3233/FI-222134⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03455697/file/paper.pdf BibTex

Conference papers

titre
Kong: a Tool to Squash Concurrent Places
auteur
Nicolas Amat, Louis Chauvet
article
43rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2022), Jun 2022, Bergen, Norway. ⟨10.1007/978-3-031-06653-5_6⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03614426/file/paper.pdf BibTex
titre
Property Directed Reachability for Generalized Petri Nets
auteur
Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa
article
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03545594/file/paper.pdf BibTex

2021

Journal articles

titre
Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems
auteur
Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin
article
Journal of Systems and Software, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03017661/file/main_jss.pdf BibTex
titre
RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus
auteur
Ning Ge, Silvano Dal Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang
article
Science of Computer Programming, 2021, 206, pp.102624. ⟨10.1016/j.scico.2021.102624⟩
Accès au bibtex
BibTex
titre
Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond
auteur
Raymond Devillers, Evgeny Erofeev, Thomas Hujsa
article
LNCS Transactions on Petri Nets and Other Models of Concurrency, 2021, Lecture Notes in Computer Science, 12530, pp.75-100. ⟨10.1007/978-3-662-63079-2_4⟩
Accès au bibtex
https://arxiv.org/pdf/1910.14387 BibTex

Conference papers

titre
Accelerating the Computation of Dead and Concurrent Places using Reductions
auteur
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
article
27th International SPIN Symposium on Model Checking of Software, Jul 2021, Aarhus, Denmark. ⟨10.1007/978-3-030-84629-9_3⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03268388/file/paper.pdf BibTex
titre
On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets
auteur
Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio
article
42rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), Jun 2021, Paris (virtual), France. ⟨10.1007/978-3-030-76983-3_9⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-03202111/file/paper.pdf BibTex

2020

Journal articles

titre
Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics
auteur
Mohammed Foughali, Pierre-Emmanuel Hladik
article
Journal of Systems Architecture, 2020, 111, pp.101817. ⟨10.1016/j.sysarc.2020.101817⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02864928/file/main.pdf BibTex
titre
Counting Petri net markings from reduction equations
auteur
Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio
article
International Journal on Software Tools for Technology Transfer, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02125337/file/sttt.pdf BibTex

Conference papers

titre
A New Product Construction for the Diagnosability of Patterns in Time Petri Net
auteur
Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias
article
59th Conference on Decision and Control (CDC) 2020, Dec 2020, Jeju Island (virtual conference), South Korea. ⟨10.1109/CDC42340.2020.9303826⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02989834/file/CDC_2020.pdf BibTex
titre
A Short Overview on Diagnosability of Patterns in Timed Petri Net
auteur
Éric Lubat, Silvano Dal Zilio
article
14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020), Jun 2020, (on line), France
Accès au texte intégral et bibtex
https://hal.science/hal-02899522/file/MOVEP.pdf BibTex
titre
MCC: a Tool for Unfolding Colored Petri Nets in PNML Format
auteur
Silvano Dal Zilio
article
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://hal.laas.fr/hal-02511881/file/main.pdf BibTex
titre
Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites
auteur
Vincent Mussot, Silvano Dal Zilio, Loic Correnson, Serge Rainjonneau, Yves Bardout, Grégoire Scano
article
10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02462058/file/main.pdf BibTex

2019

Journal articles

titre
Verifying parallel dataflow transformations with model checking and its application to FPGAs
auteur
Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, Andrew Wallace
article
Journal of Systems Architecture, 2019, 101, pp.101657. ⟨10.1016/j.sysarc.2019.101657⟩
Accès au bibtex
BibTex
titre
An Interdisciplinary Capstone Design Experience on Critical Embedded Systems using Agile Methods
auteur
Pascal Acco, Guillaume Auriol, Elodie Chanthery, M.-A Détourbe, Pierre Emmanuel Hladik, Didier Le Botlan, N Noullet, Audine Subias
article
Journal sur l'enseignement des sciences et technologies de l'information et des systèmes, 2019, 18 (0001), 23p. ⟨10.1051/j3ea/20190001⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02189482/file/ArticleJ3eA2019_final.pdf BibTex
titre
Analysis and Synthesis of Weighted Marked Graph Petri Nets: Exact and Approximate Methods
auteur
Raymond Devillers, Thomas Hujsa
article
Fundamenta Informaticae, 2019, 169 (1-2), pp.1 - 30. ⟨10.3233/FI-2019-1837⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02332309/file/WMG-FI-DH.pdf BibTex

Conference papers

titre
The tool TWINA construction d'espaces d'états abstrait pour l'intersection de Time Petri nets
auteur
Éric Lubat
article
12ème Colloque sur la Modélisation des Systèmes Réactifs (MSR 2019), Nov 2019, Angers, France
Accès au texte intégral et bibtex
https://hal.science/hal-02432695/file/MSR19_paper_22%20%281%29.pdf BibTex
titre
On Reconciling Schedulability Analysis and Model Checking in Robotics
auteur
Mohammed Foughali
article
MEDI Workshops. 9th International Conference on Model and Data Engineering, Oct 2019, Toulouse, France
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02346015/file/paper_10.pdf BibTex
titre
A State Class Construction for Computing the Intersection of Time Petri Nets Languages
auteur
Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias
article
17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aug 2019, Amsterdam, Netherlands. ⟨10.1007/978-3-030-29662-9_5⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02263832/file/main.pdf BibTex
titre
Statistical Model Checking of Complex Robotic Systems
auteur
Mohammed Foughali, Félix Ingrand, Cristina Seceleanu
article
26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02152286/file/main.pdf BibTex
titre
Synthesis of Weighted Marked Graphs from Circular Labelled Transition Systems
auteur
Raymond Devillers, Evgeny Erofeev, Thomas Hujsa
article
International Workshop on Algorithms & Theories for the Analysis of Event Data 2019, Jun 2019, Aachen, Germany
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02332213/file/ATAED19-DEH.pdf BibTex
titre
Repeatable Decentralized Simulations for Cyber-Physical Systems
auteur
Christophe Reymann, Mohammed Foughali, Simon Lacroix
article
International Conference on Software Quality, Reliability and Security (QRS), Jun 2019, Sofia, Bulgaria
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02156842/file/qrs-66.pdf BibTex
titre
Activité pédagogique sur la création d'un jeu d'évasion
auteur
Guillaume Auriol, Sonia Ben Dhia, Elodie Chanthery, Pierre-Emmanuel Hladik, Didier Le Botlan, G. Le Corre, C. Maranges, David Vignolles
article
6ème Colloque Pédagogie & Formation - groupe INSA, May 2019, Bourges, France
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-02307883/file/Colloque_p_dagogique_INSA.pdf BibTex
titre
Graphical program transformations for embedded systems
auteur
Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, Andrew Wallace
article
34th ACM/SIGAPP Symposium on Applied Computing (SAC), Apr 2019, Limassol, Cyprus. pp.647-649, ⟨10.1145/3297280.3297555⟩
Accès au bibtex
BibTex
titre
Presentation of the 9th Edition of the Model Checking Contest
auteur
Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal Zilio, Francesco Gallà, Lom Messan Hillah, Francis Hulin-Hubard, Peter Gjøl Jensen, Loïg Jezequel, Fabrice Kordon, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Andrew Miner, Emmanuel Paviot-Adet, Jiří Srba, Yann Thierry-Mieg, Tom van Dijk, Karsten Wolf
article
Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III, Apr 2019, Prague, Czech Republic. pp.50-68, ⟨10.1007/978-3-030-17502-3_4⟩
Accès au bibtex
BibTex

Book sections

titre
Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach
auteur
Raymond Devillers, Evgeny Erofeev, Thomas Hujsa
article
Transactions on Petri Nets and Other Models of Concurrency XIV, Springer, pp.172-191, 2019, 978-3-662-60650-6. ⟨10.1007/978-3-662-60651-3_7⟩
Accès au bibtex
https://arxiv.org/pdf/1911.00474 BibTex

2018

Conference papers

titre
Petri Net Reductions for Counting Markings
auteur
Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio
article
International Symposium on Model Checking Software (SPIN 2018), Jun 2018, Malaga, Spain. ⟨10.1007/978-3-319-94111-0_4⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01822078/file/spin.pdf BibTex
titre
Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms
auteur
Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet
article
FormaliSE: 6th International Conference on Formal Methods in Software Engineering, Jun 2018, Gothenburg, Sweden
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01778960/file/paper.pdf BibTex
titre
A Brute-Force Schedulability Analysis for Formal Model under Logical Execution Time Assumption
auteur
Pierre-Emmanuel Hladik
article
The 33rd ACM/SIGAPP Symposium On Applied Computing (SAC), Apr 2018, Pau, France. 13p
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01717293/file/SAC2017.pdf BibTex
titre
Timed Formal Model and Verification of Satellite FDIR in Early Design Phase
auteur
Alexandre Albore, Silvano Dal Zilio, Marie de Roquemaurel, Christel Seguin, Pierre Virelizier
article
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France. 10p
Accès au texte intégral et bibtex
https://hal.science/hal-01709008/file/2018_SE_Albore_Timed%20Formal%20Model%20and%20Verification%20of%20Satellite%20FDIR%20in%20Early%20Design%20Phase_ERTS2.pdf BibTex

2017

Conference papers

titre
Formal Verification of User-Level Real-Time Property Patterns
auteur
Ning Ge, Marc Pantel, Silvano Dal Zilio
article
11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017), Sep 2017, Sophia Antipolis, France. 8p
Accès au texte intégral et bibtex
https://hal.science/hal-01589479/file/tase2017.pdf BibTex
titre
A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica
auteur
Alexandre Albore, Silvano Dal Zilio, Guillaume Infantes, Christel Seguin, Pierre Virelizier
article
Model-Based Safety and Assessment. IMBSA 2017, Sep 2017, Trento, Italy. 15p., ⟨10.1007/978-3-319-64119-5_10⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01693391/file/imbsa2017.pdf BibTex

2016

Journal articles

titre
Symmetry reduction for time Petri net state classes
auteur
Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat
article
Science of Computer Programming, 2016, Science of Computer Programming, 132 (Part 2), pp.209 - 225. ⟨10.1016/j.scico.2016.08.008⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01561994/file/symmetries.pdf BibTex
titre
De l'illustration du guidage à l'optimisation d'un plan par un robot Lego Mindstorm NXT
auteur
Elodie Chanthery, G Le Corre, Pierre-Emmanuel Hladik
article
Journal sur l'enseignement des sciences et technologies de l'information et des systèmes, 2016, 15, ⟨10.1051/j3ea/2016006⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01392601/file/j3ea160006.pdf BibTex

Conference papers

titre
Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots
auteur
Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand, Anthony Mallet
article
18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan
Accès au texte intégral et bibtex
https://hal.science/hal-01346080/file/paper.pdf BibTex
titre
Solving Language Equations Using Flanked Automata
auteur
Florent Avellaneda, Silvano Dal Zilio, Jean-Baptiste Raclet
article
ATVA 2016: Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. pp.106 - 121, ⟨10.1007/978-3-319-46520-3_7⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01202702/file/ffa.pdf https://hal.science/hal-01202702/file/dessin.pdf https://hal.science/hal-01202702/file/restable.pdf BibTex
titre
Model-Driven Approach to the Optimal Configuration of Time-Triggered Flows in a TTEthernet Network
auteur
Sofiene Beji, Abdelouahed Gherbi, John Mullins, Pierre-Emmanuel Hladik
article
9th System Analysis and Modelling (SAM 2016), Oct 2016, Saint-Malo, France. ⟨10.1007/978-3-319-46613-2_11⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01496891/file/model-driven-approach.pdf BibTex
titre
Building Confidence on Formal Verification Models
auteur
Pierre-Alain Bourdil, Eric Jenn, Silvano Dal Zilio
article
Fast Abstracts at International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Sep 2016, Trondheim, Norway
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01369144/file/2-bourdil-jenn-dalzilio.pdf BibTex
titre
Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées
auteur
Pierre-Emmanuel Hladik, Silvano Dal Zilio, Olivier Pasquier, Sébastien Pillement, Bernard Berthomieu
article
15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jun 2016, Besançon, France
Accès au texte intégral et bibtex
https://hal.science/hal-01331726/file/main.pdf https://hal.science/hal-01331726/file/chaine.pdf BibTex

Books

titre
Quaternions réels duaux et complexes
auteur
Jean Hladik, Pierre-Emmanuel Hladik
article
Ellipses Marketing, 2016, 978-2340010468
Accès au bibtex
BibTex

2015

Journal articles

titre
Algorithmes pour l’ordonnancement temps réel multiprocesseur
auteur
Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche
article
Journal Européen des Systèmes Automatisés (JESA), 2015, 48 (7-8), pp.613-639. ⟨10.3166/JESA.48.613-63⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01221711/file/JESA_draft.pdf BibTex

Conference papers

titre
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
auteur
Silvano Dal Zilio, Bernard Berthomieu
article
1st International Conference on Theoretical Computer Science (TTCS), Aug 2015, Teheran, Iran. pp.90-104, ⟨10.1007/978-3-319-28678-5_7⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01202799/file/article.pdf BibTex
titre
Simulation of Real-Time Scheduling Algorithms with Cache Effects
auteur
Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche, Silvano Dal Zilio
article
6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems, Jul 2015, Lund, Sweden. 6p
Accès au texte intégral et bibtex
https://hal.science/hal-01232512/file/waters.pdf BibTex
titre
Symmetry reduced state classes for Time Petri nets
auteur
Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat
article
30th Annual ACM Symposium on Applied Computing, Apr 2015, Salamanca, Spain. pp.1751-1758, ⟨10.1145/2695664.2695803⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01275316/file/bourdilsymmetries.pdf BibTex

2014

Journal articles

titre
A Formal Framework to Specify and Verify Real Time Properties on Critical Systems
auteur
Didier Le Botlan, Silvano Dal Zilio, Nouha Abid
article
International Journal of Critical Computer-Based Systems, 2014, 5 (1/2), pp 4-30. ⟨10.1504/IJCCBS.2014.059593⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00941248/file/alternate.pdf BibTex

Conference papers

titre
Model-Checking Real-Time Properties of an Auto Flight Control System Function
auteur
Pierre-Alain Bourdil, Bernard Berthomieu, Éric Jenn
article
IEEE International Symposium on Software Reliability Engineering, Nov 2014, Naples, Italy. ⟨10.1109/ISSREW.2014.40⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01949464/file/autoflight-control-issre14.pdf BibTex
titre
Automated Failure Analysis in Model Checking based on Data Mining
auteur
Ning Ge, Marc Pantel, Xavier Crégut
article
4th International Conference On Model and Data Engineering, Sep 2014, Larnaca, Cyprus. pp.13-28, ⟨10.1007/978-3-319-11587-0_4⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03252269/file/Automated%20Failure%20Analysis%20in%20Model%20Checking%20based%20on%20Data%20Mining.pdf BibTex
titre
Time Petri Nets with Dynamic Firing Dates: Semantics and Applications
auteur
Silvano Dal Zilio, Lukasz Fronc, Bernard Berthomieu, François Vernadat
article
12th International Conference, FORMATS 2014, Sep 2014, Florence, Italy. pp 85-99, ⟨10.1007/978-3-319-10512-3_7⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00984354/file/dyntpn.pdf BibTex
titre
SimSo: A Simulation Tool to Evaluate Real-Time Multiprocessor Scheduling Algorithms
auteur
Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche
article
5th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS), Jul 2014, Madrid, Spain. 6 p
Accès au texte intégral et bibtex
https://hal.science/hal-01052651/file/waters_cheramy.pdf BibTex
titre
Simulation of Real-Time Scheduling with Various Execution Time Models
auteur
Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche, Sébastien Dubé
article
9th IEEE International Symposium on Industrial Embedded Systems (SIES), Jun 2014, Pise, Italy
Accès au texte intégral et bibtex
https://hal.science/hal-01052656/file/wip_sies2014.pdf BibTex
titre
Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre
auteur
Bernard Berthomieu, Silvano Dal Zilio, Lukasz Fronc
article
4th International ABZ Conference, Jun 2014, France. pp.110-125
Accès au texte intégral et bibtex
https://hal.science/hal-00967422/file/main.pdf BibTex
titre
Formalisation et génération d'injections
auteur
Eric Alata, Didier Le Botlan
article
9ème édition de la conférence Francophone SARSSI, May 2014, Lyon, France. 13p
Accès au texte intégral et bibtex
https://hal.science/hal-01022924/file/sarssi.pdf BibTex

2013

Journal articles

titre
Optimal Design of Virtual Links in AFDX Networks
auteur
Ahmad Al Sheikh, Olivier Brun, Maxime Chéramy, Pierre-Emmanuel Hladik
article
Real-Time Systems, 2013, 49 (3), 31p. ⟨10.1007/s11241-012-9171-z⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00665755/file/Optimal_design.pdf BibTex

Conference papers

titre
Simulation d'ordonnancement temps réel avec prise en compte de l'impact des caches
auteur
Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche
article
École d'été Temps Réel 2013, Aug 2013, Toulouse, France
Accès au texte intégral et bibtex
https://hal.science/hal-00870076/file/etr13.pdf BibTex
titre
Simulation of Real-Time Multiprocessor Scheduling with Overheads
auteur
Maxime Chéramy, Anne-Marie Déplanche, Pierre-Emmanuel Hladik
article
International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2013), Jul 2013, Reykjavik, Iceland. pp. 5-14
Accès au texte intégral et bibtex
https://hal.science/hal-00815502/file/camera-ready.pdf BibTex

2012

Conference papers

titre
An Experiment on Parallel Model Checking of a CTL Fragment
auteur
Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu
article
10th International Symposium, ATVA 2012, Automated Technology for Verification and Analysis, Oct 2012, Thiruvananthapuram, India. pp.284-299, ⟨10.1007/978-3-642-33386-6_23⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00782354/file/paper68.pdf BibTex
titre
Real-Time Specification Patterns and Tools
auteur
Nouha Abid, Silvano Dal Zilio, Didier Le Botlan
article
17th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2012, Aug 2012, Paris, France. pp. 1-15, ⟨10.1007/978-3-642-32469-7_1⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00782649/file/fmics2012patterns.pdf BibTex
titre
A Verified Approach for Checking Real-Time Specification Patterns
auteur
Nouha Abid, Silvano Dal Zilio, Didier Le Botlan
article
VECoS 2012, 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, Aug 2012, France. pp.11
Accès au texte intégral et bibtex
https://hal.science/hal-00782647/file/article.pdf BibTex
titre
A Verified Approach to Checking Real-Time Patterns on Fiacre Programs
auteur
Nouha Abid, Silvano Dal Zilio
article
Doctoral Symposium of FM 2012, Aug 2012, Paris, France
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01790120/file/abid-dsfm2012.pdf BibTex

2010

Conference papers

titre
Analyse d'un modèle AADL à l'aide de Pola
auteur
Pierre-Emmanuel Hladik, Florent Peres, Xiaomu Shi
article
10es journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2010, Poitiers, France. p. 239--243
Accès au texte intégral et bibtex
https://hal.science/hal-00493726/file/aadl_pola_Vcourte_final.pdf BibTex
titre
Formal Verification of AADL models with Fiacre and Tina
auteur
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, M Filali, Pierre Gaufillet, Sebastien Heim, François Vernadat
article
ERTSS 2010 - Embedded Real-Time Software and Systems, 3AF Midi-Pyrénées: the French Society of Aeronautic and Aerospace; SEE: the French Society for Electricity, Electronics, and Information & Communication Technologies; SIA: the French Society of Automobive Engineers, May 2010, Toulouse, France. pp.1-9, ⟨10.5281/zenodo.32930⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00494348/file/aadlTopcased.pdf BibTex
titre
Verification Based Development Process for Embedded Systems
auteur
T Correa, L. B. Becker, Jean-Paul Bodeveix, J-M Farines, M Filali, François Vernadat
article
European conference on Embedded Real Time Software & Systems (ERTS2 2010), 3AF Midi-Pyrénées: the French Society of Aeronautic and Aerospace; SEE: the French Society for Electricity, Electronics, and Information & Communication Technologies; SIA: the French Society of Automobive Engineers, May 2010, Toulouse, France. pp.1-10
Accès au texte intégral et bibtex
https://hal.science/hal-02267842/file/6C-2.pdf BibTex
titre
Langage intermédiaire et transformations de modèles pour le développement de systèmes temps-réel : retour d'expérience sur la chaîne de vérification formelle Fiacre
auteur
Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, M Filali, Marc Pantel, François Vernadat
article
IDM 2010 : journées sur l'Ingénierie Dirigée par les Modèles, Mar 2010, Pau, France
Accès au texte intégral et bibtex
https://hal.science/hal-00492327/file/idm2010.pdf BibTex

2009

Conference papers

titre
Formal Verification of AADL Specifications in the Topcased Environment
auteur
Bernard Berthomieu, J.-P Bodeveix, Christelle Chaudet, Silvano Dal Zilio, M Filali, François Vernadat
article
Reliable Software Technologies - Ada Europe 2009, Jun 2009, Brest, France. 15p., ⟨10.1007/978-3-642-01924-1_15⟩
Accès au texte intégral et bibtex
https://hal.laas.fr/hal-01790208/file/aadltina.pdf BibTex

2008

Conference papers

titre
Fiacre: an Intermediate Language for Model Verification in the Topcased Environment
auteur
Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, M Filali, Hubert Garavel, Pierre Gaufillet, Frederic Lang, François Vernadat
article
4th European Congress ERTS Embedded Real Time Software (ERTS 2008), SEE : Société de l'électricité, de l'électronique et des technologies de l'information et de la communication; 3AF : Association Aéronautique et Astronautique de France, Jan 2008, Toulouse, France. pp.1-8
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00262442/file/Berthomieu-Bodeveix-Farail-et-al-08.pdf BibTex

2006

Conference papers

titre
Behavioural descriptions in architecture description languages Application to AADL
auteur
Jean-Paul Bodeveix, P Dissaux, M Filali, P Farail, P Gaufillet, François Vernadat
article
3rd European Congress on Embedded Real Time Software (ERTS 2006), Jan 2006, Toulouse, France
Accès au texte intégral et bibtex
https://hal.science/hal-02270356/file/1B3_M.Filali_Feria.pdf BibTex

2004

Conference papers

titre
Decomposition and learning for a hard real-time task allocating problem
auteur
Hadrien Cambazard, Pierre-Emmanuel Hladik, Anne-Marie Déplanche, Narendra Jussien, Yvon Trinquet
article
CORS/INFORMS Joint International Meeting, 2004, Banff, Alberta, Canada
Accès au bibtex
BibTex