About me

I am a senior researcher at LAAS-CNRS, in Toulouse. My research interests include the formal verification of concurrent and distributed systems; methods and tools for checking the safety of critical embedded systems; concurrency semantics, and in particular mobile and higher-order process calculi; as well as type systems and static analysis.

I lead the Verification of Time Critical Systems (VERTICS) group, which develops new verification methods and tools for checking properties of critical systems having strong temporal and timing requirements.

Interests

  • Formal Methods
  • Model-Checking
  • Safety Critical Embedded Systems
  • Process Calculi

Recent Publications

More publications »

My publications tracked by DBLP

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias (2020). A New Product Construction for the Diagnosability of Patterns in Time Petri Net. In Proc. of CDC 2020.

PDF Project

Éric Lubat, Silvano Dal Zilio (2020). A Short Overview on Diagnosability of Patterns in Timed Petri Net. In Proc. of MOVEP 2020.

PDF Project

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (2020). Checking marking reachability with the state equation in Petri net subclasses. unpublished.

Project

Silvano Dal Zilio (2020). MCC: a Tool for Unfolding Colored Petri Nets in PNML Format. In Proc. of ICATPN 2020.

PDF Project DOI

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (2020). On the Petri Nets with a Single Shared Place and Beyond. unpublished.

Project

Vincent Mussot, Silvano Dal Zilio, Loïc Correnson, Serge Rainjonneau, Yves Bardout, Grégoire Scano (2020). Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. In Proc. of ERTSS 2020.

PDF Project

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias (2019). A State Class Construction for Computing the Intersection of Time Petri Nets Languages. In Proc. of FORMATS 2019.

PDF Project DOI

Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio (2019). Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer (STTT).

Project DOI

See all publications

Projects

More projects »

.js-id-recent
All Recent Formal System Eng. Formal Methods Security Other

Daedalus

Oct 20218 — Oct 2021.

“In a perfect world, models would always be correct and verification tools would answer all our questions. In the Daedalus project, we are preparing for an imperfect world.”

Daedalus (Debugging Architecture Description Languages ) is a project funded by RTRA STAE. Its main objective is to bridge the gap between: (1) automatic generation of code that is correct by construction; and (2) automatic verification of behavioral models.

MOISE

Dec 2015 — Apr 2019.

MOISE is a project on methods and tools for model-based collaborative system engineering (requirement engineering, multi-view modeling and verification, system engineering in extended enterprise).

This project was supported by Projet Investissements d’Avenir and the Embedded Systems technology domain at IRT Saint-Exupéry.

Synapse

March 2016 — Dec 2019.

Synapse is a project developping new technologies for Earth Observation space systems (smart programming of constellations, onboard and ground autonomous processing, ground infrastructures for big data processing).

This project is supported by Projet Investissements d’Avenir and the Embedded Systems technology domain at [IRT Saint-Exupéry](http://www.irt -saintexupery.com/expertise/embedded-systems/).

Time-accurate Virtualization

May 2017 — Oct 2017.

This project is a direct collaboration with SCALIAN Eurogiciel to work on a middleware for communication protocol virtualization that is faithfull with respect to timing constraints.

Ingequip

Dec 2013 — Nov. 2016

Ingequip is a project on Methods and tools for equipment engineering (system-hardware-software co-design, component-based development methods, formal verification methods).

This project was supported by Projet Investissements d’Avenir and the Embedded Systems technology domain at IRT Saint-Exupéry

BRiefcaSE

Apr 2013 — Sep 2016.

BRiefcaSE is a basic research project that targets methods involved in the specification, validation and verification of safety critical systems.

This project was part of the IFSE working group, an animation and reflexion group, financed by the RTRA STAE concerned with formal methods for system engineering.

ITEmIS

Oct 2008 — Dec 2011.

ITEmIS (Integrated Embedded Systems and Information Systems) is a project funded by ANR. The goal of the project is to define an abstract reference system architecture, a methodology, and a set of algorithms (transformed into tools, mechanisms, protocols and correctness verification algorithms) for realizing large systems of systems, integrating multiple levels, from information systems to mobile, embedded systems.

Quarteft

Apr 2009 — Nov 2012.

Quarteft (QUAlifiable Real TimE Fiacre Transformations) is a project funded by FNRAE, the Fondation de la Recherche pour l’Aéronautique et l’Espace. The goal of the project is to study formal specification language and qualifiable model transformations in the context of critical embedded systems.

CESAR

Mar 2009 — Jun 2012.

CESAR stands for Cost-efficient methods and processes for safety relevant embedded systems; it is a European funded project from ARTEMIS JOINT UNDERTAKING (JU).

OpenETCS

Apr 2012 — Dec 2015.

The purpose of the openETCS project is to follow an open approach (Open Proofs and Open Source) for developping an integrated modeling, validation and testing framework for the ETCS, the European Train Control System.

Spices

Sep 2006 — Nov 2009.

SPICES is a EUREKA-ITEA project on Support for Predictable Integration of mission Critical Embedded Systems.

Topcased

Sep 2006 — Nov 2009.

Topcased, Toolkit in OPen-source for Critical Application SystEms Development, is a project funded by Aerospace Valley. The goal of the project is to build an open source CASE environment for critical applications and systems development.

COPS

Mar 2006 — Dec 2008.

COPS (Composition des politiques et des services / Composition of Services and Policies) is an ANR funded project studying formal methods for Service Oriented Applications.

TraLaLa

Nov 2004 — Feb 2008.

TraLaLA, XML Transformation Languages: logic and applications, is a project funded by ACI MASSES DE DONNÉES.

The objectives of the project is to study the processing, querying and manipulation of data-masses (large amounts of data) available in XML format.

CRISS

Sep 2003 — Dec 2006.

CRISS, (Contrôle de Ressources et d’Interférence dans les Systèmes Synchrones) is a French project of ACI SÉCURITÉ INFORMATIQUE.

The CRISS project focuses on security issues raised by mobile code, that occurs in areas as diverse as programmable networks, network games and smart cards. In ths project, we focus on two classes of properties that appear naturally in the context of mobile code: the derivation of bounds on the resources needed to execute code (to avoid denial of service attacks); and control of the flow of information, or non-interference, to avoid leakage of confidential data.

Recent Posts

MCC Tool at Petri 2020 (Best Teaser Video)

A tool paper about MCC—our software for transformings models of High-Level Petri nets, given in PNML, into equivalent Place/Transition nets, not the competition!—has been accepted at Petri Nets 2020. You can find more about it here:
June 28, 2020 1 min read
MCC Tool at Petri 2020 (Best Teaser Video)

Results of the 2020 Model Checking Contest

Our tool, TINA, won a gold medal in the “state space” category of the Model-Checking Contest 2020, an international competition of model-checking tools for the verification of concurrent systems. This is the second year in a row that TINA came first in the “state space” category.
June 28, 2020 1 min read
Results of the 2020 Model Checking Contest

What About Autonomous Satellite (Best Paper)

A paper about the formal veririfcation of autonomy in earth observation satellites has been accepted at the 10th International Congress and Exhibition on Embedded Real-Time Software and Systems (ERTSS 2020).
June 28, 2020 1 min read
What About Autonomous Satellite (Best Paper)

The Moose Have Retired

For the last 20 years, I have been developing my own “static site generators” in order to create pages for my personal website. Static site generator have many benefits when compared to Content Management Systems, especially in terms of security, but also because they are generally more “low maintenance”.
February 6, 2019 2 min read
The Moose Have Retired

Short Bio

“Epoch avait un an ! Rome remplaçait Sparte …" I was born in France in 1971. I obtained my PhD from INRIA and the University of Nice - Sophia Antipolis in 1999, and I hold a Master’s Degree in computer science from École Normale Supérieure de Lyon, where I studied parallel programming and architecture.
February 4, 2019 1 min read
Short Bio

Contact

Information on how to reach LAAS