8documents trouvés
Rapport final
N.ABID, J.C.BACH, B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, N.DISSAUX, DDOOSE, M.FILALI, M.GARNACHO, D.LE BOTLAN, P.MICHEL, M.PANTEL, P.E.MOREAU, A.SCHACH, F.VERNADAT
VERTICS, LORIA, IRIT-UPS, Ellidiss Technologi, ONERA, ONERA-CERT, ONERA/DTIM, IRIT-ENSEEIHT
Rapport de Contrat : Projet QUARTEFT (FNRAE), Décembre 2012, 41p. , N° 12757
Diffusion restreinte
129019Vérification de transformations. Quarteft T42-4
N.ABID, B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, DDOOSE, M.FILALI, D.LE BOTLAN, M.PANTEL, F.VERNADAT
VERTICS, IRIT-UPS, ONERA, IRIT-ENSEEIHT
Rapport de Contrat : Projet QUARTEFT (FNRAE), Décembre 2012, 28p. , N° 12756
Diffusion restreinte
129017Définition du langage de propriétés RT - FIACRE. Quarteft T2-12-B
N.ABID, B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, M.FILALI, D.LE BOTLAN, F.VERNADAT
VERTICS, IRIT-UPS
Rapport de Contrat : Projet QUARTEFT (FNRAE), Septembre 2012, 17p. , N° 12755
Diffusion restreinte
129015A verified approach for checking real-time specification patterns
N.ABID, S.DAL ZILIO, D.LE BOTLAN
VERTICS
Manifestation avec acte : International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2012), Paris (France), 27-28 Août 2012, 19p. , N° 11365
Lien : http://hal.archives-ouvertes.fr/hal-00593963/fr/
Diffusable
Plus d'informations
Abstract
We address the problem of checking properties of Time Tran- sition Systems (TTS), a generalization of Time Petri Nets with data variables and priorities. We are specifically interested by time-related properties expressed using real-time specification patterns, a language inspired by properties commonly found during the analysis of reactive systems. Our verification approach is based on the use of observers in order to transform the verification of timed patterns into the verification of simpler LTL formulas. While the use of observers for model-checking timed extensions of temporal logics is fairly common, our approach is original in several ways. In addition to traditional observers based on the monitoring of places and transitions, we propose a new class of ob- servers based on the monitoring of data modifications that appears to be more efficient in practice. Moreover, we provide a formal framework to prove that observers are correct and non-intrusive, meaning that they do not affect the system under observation. Our approach has been inte- grated in a verification toolchain for Fiacre, a formal modeling language that can be compiled into TTS.
Real-time specification patterns and tools
N.ABID, S.DAL ZILIO, D.LE BOTLAN
VERTICS
Manifestation avec acte : International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012), Paris (France), 27-28 Août 2012, 16p. , N° 11364
Lien : http://hal.archives-ouvertes.fr/hal-00782649
Diffusable
Plus d'informations
Abstract
We propose a real-time extension to the pattern specification language of Dwyer et al. Our contributions are twofold. First, we provide a formal pattern specification language that is sim- ple enough to ease the specification of requirements by non-experts and rich enough to express general temporal constraints commonly found in reactive systems, such as compliance to deadlines, bounds on the worst- case execution time, etc. For each pattern, we give a precise definition based on three different formalisms: a denotational interpretation based on first-order formulas over timed traces; a definition based on a non- ambiguous, graphical notation; and a logic-based definition based on a translation into a real-time temporal logic. Our second contribution is a framework for the model-based verification of timed patterns. Our approach makes use of observers in order to reduce the verification of timed patterns to the verification of Linear Temporal Logic formulas. This framework has been integrated in a verification toolchain for Fiacre, a formal modeling language for real-time systems.
Définition formelle du langage de comportement RT- FIACRE V3. Quarteft T12-12-A
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, M.FILALI, D.LE BOTLAN, R.SPADOTTI, G.VERDIER, F.VERNADAT
VERTICS, IRIT-UPS
Rapport de Contrat : Projet QUARTEFT (FNRAE), Août 2012, 35p. , N° 12754
Diffusion restreinte
129013Spécification des besoins RT-Fiacre
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, DDOOSE, M.FILALI, D.LE BOTLAN, P.MICHEL, M.PANTEL, F.VERNADAT
OLC, IRIT-UPS, ONERA, ONERA-CERT
Rapport de Contrat : FNRAE-QUARTEFT T1-06-A, Juillet 2010, 22p. , N° 10434
Diffusable
122073Recasting MLF
D.LE BOTLAN, D.REMY
OLC, INRIA Rocquencourt
Revue Scientifique : Information and Computation, Vol.207, N°6, pp.726-785, Juin 2009 , N° 09359
Lien : http://hal.inria.fr/inria-00156628/fr/
Diffusable
118132