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

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2011
Druh Článek v odborném periodiku
Časopis / Zdroj Science of Computer Programming
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1016/j.scico.2010.02.008
Doi http://dx.doi.org/10.1016/j.scico.2010.02.008
Obor Informatika
Klíčová slova State/event LTL; Partial order reduction; Formal verification; Model checking; Component-based systems; Component-interaction automata
Přiložené soubory
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.