Specification and Generation of Environment for Model Checking of Software Components

0090204 - ÚI 2008 RIV NL eng J - Článek v odborném periodiku
Pařízek, P. - Plášil, František
Specification and Generation of Environment for Model Checking of Software Components.
[Specifikace a generování prostředí pro model checking softwarových komponent.]
Electronic Notes in Theoretical Computer Science. Roč. 176, - (2007), s. 143-154. ISSN 1571-0661
Grant CEP: GA AV ČR 1ET400300504
Výzkumný záměr: CEZ:AV0Z10300504
Klíčová slova: software components * behavior protocols * model checking * automated generation of environment
Kód oboru RIV: JC - Počítačový hardware a software

Model checking of isolated software components is inherently not possible because a component does not form a complete program with an explicit starting point. To overcome this obstacle, it is typically necessary to create an environment of the component which is the intended subject to model checking. We present our approach to automated environment generation that is based on behavior protocols; to our knowledge, this is the only environment generator designed for model checking of software components. We compare it with the approach taken in the Bandera Environment Generator tool, designed for model checking of sets of Java classes.

Model checking izolovaných softwarových komponent není možný, protože komponenta netvoří kompletní program s explicitním místem začátku. Pro řešení této překážky je obvykle nutné vytvořit prostředí pro komponentu, kterou chceme ověřovat. Prezentujeme náš přístup ke automatickému generování prostředí, který je založen na protokolech chování. Podle našich znalostí je toto jediný generátor prostředí navržený pro model checking softwarových komponent. Srovnáváme to s přístupem implementovaným v nástroji Bandera Environment Generator, který je určen pro model checking množin tříd v jazyce Java.
Trvalý link: http://hdl.handle.net/11104/0151179