Advanced Search

Content Type

Topics

Publication Date

Verification of Evolving Software via Component Substitutability Analysis

  • Author(s): , , ,
  • Publish Date:
  • Publisher: Software Engineering Institute
  • SEI Identifier: CMU/SEI-2005-TR-008
  • Type: Technical Report
  • Description: 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.

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 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.

Cite This Report

Show Citation Formats

SEI

Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; & Sinha, Nishant. Verification of Evolving Software via Component Substitutability Analysis (CMU/SEI-2005-TR-008). Software Engineering Institute, Carnegie Mellon University, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7647

IEEE

Chaki. Sagar, Clarke. Edmund, Sharygina. Natasha, and Sinha. Nishant, "Verification of Evolving Software via Component Substitutability Analysis," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-2005-TR-008, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7647

APA

Chaki, Sagar., Clarke, Edmund., Sharygina, Natasha., & Sinha, Nishant. (2005). Verification of Evolving Software via Component Substitutability Analysis (CMU/SEI-2005-TR-008). Retrieved September 19, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7647

CHI

Sagar Chaki, Edmund Clarke, Natasha Sharygina, & Nishant Sinha. Verification of Evolving Software via Component Substitutability Analysis (CMU/SEI-2005-TR-008). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7647

MLA

Chaki, Sagar., Clarke, Edmund., Sharygina, Natasha., & Sinha, Nishant. 2005. Verification of Evolving Software via Component Substitutability Analysis (Technical Report CMU/SEI-2005-TR-008). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7647