The search functionality is under construction.

The search functionality is under construction.

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

The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.

Copy

Kunihiko HIRAISHI, Petr KUVCERA, "Application of DES Theory to Verification of Software Components" in IEICE TRANSACTIONS on Fundamentals,
vol. E92-A, no. 2, pp. 604-610, February 2009, doi: 10.1587/transfun.E92.A.604.

Abstract: 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.

URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E92.A.604/_p

Copy

@ARTICLE{e92-a_2_604,

author={Kunihiko HIRAISHI, Petr KUVCERA, },

journal={IEICE TRANSACTIONS on Fundamentals},

title={Application of DES Theory to Verification of Software Components},

year={2009},

volume={E92-A},

number={2},

pages={604-610},

abstract={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.},

keywords={},

doi={10.1587/transfun.E92.A.604},

ISSN={1745-1337},

month={February},}

Copy

TY - JOUR

TI - Application of DES Theory to Verification of Software Components

T2 - IEICE TRANSACTIONS on Fundamentals

SP - 604

EP - 610

AU - Kunihiko HIRAISHI

AU - Petr KUVCERA

PY - 2009

DO - 10.1587/transfun.E92.A.604

JO - IEICE TRANSACTIONS on Fundamentals

SN - 1745-1337

VL - E92-A

IS - 2

JA - IEICE TRANSACTIONS on Fundamentals

Y1 - February 2009

AB - 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.

ER -