Download Printable PDF

Model Checking of Software Designs

With ONR support, GrammaTech and sub-contractor Formal Systems (Europe) Ltd. are integrating FDR2, Formal Systems' advanced state space exploration tool, with the Rational Rose RealTime UML environment. This integration will enable software engineers to formally verify critical properties of the design of embedded systems. Design verification allows developers and designers to detect errors early in the development life-cycle, reducing the substantial time and cost of correction, making "on-time and under-budget" a reality.

Formal methods offer great promise for the elimination of errors in distributed, real­time, network­centric warfare software, but before they can be widely adopted in industry, they must be supported by good tools readily acceptable to professional programmers. Existing formal­methods tools are hobbled by weak user­interfaces, and severely limited capabilities for integration with other tools. In an existing SBIR Phase II project, GrammaTech is seeking to remedy these problems by developing a professional­quality, standards­compliant, customizable, portable, common interface tailored to formal­methods applications. GrammaTech proposes to complement the existing SBIR project by building a vendor-independent UML communication layer, so that formal methods tools can be integrated with different vendor's UML implementations with minimal effort; by integrating FDR2 with Rational's Rose; by adapting GrammaTech's CodeSurfer system to provide slicing and navigation in dependence graphs manipulated by Formal Methods tools; and by interacting closely with potential industrial users of the technology.

DoD is moving rapidly to put networks, with their ability to disseminate information quickly, at the center of its military strategy during the next decade. Although DoD will make heavy use of commercial products, it is no ordinary commercial customer. Warfighting networks demand high connectivity, reliability, and redundancy, as well as data integrity and data security; single­point failures can not be tolerated, and systems must degrade gracefully in the event of a failure. Getting distributed real­time software right is notoriously difficult.

Because installation of network­centric warfighting infrastructure represents such a large and long term investment, it must be done right the first time. Thus, in (say) the Navy's IT­21 project, the system and software production methodologies themselves need high assurance. Designs must be thoroughly simulated, debugged, validated, and (if possible) verified before implementation. Design flaws discovered during or after implementation can be horrifically expensive to correct. UML. The Unified Modeling Language (UML) is used for specifying, visualizing, constructing, and documenting the artifacts of software systems. It simplifies the complex process of software design, making a "blueprint" for construction. UML incorporates Harel's Statecharts for finite state modeling. Although the UML definition was led by three software methodologists (Booch, Jacobson, and Rumbaugh) from one company (Rational Software), its adoption as an standard throughout the object­oriented analysis and design (OOAD) industry has been a watershed event of considerable importance to DoD. Rational Software's recent acquisition of ObjecTime has merged Selic's ROOM methodology with UML, a combination uniquely suited for embedded systems.

Although DoD contractors are heavy users of OOAD systems, their value has been limited by the absence of powerful reasoning and formal analysis techniques that validate the models after they have been produced. Indeed, the "analysis" in OOAD is informal "problem analysis" that precedes design. Once a model has been created, it is rarely subjected to any formal analysis. This accounts, in part, for OOAD's poor reputation in some circles as "mere documentation". Without formal analysis of models, OOAD has not been yielding a full return on its investment.

Papers

Related Links:


Free Trial | Products | Customers | Support | News | Jobs | About Us         © 2007-2008, GrammaTech, Inc. All rights reserved.