91documents 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
129019An 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
129015Dé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
129013A flexible WCET analysis method for safety critical real-time systems using UML-MARTE model checker
N.GE, M.PANTEL, B.BERTHOMIEU, X.CREGUT
IRIT-ENSEEIHT, VERTICS
Rapport LAAS N°12401, Juillet 2012, 11p.
Diffusable
127782Who ckecks the model-checkers ?
N.ABID, S.DAL ZILIO, B.BERTHOMIEU
VERTICS
Rapport LAAS N°12367, Juillet 2012, 16p.
Diffusable
127687Model-checking support for AADL
S.DAL ZILIO, F.VERNADAT, B.BERTHOMIEU, M.FILALI, J.P.BODEVEIX
VERTICS, IRIT-UPS
Rapport LAAS N°12758,
Diffusable
129022Parallel model cheking with lazy cycle detection MCLCD
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU
VERTICS
Rapport LAAS N°12139, Mars 2012, 49p.
Non diffusable
126852La traduction AADL-FIACRE. L'expérience TOPCASED
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, P.FARAIL, M.FILALI, P.GAUFILLET, F.VERNADAT
VERTICS, IRIT-UPS, EADS AIRBUS SA
Manifestation sans acte : Approches Formelles dans l'Assistance au Développement de Logiciels ( AFADL ) 2012 du 11 janvier au 13 janvier 2012, Grenoble (France), Janvier 2012, 51p. , N° 12773
Diffusable
129066