Result: Forward reachability analysis of timed Petri nets

Title:
Forward reachability analysis of timed Petri nets
Authors:
PAROSH AZIZ ABDULLA, DENEUX, Johann, MAHATA, Pritha, NYLEN, Aletta
Source:
FORMATS 2004 : formal techniques, modelling and analysis of timed and fault-tolerant systems (Grenoble, 22-24 September 2004)Lecture notes in computer science. :343-362
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 21 ref
Original Material:
INIST-CNRS
Subject Terms:
Control theory, operational research, Automatique, recherche opérationnelle, Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Automates. Machines abstraites. Machines de turing, Automata. Abstract machines. Turing machines, Théorie programmation, Programming theory, Analyse atteignabilité, Reachability analysis, Analyse symbolique, Symbolic analysis, Análisis simbolico, Machine état fini, Finite state machine, Máquina estado finito, Réseau Pétri, Petri net, Red Petri, Simultanéité informatique, Concurrency, Simultaneidad informatica, Système réparti, Distributed system, Sistema repartido, Système temporisé, Timed system, Sistema temporizado, Système temps réel, Real time system, Sistema tiempo real, Vérification programme, Program verification, Verificación programa
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Uppsala University, Sweden
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=16335676
Rights:
Copyright 2005 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.16335676
Database:
PASCAL Archive

Further Information

We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions, and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.