24documents trouvés
Vé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
129017Rapport 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
129019Towards timed requirement verification for service choreographies
N.GUERMOUCHE, S.DAL ZILIO
SARA, VERTICS
Manifestation avec acte : IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing ( COLLABORATECOM ) 2012 du 14 octobre au 17 octobre 2012, Pittsburgh (USA), Octobre 2012, 10p. , N° 12495
Diffusable
Plus d'informations
Abstract
In this paper, we propose an approach for analyzing and validating a composition of services with respect to real time properties. We consider services defined using an extension of the Business Process Execution Language (BPEL) where timing constraints can be associated to the execution of an activity or define delays between events. The goal is to check whether a choreography of timed services satisfies given complex real time requirements. Our approach is based on a formal interpretation of timed choreographies in the Fiacre verification language that defines a precise model for the behavior of services and their timed interactions. We also rely on a logic-based language for property definition to formalize complex real-time requirements and on specific tooling for model-checking Fiacre specifications.
An experiment on parallel model checking of a CTL fragment
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
VERTICS
Manifestation avec acte : International Symposium on Automated Technology for Verification and Analysis ( ATVA ) 2012 du 03 octobre au 06 octobre 2012, Thiruvananthapuram (Inde), Octobre 2012, 15p. , N° 12400
Lien : http://hal.archives-ouvertes.fr/hal-00782354
Diffusable
Plus d'informations
Abstract
We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm takes bene t from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions on the models that can be analyzed; no restrictions on the way states are distributed; and no restrictions on the way work is shared among processors. We evaluate the performance of diff erent versions of our algorithm and compare our results with those obtained using other parallel model checking tools. One of the most novel contributions of this work is to study a space-e fficient variant for CTL model-checking that does not require to store the whole transition graph but that operates on a reverse spanning tree.
Dé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
129015Real-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.
A verified approach to checking real-time patterns on fiacre programs
N.ABID, S.DAL ZILIO
VERTICS
Manifestation avec acte : Doctoral Symposium of FM 2012, Paris (France), 27-31 Août 2012, pp.13-23 , N° 12365
Diffusable
127886A 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.
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
129013Who ckecks the model-checkers ?
N.ABID, S.DAL ZILIO, B.BERTHOMIEU
VERTICS
Rapport LAAS N°12367, Juillet 2012, 16p.
Diffusable
127687