Silvano DAL ZILIO
Silvano DAL ZILIO
Home
Publications
Projects
Courses
Posts
Software
Contact
Light
Dark
Automatic
Patterns
RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus
We define a new verification method, called RT-MOBS, for checking real-time requirements based on Time Petri nets (TPN). Our approach …
Ning Ge
,
Silvano Dal Zilio
,
Hongyu Liu
,
Li Zhang
,
Lianyi Zhang
Cite
Project
DOI
Formal Verification of User-Level Real-Time Property Patterns
To ease the expression of real-time requirements, Dwyer, and then Konrad, studied a large collection of existing systems in order to …
Ning Ge
,
Marc Pantel
,
Silvano Dal Zilio
PDF
Cite
Project
DOI
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
A classical method for model-checking timed properties, such as those expressed using timed extensions of temporal logic, is to rely on …
Silvano Dal Zilio
,
Bernard Berthomieu
PDF
Cite
Project
DOI
A formal framework to specify and verify real-time properties on critical systems
We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties …
Nouha Abid
,
Silvano Dal Zilio
,
Didier Le Botlan
Cite
Project
DOI
A Verified Approach for Checking Real-Time Specification Patterns
We propose a verified approach to the formal verification of timed properties using model-checking techniques. We focus on properties …
Nouha Abid
,
Silvano Dal Zilio
,
Didier Le Botlan
PDF
Cite
Project
Real-Time Specification Patterns and Tools
An issue limiting the adoption of model checking technologies by the industry is the ability, for non-experts, to express their …
Nouha Abid
,
Silvano Dal Zilio
,
Didier Le Botlan
PDF
Cite
Project
DOI
A Timed Graphical Interval Logic
We define a graphical language for expressing timed requirements on concurrent systems. This formal language, called
Timed Graphical …
Silvano Dal Zilio
,
Nouha Abid
PDF
Cite
Project
Verification of Real-Time Specification Patterns on Time Transitions Systems
We address the problem of checking properties of Time Transition Systems (TTS), a generalization of Time Petri Nets with data variables …
Silvano Dal Zilio
,
Nouha Abid
,
Didier Le Botlan
PDF
Cite
Project
Definition of the Fiacre Real-Time Specification Patterns Language
In this report, we define a high-level language for expressing properties over system expressed using Fiacre. Our approach is based on …
Silvano Dal Zilio
,
Nouha Abid
,
Didier Le Botlan
,
Bernard Berthomieu
,
François Vernadat
,
Mamoun Filali
,
Jean-Paul Bodeveix
PDF
Cite
Project
Cite
×