VERification des Systèmes Temporisés CritiqueS

- vertics -

L'équipe Vertics s'intéresse à la vérification formelle de systèmes critiques présentant de fortes exigences en termes de contraintes temporelles. Nos recherches portent principalement sur le model-checking, l'ordonnancement des systèmes temps réel, ainsi que sur l'intégration de ces techniques.

L’AGENDA DE L’ÉQUIPE

22.11.23 - MSR '23 14e colloque sur la modélisation des systèmes réactifs

Tous les événements de l'équipe

RESPONSABLE

Silvano Dal Zilio

Responsable

Silvano
Dal Zilio

Cadre scientifique

Tomasz
Kloda

Didier
Le Botlan

François
Vernadat

Stagiaire

Adrien
Jakubiak

Dernières Publications

2024

Communications dans un congrès

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability. Verification, Model Checking, and Abstract Interpretation. VMCAI 2024, Jan 2024, London, United Kingdom. pp.101-123, ⟨10.1007/978-3-031-50524-9_5⟩. ⟨hal-04375443⟩

2023

Articles dans une revue

Jiyang Chen, Tomasz Kloda, Rohan Tabish, Ayoosh Bansal, Chien-Ying Chen, et al.. SchedGuard++: Protecting against Schedule Leaks Using Linux Containers on Multi-Core Processors. ACM Transactions on Cyber-Physical Systems, 2023, 7 (1), pp.1-25. ⟨10.1145/3565974⟩. ⟨hal-04235349⟩

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Leveraging polyhedral reductions for solving Petri net reachability problems. International Journal on Software Tools for Technology Transfer, 2023, 25, pp.95-114. ⟨10.1007/s10009-022-00694-8⟩. ⟨hal-03973463⟩

Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet. A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩. ⟨hal-03683044v2⟩

Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, et al.. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). Dagstuhl Artifacts Series, 2023, 9 (1), ⟨10.4230/DARTS.9.1.4⟩. ⟨hal-04254710⟩

Nicolas Amat, Pierre Bouvier, Hubert Garavel. A Toolchain to Compute Concurrent Places of Petri Nets. 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⟩. ⟨hal-04392784⟩

Communications dans un congrès

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Automated Polyhedral Abstraction Proving. 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⟩. ⟨hal-04115006⟩

Nicolas Amat, Silvano Dal Zilio. SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.445-453, ⟨10.1007/978-3-031-27481-7_25⟩. ⟨hal-04007410⟩

Autres documents

Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. Polyhedral Reductions for Petri nets. Modélisation des Systèmes Réactifs (MSR'23), Nov 2023, Toulouse, France. , 2023. ⟨hal-04355257⟩

Pré-publications, documents de travail

Bernard Berthomieu, Dmitry A Zaitsev. Sleptsov Nets are Turing-complete. 2023. ⟨hal-04139308⟩

2022

Articles dans une revue

Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio. A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking. Fundamenta Informaticae, 2022, 187 (2-4), pp.103-138. ⟨10.3233/FI-222134⟩. ⟨hal-03455697v2⟩

Communications dans un congrès

Nicolas Amat, Louis Chauvet. Kong: a Tool to Squash Concurrent Places. 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⟩. ⟨hal-03614426⟩

Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩. ⟨hal-03545594⟩

2021

Articles dans une revue

Raymond Devillers, Evgeny Erofeev, Thomas Hujsa. Efficient Synthesis of Weighted Marked Graphs with Circular Reachability Graph, and Beyond. 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⟩. ⟨hal-02348494⟩

Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin. Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems. Journal of Systems and Software, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩. ⟨hal-03017661v4⟩

Ning Ge, Silvano Dal Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang. RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus. Science of Computer Programming, 2021, 206, pp.102624. ⟨10.1016/j.scico.2021.102624⟩. ⟨hal-03187896⟩

Communications dans un congrès

Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio. On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets. 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⟩. ⟨hal-03202111⟩

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Accelerating the Computation of Dead and Concurrent Places using Reductions. 27th International SPIN Symposium on Model Checking of Software, Jul 2021, Aarhus, Denmark. ⟨10.1007/978-3-030-84629-9_3⟩. ⟨hal-03268388⟩

2020

Articles dans une revue

Mohammed Foughali, Pierre-Emmanuel Hladik. Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics. Journal of Systems Architecture, 2020, 111, pp.101817. ⟨10.1016/j.sysarc.2020.101817⟩. ⟨hal-02864928v3⟩

Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio. Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩. ⟨hal-02125337⟩

Communications dans un congrès

Silvano Dal Zilio. MCC: a Tool for Unfolding Colored Petri Nets in PNML Format. 41st International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2020, Paris, France. ⟨hal-02511881⟩

Vincent Mussot, Silvano Dal Zilio, Loic Correnson, Serge Rainjonneau, Yves Bardout, et al.. Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France. ⟨hal-02462058⟩

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias. A New Product Construction for the Diagnosability of Patterns in Time Petri Net. 59th Conference on Decision and Control (CDC) 2020, Dec 2020, Jeju Island (virtual conference), South Korea. ⟨10.1109/CDC42340.2020.9303826⟩. ⟨hal-02989834⟩

Éric Lubat, Silvano Dal Zilio. A Short Overview on Diagnosability of Patterns in Timed Petri Net. 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020), Jun 2020, (on line), France. ⟨hal-02899522⟩

Pré-publications, documents de travail

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. On the Petri Nets with a Single Shared Place and Beyond. 2020. ⟨hal-02992541⟩

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. Checking marking reachability with the state equation in Petri net subclasses. 2020. ⟨hal-02992521⟩

2019

Articles dans une revue

Pascal Acco, Guillaume Auriol, Elodie Chanthery, M.-A Détourbe, Pierre Emmanuel Hladik, et al.. An Interdisciplinary Capstone Design Experience on Critical Embedded Systems using Agile Methods. Journal sur l'enseignement des sciences et technologies de l'information et des systèmes, 2019, 18 (0001), 23p. ⟨10.1051/j3ea/20190001⟩. ⟨hal-02189482⟩

Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, et al.. Verifying parallel dataflow transformations with model checking and its application to FPGAs. Journal of Systems Architecture, 2019, 101, pp.101657. ⟨10.1016/j.sysarc.2019.101657⟩. ⟨hal-02347401⟩

Raymond Devillers, Thomas Hujsa. Analysis and Synthesis of Weighted Marked Graph Petri Nets: Exact and Approximate Methods. Fundamenta Informaticae, 2019, 169 (1-2), pp.1 - 30. ⟨10.3233/FI-2019-1837⟩. ⟨hal-02332309⟩

Chapitres d’ouvrages

Raymond Devillers, Evgeny Erofeev, Thomas Hujsa. Synthesis of Weighted Marked Graphs from Constrained Labelled Transition Systems: A Geometric Approach. 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⟩. ⟨hal-02348962⟩

Communications dans un congrès

Éric Lubat. The tool TWINA construction d'espaces d'états abstrait pour l'intersection de Time Petri nets. 12ème Colloque sur la Modélisation des Systèmes Réactifs (MSR 2019), Nov 2019, Angers, France. ⟨hal-02432695⟩

Raymond Devillers, Evgeny Erofeev, Thomas Hujsa. Synthesis of Weighted Marked Graphs from Circular Labelled Transition Systems. International Workshop on Algorithms & Theories for the Analysis of Event Data 2019, Jun 2019, Aachen, Germany. ⟨hal-02332213⟩

Mohammed Foughali, Félix Ingrand, Cristina Seceleanu. Statistical Model Checking of Complex Robotic Systems. 26th International SPIN Symposium on Model Checking of Software, Jul 2019, Beijing, China. ⟨hal-02152286⟩

Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal Zilio, Francesco Gallà, et al.. Presentation of the 9th Edition of the Model Checking Contest. 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⟩. ⟨hal-02094047⟩

Christophe Reymann, Mohammed Foughali, Simon Lacroix. Repeatable Decentralized Simulations for Cyber-Physical Systems. International Conference on Software Quality, Reliability and Security (QRS), Jun 2019, Sofia, Bulgaria. ⟨hal-02156842⟩

Mohammed Foughali. On Reconciling Schedulability Analysis and Model Checking in Robotics. MEDI Workshops. 9th International Conference on Model and Data Engineering, Oct 2019, Toulouse, France. ⟨hal-02346015⟩

Guillaume Auriol, Sonia Ben Dhia, Elodie Chanthery, Pierre-Emmanuel Hladik, Didier Le Botlan, et al.. Activité pédagogique sur la création d'un jeu d'évasion. 6ème Colloque Pédagogie & Formation - groupe INSA, May 2019, Bourges, France. ⟨hal-02307883⟩

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias. A State Class Construction for Computing the Intersection of Time Petri Nets Languages. 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aug 2019, Amsterdam, Netherlands. ⟨10.1007/978-3-030-29662-9_5⟩. ⟨hal-02263832⟩

Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, et al.. Graphical program transformations for embedded systems. 34th ACM/SIGAPP Symposium on Applied Computing (SAC), Apr 2019, Limassol, Cyprus. pp.647-649, ⟨10.1145/3297280.3297555⟩. ⟨hal-02305621⟩

Autres documents

Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand. On the Semantics of the GenoM3 Framework. Rapport LAAS n° 19036. 2019. ⟨hal-01992470⟩

Participation au pôle de compétitivité Aerospace Valley, pour l’écosystème Systèmes Embarqués et Communicants (SEC)
Membre du groupe de travail IFSE (Ingéniérie Formelle des Systèmes Embarqués) au sein du RTRA STAE (Sciences et Technologies pour l'Aéronautique et l'Espace). Voir nos journées annuelles FAC (pour Formalisation des Activités Concurrentes)
Co-organisateur du cycle de conférences FMF (Forum Méthodes Formelles)

L’équipe Vertics développe deux outils logiciels principaux: Tina, une boîte à outils pour l'analyse de Time Petri Nets et Frac, un compilateur pour le langage de spécification Fiacre.

Tina

La Boîte à outils TINA est un ensemble d’outils pour l'édition et l'analyse des réseaux de Petri et de leurs extensions. En particulier. Tina peut gérer des réseaux de Petri temporels (TPN), des priorités, des arcs inhibiteurs, ainsi qu'une extension des TPN avec data processing appelée TTS.

Tina comprend un éditeur et une interface utilisateur graphique (nd) pour les TPN et les automates; des simulateurs et des outils de génération d'espaces d'états (tina etsift); des outils d'analyse structurelle (struct); et des model-checkers pour LTL (selt), ainsi que pour CTL* et un fragment existentiel du μ calcul (muse).

sift est une version spécialisée de tina prenant en charge la vérification à la volée des propriétés d'accessibilité. Si sift offre moins d’options que tina, il est généralement plus rapide et consomme beaucoup moins d'espace mémoire.

FIACRE

FIACRE est un langage formel intermédiaire pour la description des activités concurrentes avec contraintes temps réel. Fiacre est un langage défini formellement qui peut représenter à la fois, de manière compositionnelle, le comportement et les aspects temporels des systèmes distribués. Nous fournissons un compilateur (frac) capable de générer un modèle TTS à partir d'une spécification Fiacre donnée. Ce modèle TTS peut ensuite être utilisé avec Tina. Nous avons récemment étendu la langue avec: des fonctions du premier ordre; et des propriétés de vérification temps-réels.

Divers

Nous distribuons également plusieurs prototypes:

AADL2Fiacre: un plugin Eclipse, compatible OSATE, pour générer des spécifications Fiacre (comportementales) à partir d’un Modèle AADL utilisant l'Annexe Comportementale.
SimSo (Simulation of Multiprocessor Scheduling with Overheads): un simulateur de planification temps réel pour architectures multiprocesseurs prenant en compte, à travers des modèles statistiques, l'effet des changements de contexte et de l'accès concurrent aux caches. Le moyen le plus simple d’évaluer le simulateur est d'utiliser SimSo Web, une interface complète de SimSo sur le Web.
Twina: un outil d'analyse du « produit » de deux réseaux de Petri temporels (TPN). L’objectif principal de Twina est de calculer une représentation utilisable de l’intersection du language de deux TPN.
Ramona: un outil d'analyse en temps réel de systèmes de RAte MONotonic tAsks. Son objectif principal est de vérifier l'ordonnancabilité d'un ensemble de tâches périodiques en utilisant certaines hypothèses sur leurs exécutions; plus spécifiquement l'utilisation d'un sdcheduler à priorité fixe et d'une modèle d'exécution avec temps logique (LET).
MCC: un outil pour déplier des réseaux de Petri (colorés) pouvant être appliqués sur les modèles utilisés dans le Model-Checking Contest.