RIV/00216224:14330/11:00049649 - Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata (2011)

Údaje o výsledku
Identifikační kódRIV/00216224:14330/11:00049649
Název v původním jazycePartial Order Reduction for State/Event LTL with Application to Component-Interaction Automata
DruhJ - Článek v odborném periodiku
Jazykeng - angličtina
OborIN - Informatika
Rok uplatnění2011
Kód důvěrnosti údajůS - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
Počet výskytů výsledku2
Údaje z Hodnocení výsledků výzkumných organizací 2014
Výsledek byl hodnocen v Pilíři I
Rozsah vyřazení výsledkuTento výskyt výsledku není vyřazen
Zařazení výsledku v hodnoceníJimp - Článek v impaktovaném časopise evidovaném ve Web of Science
Skupina oboru v hodnocení04 - Technické a informatické vědy
Konkrétní způsob(y) hodnocení výsledkuVýsledek hodnocený již v předchozím hodnocení, body se přebírají
Bodové ohodnocení17,636
Faktor korekce100,9 %
Body (upravené podle přílohy č. 8 Metodiky)17,800
Rozdělení výsledku mezi předkladatele
OrganizaceVýzkumná organizace?PodílBodyBody (upravené podle přílohy č. 8 Metodiky)
Masarykova univerzita / Fakulta informatikyano100,0 %17,63617,800
Tvůrci výsledku
Počet tvůrců celkem6
Počet domácích tvůrců6
TvůrceBeneš Nikola (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; G - garant výsledku; vedidk: 2050587)
TvůrceBrim Luboš (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 6500773)
TvůrceBühnová Barbora (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 5332877)
TvůrceČerná Ivana (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2361132)
TvůrceSochor Jiří (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 7676239)
TvůrceMoravcová Vařeková Pavlína (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 3664449)
Údaje blíže specifikující výsledek
Popis v původním jazyceSoftware systems assembled from autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL (Chaki et al. 2004, 2005) incorporates both states and events to express important properties of component-based software systems. The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core is a novel notion of stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
Klíčová slovaState/event LTL; Partial order reduction; Formal verification; Model checking; Component-based systems; Component-interaction automata
Kód UT ISI000292232900004
Název periodkaScience of Computer Programming
Rozsah stran877-890
ISSN0167-6423
Svazek periodika76
Číslo periodika v rámci uvedeného svazku10
Stát vydavatele periodikaCZ - Česká republika
Počet stran výsledku14
DOI výsledku10.1016/j.scico.2010.02.008
Údaje o tomto záznamu o výsledku
PředkladatelMasarykova univerzita / Fakulta informatiky
DodavatelMSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT)
Rok sběru2012
Systémové označení dodávky datRIV12-MSM-14330___/01:1
SpecifikaceRIV/00216224:14330/11:00049649!RIV12-MSM-14330___
Kontrolní kód[7F1B2A44FBDE]
Další výskyty tohoto výsledku od stejného předkladatele
Dodáno GA ČR v roce 2012Záznam s identifikačním kódem RIV/00216224:14330/11:00049649 v dodávce dat RIV12-GA0-14330___/02:1
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
ProjektGA201/09/1389 - Verifikace a analýza velmi velkých počítačových systémů (2009-2011, GA0/GA)
Výzkumný záměrMSM0021622419 - Vysoce paralelní a distribuované výpočetní systémy (2005-2011, MSM)
S - Specifický výzkum na vysokých školách