Component-based software development has posed a serious challenge to system verification since externally-obtained components could be a new source of system failures. This issue can not be completely solved by either model-checking or traditional software testing techniques alone due to several reasons: 1) externally obtained components are usually unspecified partially specified; 2)it is generally difficult to establish an adequacy criteria for testing a component; 3)components may be used to dynamically upgrade a system. This paper introduces a new approach (called model-checking driven black-box testing ) that combines model-checking with traditional black-box software testing to tackle the problem in a complete, sound, and automatic way. The idea is to, with respect to some requirement (expressed in CTL or LTL) about the system, use model-checking techniques to derive a condition (expressed in communication graphs) for an unspecified component such that the system satisfies the requirement iff the condition is satisfied by the component, and which can be established by testing the component with test cases generated from the condition on-the-fly. In this paper, we present model-checking driven black-box testing algorithms to handle both CTL and LTL requirements. We also illustrate the idea through some examples.
Peled et. al. @cite_27 @cite_29 @cite_5 studied the issue of checking a black-box against a temporal property (called black-box checking). But their focus is on how to efficiently establish an abstract model of the black-box through black-box testing , and their approach requires a clearly-defined property (LTL formula) about the black-box, which is not always possible in component-based systems. Kupferman and Vardi @cite_28 investigated module checking by considering the problem of checking an open finite-state system under all possible environments. Module checking is different from the problem in (*) mentioned at the beginning of the paper in the sense that a component understood as an environment in @cite_28 is a specific one. Fisler et. al. @cite_24 @cite_6 proposed an idea of deducing a model-checking condition for extension features from the base feature, which is adopted to study model-checking feature-oriented software designs. Their approach relies totally on model-checking techniques; their algorithms have false negatives and do not handle LTL formulas.
@cite_28 @cite_29 @cite_6 @cite_24 @cite_27 @cite_5
1493173186 2141399917 1968542268 1482663303 1539019418
The AMC (for adaptive model checking) system allows one to perform model checking directly on a system, even when its internal structure is unknown or invisible. It also allows one to perform model checking using an inaccurate model, incrementally improving the model each time that a false negative (i.e., not an actual) counterexample is found. Feature-oriented software designs capture many interesting notions of cross-cutting, and offer a powerful method for building product-line architectures. Each cross-cutting feature is an independent module that fundamentally yields an open system from a verification perspective. We describe desiderata for verifying such modules through model checking and find that existing work on the verification of open systems fails to address most of the concerns that arise from feature-oriented systems. We therefore provide a new methodology for verifying such systems. To validate this new methodology, we have implemented it and applied it to a suite of modules that exhibit feature interaction problems. Our model checker was able to automatically locate ten problems previously found through a laborious simulation-based effort. Most existing modular model checking techniques betray their hardware roots: they assume that modules compose in parallel. In contrast, collaboration-based software designs, which have proven very successful in several domains, are sequential in the simplest case. Most interesting collaboration-based designs are really quasi-sequential compositions of parallel compositions. These designs demand and inspire new verification techniques. This paper presents algorithms that exploit the software's modular decomposition to verify collaboration-based designs. Our technique can verify most properties locally in the collaborations; we also characterize when a global state space construction is unavoidable. We have validated our proposal by testing it on several designs. Two main approaches are used for increasing the quality of systems: in model checking, one checks properties of a known design of a system; in testing, one usually checks whether a given implementation, whose internal structure is often unknown, conforms with an abstract design. We are interested in the combination of these techniques. Namely, we would like to be able to test whether an implementation with unknown structure satisfies some given properties. We propose and formalize this problem of black box checking and suggest several algorithms. Since the input to black box checking is not given initially, as is the case in the classical model of computation, but is learned through experiments, we propose a computational model based on games with incomplete information. We use this model to analyze the complexity of the problem. We also address the more practical question of finding an approach that can detect errors in the implementation before completing an exhaustive search. Model checking is a technique for automatically checking properties of models of systems. We present here several combinations of model checking with testing techniques. This allows checking systems when no model is given, when the model is inaccurate, or when only a part of its description is given.