Application of DES Theory to Verification of Software Components

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F09%3A00206712" target="_blank" >RIV/00216208:11320/09:00206712 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Application of DES Theory to Verification of Software Components

Popis výsledku v původním jazyce

Software model checking is typically applied to components of large systems. The assumption generation is the problem of finding the least restrictive environment in which the components satisfy a given safety property. There is an algorithm to compute the environment for properties given as a regular language. In this paper, we propose a general scheme for computing the assumption even for non-regular properties, and show the uniqueness of the least restrictive assumption for any class of languages. Ingeneral, dealing with non-regular languages may fall into undecidability of problems. We also show a method to compute assumptions based on visibly pushdown automata and their finite-state abstractions.

Název v anglickém jazyce

Application of DES Theory to Verification of Software Components

Popis výsledku anglicky

Software model checking is typically applied to components of large systems. The assumption generation is the problem of finding the least restrictive environment in which the components satisfy a given safety property. There is an algorithm to compute the environment for properties given as a regular language. In this paper, we propose a general scheme for computing the assumption even for non-regular properties, and show the uniqueness of the least restrictive assumption for any class of languages. Ingeneral, dealing with non-regular languages may fall into undecidability of problems. We also show a method to compute assumptions based on visibly pushdown automata and their finite-state abstractions.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

IEICE Transactions On Fundamentals Of Electronics Communications And Computer Sciences

ISSN

0916-8508

e-ISSN

—

Svazek periodika

E92A

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

JP - Japonsko

Počet stran výsledku

7

Strana od-do

—

Kód UT WoS článku

000265701000032

EID výsledku v databázi Scopus

—