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