Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets (2014)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/14:00080035 |
|---|---|
| Název v anglickém jazyce | Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2014 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 1 |
| Počet tvůrců celkem | 6 |
| Počet domácích tvůrců | 1 |
| Výčet všech uvedených jednotlivých tvůrců | Sine V. Birch (státní příslušnost: DK - Dánské království) Thomas S. Jacobsen (státní příslušnost: DK - Dánské království) Jacob J. Jensen (státní příslušnost: DK - Dánské království) Christoffer Moesgaard (státní příslušnost: DK - Dánské království) Niels N. Samuelsen (státní příslušnost: DK - Dánské království) Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057) |
| Popis výsledku v anglickém jazyce | State-space explosion is a major obstacle in verification of time-critical distributed systems. An important factor with a negative influence on the tractability of the analysis is the size of constants that clocks are compared to. This problem is particularly accented in explicit state-space exploration techniques. We suggest an approximation method for reducing the size of constants present in the model. The proposed method is developed for Timed-Arc Petri Nets and creates an under-approximation or anover-approximation of the model behaviour. The verification of approximated Petri net models can be considerably faster but it does not in general guarantee conclusive answers. We implement the algorithms within the open-source model checker TAPAAL anddemonstrate on a number of experiments that our approximation techniques often result in a significant speed-up of the verification. |
| Klíčová slova oddělená středníkem | timed-arc Petri nets; approximation; abstractions; verification |
| Stránka www, na které se nachází výsledek | http://link.springer.com/chapter/10.1007%2F978-3-319-10512-3_17 |
| DOI výsledku | 10.1007/978-3-319-10512-3_17 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Proceedings of the 12th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'14) |
|---|---|
| ISBN | 9783319105116 |
| ISSN | 0302-9743 |
| Počet stran výsledku | 15 |
| Strana od-do | 237-251 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Nizozemsko |
| Místo konání akce | Italie |
| Datum konání akce | 2014 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2015 |
| Specifikace | RIV/00216224:14330/14:00080035!RIV15-MSM-14330___ |
| Datum poslední aktualizace výsledku | 29.05.2015 |
| Kontrolní číslo | 152395607 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Podpora / návaznosti | Institucionální podpora na rozvoj výzkumné organizace |
|---|