136documents trouvés
Spé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
122073Verification based development process for embedded systems
T.CORREA, L.B.BECKER, J.P.BODEVEIX, J.M.FARINES, M.FILALI, F.VERNADAT
UFSC, IRIT-UPS, LCMI/EEL/UFSC, OLC
Manifestation avec acte : Embedded Real Time Software and Systems (ERTS2 2010), Toulouse (France), 19-21 Mai 2010, 10p. , N° 10479
Diffusable
122251Supporting the design of safety critical systems using AADL
T.CORREA, L.B.BECKER, J.M.FARINES, J.P.BODEVEIX, M.FILALI, F.VERNADAT
DAS/UFSC, IRIT-UPS, OLC
Manifestation avec acte : International Conference on Engineering of Complex Computer Systems (ICECCS'2010), Oxford (UK), 22-26 Mars 2010, 6p. , N° 10953
Diffusable
126069Langage intermédiaire et transformations de modèles pour le développement de systèmes temps-réel: retour d'expérience sur la chaîne de vérification formelle Fiacre
B.BERTHOMIEU, J.P.BODEVEIX, S.DAL ZILIO, M.FILALI, M.PANTEL, F.VERNADAT
OLC, IRIT-UPS
Manifestation sans acte : IDM 2010 : journées sur l'Ingénierie Dirigée par les Modèles, Pau (France), 9-10 Mars 2010, 6p. , N° 10346
Diffusable
121696Composer des réseaux de Petri temporels
F.PERES, B.BERTHOMIEU, F.VERNADAT
OLC
Manifestation avec acte : Journal européen des systèmes automatisés - Modèlisation des systèmes réactifs (JESA-MSR 2009) , Nantes (France), 16-18 Novembre 2009, Vol.43, pp.1001-1015 , N° 09400
Lien : http://hal.archives-ouvertes.fr/hal-00438377/fr/
Diffusable
Plus d'informations
Mots-Clés / Keywords
Composition; Réseaux de Petri intemporels; Compositionnalité;
Enumerative Parallel and Distributed State Space Construction
R.SAAD, S.DAL ZILIO, B.BERTHOMIEU, F.VERNADAT
OLC
Manifestation avec acte : Ecole dEté Temps Réel (ETR09), Paris (France), 31 Août-4 septembre 2009, 15p. , N° 09852
Diffusable
120310Specification and verification of real-time systems using the POLA tool
F.PERES, P.E.HLADIK, F.VERNADAT
OLC
Manifestation avec acte : 3rd International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS 2009), Rabat (Maroc), 2-3 Juillet 2009, 12p. , N° 09388
Diffusable
Plus d'informations
Mots-Clés / Keywords
D.S.L.; Model checking; Real Time Systems;
Chapter 3 : Analysis Methods for Petri Nets
F.VERNADAT, S.HADDAD
OLC, LSV
Ouvrage (auteur) : Petri Nets. fundamental Models, Verification and Applications, ISTE & Wiley, N°978-1-84821-079-0, Juillet 2009, pp.41-86 , N° 09805
Diffusion restreinte
120120Chapter 12 : Verification od Specific Properties
F.VERNADAT, S.HADDAD
OLC, LSV
Ouvrage (auteur) : Petri Nets. fundamental Models, Verification and Applications, ISTE & Wiley, N°978-1-84821-079-0, Juillet 2009, pp.349-414 , N° 09808
Diffusion restreinte
120126Formal verification of AADL specifications in the topcased environment
B.BERTHOMIEU, J.P.BODEVEIX, C.CHAUDET, S.DAL ZILIO, M.FILALI, F.VERNADAT
OLC, IRIT-UPS
Manifestation avec acte : Reliable Software Technologies - Ada Europe 2009, Brest (France), 8-12 Juin 2009, 15p. , N° 09314
Diffusable
Plus d'informations
Abstract
We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its behavioral annex. Our approach is based on tools that are integrated in the Topcased environment. We give a high-level view of the tools involved and illustrate the successive transformations that take place during the verification process.