91documents trouvés
Time petri nets. Analysis methods and verification with TINA
B.BERTHOMIEU, F.PERES, F.VERNADAT
OLC
Ouvrage (contribution) : Modeling and Verification of Real-Time Systems, N°ISBN 9781848210134, 2008, Chapitre 1, pp.19-48 , N° 08722
Diffusable
116076An approach to model and verify complex systems using the TOPCASED toolkit
R.SAAD, F.PERES, F.VERNADAT, B.BERTHOMIEU, M.V.LINHARES , R.S.DE OLIVEIRA, J.M.FARINES
OLC, LCMI/EEL/UFSC
Rapport LAAS N°07579, Octobre 2007, 5p.
Diffusable
111785Model checking prioritized time Petri nets
B.BERTHOMIEU, F.PERES, F.VERNADAT
OLC
Manifestation avec acte : 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), Tokyo (Japon), 22-25 Octobre 2007, 15p. , N° 07261
Diffusable
Plus d'informations
Abstract
In a companion paper [BPV06], we investigated the expressiveness of Time Petri Nets extended with Priorities and showed that it is very close to that Timed Automata, in terms of weak timed bisimilarity. As a continuation of this work we investigate here the applicability of the available state space abstractions for Bounded Time Petri Nets to Bounded Prioritized Time Petri Nets. We show in particular that a slight extension of the strong state classes construction of [BV03] provides a convenient state space abstraction for these nets, preserving markings, states, and LTL formulas. Interestingly, and conversely to Timed Automata, the construction proposed does not require to compute polyhedra differences.
Spécification des besoins pour la représentation du temps quantitatif dans un modèle de calcul asynchrone
B.BERTHOMIEU, M.FILALI, H.GARAVEL, F.LANG, F.PERES, J.STOECKER, F.VERNADAT
OLC, IRIT-UPS, INRIA Rhône-Alpes
Rapport de Contrat : Projet ANR05RNTL03101 OpenEmbeDD, Août 2007, 10p. , N° 07473
Diffusable
111301Reachability problems and abstract state spaces for time Petri nets with stopwatches
B.BERTHOMIEU, D.LIME, O.H.ROUX, F.VERNADAT
OLC, Aalborg, IRCCYN
Revue Scientifique : Discrete Event Dynamic Systems, Vol.17, N°2, pp.133-158, Juin 2007 , N° 04483
Diffusable
Plus d'informations
Abstract
Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs, based on the known state class method for Time Petri nets. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By adjusting a parameter, the exact behavior can be approximated as closely as desired. The methods have been implemented, experiments are reported.
The syntax and semantics of FIACRE
B.BERTHOMIEU, J.P.BODEVEIX, M.FILALI, H.GARAVEL, F.LANG, F.PERES, R.SAAD, J.STOECKER, F.VERNADAT
IRIT-UPS, OLC, INRIA Rhône-Alpes, M2D
Rapport de Contrat : Projet ANR05RNTL03101 OpenEmbeDD, Mai 2007, 30p. , N° 07264
Diffusable
110541SimplePDL2Tina: mise en oeuvre d'une validation de modèles de processus
B.COMBEMALE, X.CREGUT, B.BERTHOMIEU, F.VERNADAT
ENSEEIHT, OLC
Manifestations avec acte à diffusion limitée : 3ème journées de l'Ingénierie Dirigée par les Modèles (IDM'07), Toulouse (FRANCE), 29-30 Mars 2007, pp.149-164 , N° 06744
Diffusable
Plus d'informations
Mots-Clés / Keywords
MDE; Transformations; Semantics; Validation; ATL; Petri nets; Tina;
SimplePDL2Tina: mise en oeuvre d'une validation de modèles de processus
B.COMBEMALE, X.CREGUT, B.BERTHOMIEU, F.VERNADAT
ENSEEIHT, OLC
Manifestation avec acte : Journées FAC'2007. Formalisation des Activités Concurrentes, Toulouse (France), 15-16 Mars 2007, 12p. , N° 06744
Diffusable
Plus d'informations
Mots-Clés / Keywords
MDE; Transformations; Semantics; Validation; ATL; Petri nets; Tina;
Vérification des applications temps réel
F.SIMONOT-LION, Y.Q.SONG, B.BERTHOMIEU, F.VERNADAT
LORIA, OLC
Ouvrage (contribution) : Encyclopédie de l'Informatique et des Systèmes d'Information, Vuibert (Ed.), J.Akoka, I.Comyn-Wattiau (Eds), N°ISBN 978-2-7117-4846, 2006, pp.761-773 , N° 05578
Diffusable
109727Réseaux de Petri temporels : méthodes d'analyse et vérification avec TINA
B.BERTHOMIEU, F.VERNADAT
OLC
Ouvrage (contribution) : Systèmes temps réel 1. Techniques de description et de vérification, Traité Information-Commande-Communication. Informatique et Systèmes d'Information, Ed. Lavoisier, N°ISBN 2-7462-1303-6, 2006, Chapitre 1, pp.25-57 , N° 06354
Diffusable
108332