BENEŠ, Nikola, Luboš BRIM, Barbora BÜHNOVÁ, Ivana ČERNÁ, Jiří SOCHOR a Pavlína MORAVCOVÁ VAŘEKOVÁ. Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata. Science of Computer Programming. Elsevier, 2011, roč. 76, č. 10, s. 877-890. ISSN 0167-6423. doi:10.1016/j.scico.2010.02.008.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata
Autoři BENEŠ, Nikola (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Barbora BÜHNOVÁ (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Jiří SOCHOR (203 Česká republika, domácí) a Pavlína MORAVCOVÁ VAŘEKOVÁ (203 Česká republika, domácí).
Vydání Science of Computer Programming, Elsevier, 2011, 0167-6423.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.622
Kód RIV RIV/00216224:14330/11:00049649
Organizační jednotka Fakulta informatiky
Doi http://dx.doi.org/10.1016/j.scico.2010.02.008
UT WoS 000292232900004
Klíčová slova anglicky State/event LTL; Partial order reduction; Formal verification; Model checking; Component-based systems; Component-interaction automata
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Nikola Beneš, Ph.D., učo 72525. Změněno: 24. 10. 2013 16:21.
Anotace
Software 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. To bring some evidence of the method’s efficiency, we present the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems.
Návaznosti
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 19. 8. 2022 09:19