VERification of TIme Critical Systems

- vertics -


*Members of Vertics are now part of the new research team TRUST* The Vertics team focuses on the formal verification of time-critical systems. Our research focuses on enhancing model-checking techniques, scheduling real-time systems, and integrating our methods into existing engineering processes.


Latest publications

2024

Conference papers

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

Journal articles

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⟩

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⟩

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⟩

Conference papers

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⟩

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 (Invited Paper). 35th Euromicro Conference on Real-Time Systems (ECRTS 2023), Jul 2023, Vienne, Austria. ⟨10.4230/LIPIcs.ECRTS.2023.19⟩. ⟨hal-04654624⟩

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⟩

Other 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⟩

Preprints, Working Papers, ...

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

2022

Journal articles

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⟩

Conference papers

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⟩

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⟩

2021

Journal articles

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⟩

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⟩

Conference papers

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

Journal articles

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⟩

Conference papers

É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⟩

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⟩

É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⟩

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⟩

Preprints, Working Papers, ...

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

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

2019

Journal articles

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⟩

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⟩

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⟩

Book sections

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⟩

Conference papers

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⟩

É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⟩

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⟩

Other documents

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

  • Participation to the Aerospace Valley competitiveness cluster, for the Embedded and Communicating Systems (SEC) ecosystem.
  • Member of the IFSE (Ingéniérie Formelle des Systèmes Embarqués) working group within the RTRA STAE (Sciences et Technologies pour l'Aéronautique et l'Espace).
  • Co-organizer of the FMF conference series (Forum Méthodes Formelles)

The Vertics team develops two main software tools: Tina, a toolbox for the analysis of Time Petri Nets, and Frac, the Fiacre compiler.

Tina

The TINA toolbox is a set of tools for the edition and analysis of time Petri Nets and their extensions. In particular it can handle Time Petri Nets (TPN), priorities, inhibitor arcs, and an extension of TPN with data handling called TTS.

Tina includes an editor and GUI (nd) for Time Petri Nets and Automata; stepper simulators and state space generation tools (tina and sift); structural analysis tools (struct); and model-checkers for state/event LTL (selt), and for CTL* and an existential fragment of μ calculus (muse).

sift is a specialized version of tina supporting in addition on the fly verification of reachability properties. If offers less options than tina but is typically faster and requires considerably less space.

FIACRE

FIACRE is an Intermediate Formal language for the description of concurrent activities with real-time constraints. It is a formally defined language for representing compositionaly both the behavioral and timing aspects of embedded and distributed systems for formal verification and simulation purposes. We provide a compiler (frac) that is able to generate a TTS model from a given Fiacre specification. This TTS model can then be used with Tina. We have recently extended the language with: native functions; and real-time verification patterns, that is a possibility to define timed temporal properties directly within a specification.

Miscellaneous

We also distribute several prototypes:

  • AADL2Fiacre: an OSATE compliant Eclipse plugin for generating Fiacre (behavioral) specifications from an AADL model using the Behavioral Annex.
  • SimSo (Simulation of Multiprocessor Scheduling with Overheads): is a scheduling simulator for real-time multiprocessor architectures that takes into account some scheduling overheads (scheduling decisions, context switches) and the impact of caches through statistical models. The easiest way to evaluate the simulator is to use SimSo Web, a full browser interface of SimSo.
  • Twina: a tool for analyzing the “product” of two Time Petri Nets (TPN), with possibly inhibitor and read arcs. Its main objective is to compute a usable representation of the intersection of two net languages; meaning the intersection of the (timed) languages obtained from the executions of two TPN, in which transitions with the same labels are fired at the same date.
  • Ramona: a tool for analyzing real-time properties of systems of RAte MONotonic tAsks. Its main objective is to check the schedulabity of a set of periodic tasks using some hypothesis on the behavior; more specifically the use of fixed priority scheduling and a Logical Execution Time (LET) model.
  • MCC: a tool to unfold high-level (colored) Petri Nets that can be applied on models used in the Model-Checking Contest.

REJOINDRE

Notre équipe de recherche

Pour plus d’informations sur les offres d’emploi, vous pouvez contacter