Gaoyan Xie and ZheDang

Title: Gaoyan Xie and ZheDang

Authors: Gaoyan Xie and ZheDang

Abstract: This research introduces a new approach called model-checking driven black-box testing. This approach combines model-checking with traditional black-box software testing to tackle the problem of verifying systems with unspecified components. The idea is to derive a condition for an unspecified component such that the system satisfies the requirement iff the condition is satisfied by the component. This condition's satisfiability can be established by testing the component with test cases generated from the condition on-the-fly. The authors present algorithms for model-checking driven black-box testing, handling both CTL and LTL requirements for systems with unspecified components. They illustrate the ideas through some examples.

Main Research Question: How can we ensure that unspecified components function correctly in the host system where they are deployed?

Methodology: The authors propose a new approach called model-checking driven black-box testing. This approach combines model-checking, a formal method used to verify the correctness of systems, with traditional black-box testing, which focuses on the behavior of the system as a whole without considering the internal workings. The idea is to derive a condition for an unspecified component such that the system satisfies the requirement iff the condition is satisfied by the component. This condition's satisfiability can be established by testing the component with test cases generated from the condition on-the-fly.

Results: The authors present algorithms for model-checking driven black-box testing, handling both CTL and LTL requirements for systems with unspecified components. They illustrate the ideas through some examples.

Implications: This research has significant implications for the field of software development and verification. By combining model-checking with traditional testing, it provides a complete, sound, and automatic way to tackle the problem of verifying systems with unspecified components. This can lead to more reliable and safer systems, particularly in safety-critical and mission-critical domains.

Link to Article: https://arxiv.org/abs/0404037v2 Authors: arXiv ID: 0404037v2