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://dx.doi.org/10.1016/j.scico.2010.02.008. |
Další formáty:
BibTeX
LaTeX
RIS
@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 = {http://dx.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://dx.doi.org/10.1016/j.scico.2010.02.008.
|