The search functionality is under construction.
The search functionality is under construction.

Application of DES Theory to Verification of Software Components

Kunihiko HIRAISHI, Petr KUVCERA

  • Full Text Views

    0

  • Cite this

Summary :

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. In general, 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.

Publication
IEICE TRANSACTIONS on Fundamentals Vol.E92-A No.2 pp.604-610
Publication Date
2009/02/01
Publicized
Online ISSN
1745-1337
DOI
10.1587/transfun.E92.A.604
Type of Manuscript
PAPER
Category
Concurrent Systems

Authors

Keyword