2011
Verification of Timed-Arc Petri Nets (invited talk)
JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBAZákladní údaje
Originální název
Verification of Timed-Arc Petri Nets (invited talk)
Název česky
Verifikace Casovych Petriho Siti
Autoři
JACOBSEN, Lasse; Morten JACOBSEN; H. Mikael MOLLER a Jiří SRBA
Vydání
Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM'11, 2011
Další údaje
Jazyk
angličtina
Typ výsledku
Vyžádané přednášky
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Nizozemské království
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Označené pro přenos do RIV
Ano
Kód RIV
RIV/00216224:14330/11:00054541
Organizační jednotka
Fakulta informatiky
Klíčová slova česky
verifikace; Petriho site; nastroje; rozhodnutelnost
Klíčová slova anglicky
verification; Petri net; tool; decidability
Příznaky
Mezinárodní význam
Změněno: 21. 12. 2011 18:43, Prof. Jiří Srba, Ph.D.
V originále
Timed-Arc Petri Nets (TAPN) are an extension of the classical P/T nets with continuous time. Tokens in TAPN carry an age and arcs between places and transitions are labelled with time intervals restricting the age of tokens available for transition firing. The TAPN model posses a number of interesting theoretical properties distinguishing them from other time extensions of Petri nets. We shall give an overview of the recent theory developed in the verification of TAPN extended with features like read/transport arcs, timed inhibitor arcs and age invariants. We will examine in detail the boundaries of automatic verification and the connections between TAPN and the model of timed automata. Finally, we will mention the tool TAPAAL that supports modelling, simulation and verification of TAPN and discuss a small case study of alternating bit protocol.
Česky
Časované Petriho sítě Arc (TAPN) je rozšíření klasické P / T sítí se spojitým časem. Tokeny TAPN nesou věku a oblouky mezi místy a přechody jsou označeny časových intervalech omezení věku známek pro přechod palbu.TAPN modelu vlastnit několik zajímavých teoretických vlastností odlišuje od ostatních doby rozšíření Petriho sítí. Měli bychom dát přehled o posledních teorie byla vyvinuta při ověřování TAPN rozšířena o funkce, jako je čtení / doprava oblouky, časované inhibitor oblouky a věku invarianty. Se budeme podrobně prozkoumat hranice automatické verifikace a spojení mezi TAPN a model automatu časově. Nakonec se zmíníme o nástroj, který podporuje TAPAAL modelování, simulaci a ověření TAPN a diskutovat o malou případovou studii střídání bit protokolu.
Návaznosti
| MSM0021622419, záměr |
|