Application of DES Theory to Verification of Software Components

Kunihiko HIRAISHI  Petr KUVCERA 

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences  Vol.E92-A  No.2  pp.604-610
Publication Date: 2009/02/01
Online ISSN: 1745-1337
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: Concurrent Systems
Keyword: 
discrete event systems,  software component verification,  supervisory control, 

Full Text: PDF(275.6KB)

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.