MODEL BASED SOFTWARE BEHAVIOR VERIFICATION ENVIRONMENT FOR DEPENDABLE UPGRADES

"Rapid, model-based development along with perpetual and complexchange characterizes today's software-dependent mission criticalsystems. The costs associated with detecting and fixing errors insuch software-intensive systems can total 75% of the cost ofdeveloping that software. Furthermore, fixing errors late in thelife cycle is more costly due to the overall impact of code levelchanges. Hence, error reduction earlier in the development ofsoftware-intensive systems is needed. Trident proposes to delivera model-based verification methodology and supporting environmentprototype to detect inconsistencies and behavioral defects at theanalysis and design stage. The selective application of formalmethodologies (models), and the focus on error identification andcorrection, distinguishes our model-based verification approachfrom more traditional formal method approaches. In particular,the proposed framework constitutes three main components: (1)formal consistency analysis and management of UML structuralanalysis and design models, (2) analytical model checking of UMLbehavioral design models based on their finite state reachabilitygraphs using safe refinement, mutual compatibility, and protocolconsistency analysis methods developed during Phase I, and (3)model-based test suite generator subsystem. These test suiteswill be utilized by a test vector generator and underlying testdriver infrastructure to exercise the actual baseline system.BENEFIT