On Locally Strongest Assumption Generation Method for Component-Based Software Verification

Assume-guarantee reasoning, a well-known approach in component-based software (CBS) verification, is infact a language containment problem whose computational cost depends on the sizes of languages of the softwarecomponents under checking and the assumption to be generated. Therefore, the smaller language assumptions,the more computational cost we can reduce in software verification. Moreover, strong assumptions are moreimportant in CBS verification in the context of software evolution because they can be reused many times in theverification process. For this reason, this paper presents a method for generating locally strongest assumptions withlocally smallest languages during CBS verification. The key idea of this method is to create a variant techniquefor answering membership queries of the Teacher when responding to the Learner in the L–based assumptionlearning process. This variant technique is then integrated into an algorithm in order to generate locally strongestassumptions. These assumptions will effectively reduce the computational cost when verifying CBS, especiallyfor large–scale and evolving ones. The correctness proof, experimental results, and some discussions about theproposed method are also presented.Keywords: Assume-guarantee reasoning, Model checking, Component-based software verification, Locallystrongest assumptions, Locally smallest language assumptions.

A Transformation-Based Approach to Implication of GSTE Assertion Graphs

Generalized symbolic trajectory evaluation (GSTE) is a model checking approach and has successfully demonstrated its powerful capacity in formal verification of VLSI systems. GSTE is an extension of symbolic trajectory evaluation (STE) to the model checking ofω-regular properties. It is an alternative to classical model checking algorithms where properties are specified as finite-state automata. In GSTE, properties are specified as assertion graphs, which are labeled directed graphs where each edge is labeled with two labeling functions: antecedent and consequent. In this paper, we show the complement relation between GSTE assertion graphs and finite-state automata with the expressiveness of regular languages andω-regular languages. We present an algorithm that transforms a GSTE assertion graph to a finite-state automaton and vice versa. By applying this algorithm, we transform the problem of GSTE assertion graphs implication to the problem of automata language containment. We demonstrate our approach with its application to verification of an FIFO circuit.