Automatic verification of transition systems with unspecified components

Model checking has had a substantive impact on the verification of software, and nowadays more and more software are developed with components manufactured by a third party. This paper examines the verification of systems with unspecified components. The method is based on the model of oracle automaton and related checking algorithms. Two problems in the previous checking algorithm are found and analyzed. To correct the previous error, an efficient algorithm for verifying the system with unspecified components is introduced. The new algorithm not only corrects the errors but also extends the original algorithm to multi-oracle finite automaton. The set of input transitions that are not related to the oracles is minimized by the new algorithm. Further, a prototype tool for checking oracle finite automaton (OFA) is implemented. It has advantages for modeling systems with unspecified components and merging different checking algorithms. Finally, the architecture and design of this tool are illustrated.