Specifikace a generování prostředí pro model checking softwarových komponent

Abstrakt

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.

Klíčová slova

• Specification
• Generation
• Environment
• Model
• Checking
• Software
• Components