Verification of Evolving Software via Component Substitutability Analysis

The software architecture of a software-intensive system greatly determines system quality. Evaluating that architecture for fitness of purpose before the system is implemented or undergoes a major modification is a cost-effective approach to uncovering deficiencies early and reducing risk. When used appropriately, software architecture evaluations can have a favorable effect on a delivered or modified government system. This technical note describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system. The WIN-T system is being developed by a government-contractor team headquartered at the U.S. Army's Communications and Electronics Command (CECOM) in Ft. Monmouth, New Jersey. This technical note presents the WIN-T program context, the definition of software architecture, and the background of the WIN-T organization and system being evaluated. It also provides a general overview of the ATAM process, describes the application of the ATAM to the WIN-T system, presents important results, and summarizes the benefits the program received. The report presents an automated and compositional procedure to solve the component substitutability problem. The solution contributes two techniques for checking the correctness of software upgrades: (1) a technique based on simultaneous use of overapproximations and underapproximations obtained via existential and universal abstractions and (2) a dynamic assume-guarantee reasoning algorithm in which previously generated component assumptions are reused and altered "on the fly" to prove or disprove the global safety properties on the updated system. When upgrades are found to be non-substitutable, the solution generates constructive feedback that shows developers how to improve the components. The substitutability approach has been implemented and validated in the Component Formal Reasoning Technology (COMFORT) model checking tool set. The experimental evaluation of an industrial benchmark demonstrates encouraging results.