Partial Order Reduction for State/Event LTL with Application to
Component-Interaction Automata

J 2011

Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata

BENEŠ, Nikola; Luboš BRIM; Barbora BÜHNOVÁ; Ivana ČERNÁ; Jiří SOCHOR et al.

Základní údaje

Originální název

Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata

Autoři

BENEŠ, Nikola; Luboš BRIM; Barbora BÜHNOVÁ; Ivana ČERNÁ ; Jiří SOCHOR a Pavlína MORAVCOVÁ VAŘEKOVÁ

Vydání

Science of Computer Programming, Elsevier, 2011, 0167-6423

Další údaje

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í

Odkazy

URL

Impakt faktor

Impact factor: 0.622

Kód RIV

RIV/00216224:14330/11:00049649

Organizační jednotka

Fakulta informatiky

DOI

https://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ěněno: 24. 10. 2013 16:21, RNDr. Nikola Beneš, Ph.D.

Anotace

V originále

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 VaV

Ná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ěr

Ná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 MU

Ná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

Přiložené soubory

2011-SCP.pdf

Požádat o autorskou verzi souboru

Citovat

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. Dostupné z: https://doi.org/10.1016/j.scico.2010.02.008.

@article{905464,
   author = {Beneš, Nikola and Brim, Luboš and Bühnová, Barbora and Černá, Ivana and Sochor, Jiří and Moravcová Vařeková, Pavlína},
   article_number = {10},
   doi = {https://doi.org/10.1016/j.scico.2010.02.008},
   keywords = {State/event LTL; Partial order reduction; Formal verification; Model checking; Component-based systems; Component-interaction automata},
   language = {eng},
   issn = {0167-6423},
   journal = {Science of Computer Programming},
   title = {Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata},
   url = {http://dx.doi.org/10.1016/j.scico.2010.02.008},
   volume = {76},
   year = {2011}
}

TY  - JOUR
ID  - 905464
AU  - Beneš, Nikola - Brim, Luboš - Bühnová, Barbora - Černá, Ivana - Sochor, Jiří - Moravcová Vařeková, Pavlína
PY  - 2011
TI  - Partial Order Reduction for State/Event LTL with Application to Component-Interaction Automata
JF  - Science of Computer Programming
VL  - 76
IS  - 10
SP  - 877-890
EP  - 877-890
PB  - Elsevier
SN  - 01676423
KW  - State/event LTL
KW  - Partial order reduction
KW  - Formal verification
KW  - Model checking
KW  - Component-based systems
KW  - Component-interaction automata
UR  - http://dx.doi.org/10.1016/j.scico.2010.02.008
N2  - 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.
ER  -

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. \textit{Science of Computer Programming}. Elsevier, 2011, roč.~76, č.~10, s.~877-890. ISSN~0167-6423. Dostupné z: https://doi.org/10.1016/j.scico.2010.02.008.

Přehled o publikaci