BENEŠ, Nikola, Milan KŘIVÁNEK a Filip ŠTEFAŇÁK. Space Effective Model Checking for Component-Interaction Automata. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Dagstuhl, Německo: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo, 2009. 8 s. ISBN 978-3-939897-15-6.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Space Effective Model Checking for Component-Interaction Automata
Název česky Prostorově efektivní ověřování modelu pro komponentově-interakční automaty
Autoři BENEŠ, Nikola (203 Česká republika, garant, domácí), Milan KŘIVÁNEK (203 Česká republika, domácí) a Filip ŠTEFAŇÁK (703 Slovensko, domácí).
Vydání Dagstuhl, Německo, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09), 8 s. 2009.
Nakladatel Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Německo
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/09:00028809
Organizační jednotka Fakulta informatiky
ISBN 978-3-939897-15-6
Klíčová slova česky redukce pomocí reprezentantů; ověřování modelu; komponentové systémy
Klíčová slova anglicky partial order reduction; model checking; component-based systems
Štítky Component-based systems, Component-Interaction automata, Model checking, partial order reduction, verification
Změnil Změnil: RNDr. Nikola Beneš, Ph.D., učo 72525. Změněno: 17. 12. 2010 12:27.
Anotace
The techniques of component-based development are becoming a common practice in the area of software engineering. One of the crucial issues in the correctness of such systems is the correct interaction among the components. The formalism of component-interaction automata was devised to model various aspects of such interaction, as well as to allow automated verification in the form of model checking with properties expressed in the component-interaction LTL, a variant of the known linear temporal logic. As the state space of a component-based system can grow exponentially with the number of components, it is desirable to employ reduction techniques to make the verification task more feasible. In our work, we describe the implementation of the ample set partial order reduction method within the component-interaction automata verification framework. Due to the state and action-based nature of both the modelling and specification formalisms, the implementation differs from traditional state-based approaches. After describing the implementation, we present some of the results obtained by employing the enhanced verification framework on a case study.
Návaznosti
GD102/09/H042, projekt VaVNázev: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaný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
1ET400300504, projekt VaVNázev: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
VytisknoutZobrazeno: 29. 9. 2022 13:29