Number of the records: 1  

Specification and Generation of Environment for Model Checking of Software Components

  1. 1.
    0090204 - ÚI 2008 RIV NL eng J - Journal Article
    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
    R&D Projects: GA AV ČR 1ET400300504
    Institutional research plan: CEZ:AV0Z10300504
    Keywords : software components * behavior protocols * model checking * automated generation of environment
    Subject RIV: JC - Computer Hardware ; 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.
    Permanent Link: http://hdl.handle.net/11104/0151179
     
Number of the records: 1