29 citations · 81 across the 19 of their papers we have counts for
4 papers · 1 filter
Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
Silvano Dal Zilio, Bernard Berthomieu
A classical method for model-checking timed properties-such as those expressed using timed extensions of temporal logic-is to rely on the use of observers. In this context, a major…
Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina
Silvano Dal Zilio, Bernard Berthomieu, Didier Le Botlan
We describe our experience with modeling a video tracking system used to detect and follow moving targets from an airplane. We provide a formal model that takes into account the re…
On the Complexity of Flanked Finite State Automata
Florent Avellaneda, Silvano Dal Zilio, Jean-Baptiste Raclet
We define a new subclass of nondeterministic finite automata for prefix-closed languages called Flanked Finite Automata (FFA). We show that this class enjoys good complexity proper…
Real-Time Model Checking Support for AADL
B Berthomieu, J. -P Bodeveix, S Dal Zilio +4
We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the…