search menu icon-carat-right cmu-wordmark

Verification of Evolving Software via Component Substitutability Analysis

Technical Report
This 2005 report describes the application of the SEI Architecture Tradeoff Analysis Method (ATAM) to the U.S. Army's Warfighter Information Network-Tactical (WIN-T) system.
Publisher

Software Engineering Institute

CMU/SEI Report Number
CMU/SEI-2005-TR-008
DOI (Digital Object Identifier)
10.1184/R1/6585872.v1

Abstract

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 the simultaneous use of over-approximations and under-approximations 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 toolset. The experimental evaluation of an industrial benchmark demonstrates encouraging results.

Cite This Technical Report

Chaki, S., Clarke, E., Sharygina, N., & Sinha, N. (2005, December 1). Verification of Evolving Software via Component Substitutability Analysis. (Technical Report CMU/SEI-2005-TR-008). Retrieved April 13, 2024, from https://doi.org/10.1184/R1/6585872.v1.

@techreport{chaki_2005,
author={Chaki, Sagar and Clarke, Edmund and Sharygina, Natasha and Sinha, Nishant},
title={Verification of Evolving Software via Component Substitutability Analysis},
month={Dec},
year={2005},
number={CMU/SEI-2005-TR-008},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6585872.v1},
note={Accessed: 2024-Apr-13}
}

Chaki, Sagar, Edmund Clarke, Natasha Sharygina, and Nishant Sinha. "Verification of Evolving Software via Component Substitutability Analysis." (CMU/SEI-2005-TR-008). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, December 1, 2005. https://doi.org/10.1184/R1/6585872.v1.

S. Chaki, E. Clarke, N. Sharygina, and N. Sinha, "Verification of Evolving Software via Component Substitutability Analysis," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Report CMU/SEI-2005-TR-008, 1-Dec-2005 [Online]. Available: https://doi.org/10.1184/R1/6585872.v1. [Accessed: 13-Apr-2024].

Chaki, Sagar, Edmund Clarke, Natasha Sharygina, and Nishant Sinha. "Verification of Evolving Software via Component Substitutability Analysis." (Technical Report CMU/SEI-2005-TR-008). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Dec. 2005. https://doi.org/10.1184/R1/6585872.v1. Accessed 13 Apr. 2024.

Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; & Sinha, Nishant. Verification of Evolving Software via Component Substitutability Analysis. CMU/SEI-2005-TR-008. Software Engineering Institute. 2005. https://doi.org/10.1184/R1/6585872.v1