An integrated verification and testing environment

摘要

AbstractA verification and testing environment that includes static analysis, symbolic execution, and dynamic analysis capabilities is presented. Tool integration and co‐operation are promoted through use of an intermediate program representation and a system data manager. A substantial user interface aids application of the tools. Their use is guided by a verification and testing methodology on which the system's design is based. The environment has been engineered to support the production of flight control software written in HAL/S. The environment itself is written in Pascal and is designed to be portable. Several development experiences are described. The environment demonstrates that a strong, unified verification and testing environment can be bui it serves as a basis for future investigation