Integration of Formal Verification with Real Time Design
Small Business Information
12200 E. Briarwood Avenue,, Suite 260, Englewood, CO, 80112
Mr. George L. Krasovec
AbstractFormal methods based on rigorous mathematical specification and verification techniques have been shown to be a feasible way of identifying design errors early in the development of complex, ultrareliable computer systems. However, the mathematical expertise required to exercise formal verification systems for non-trivial applications has restricted their use to formal methods experts. The purpose of the proposed R&D is to extend the availability of formal methods of adequately trained engineers by coupling various real-time structured analysis design tools with any of a family of general purpose verification systems. Phase I research will determine the feasibility of developing an automated, extensible tool, called FM*Link, that supports the process of formal specification and reasoning about the temporal, liveness, and safety properties of hard real-time systems. Goals of this research include the extension of the RT/SA notation to cover additional formal method semantics within the system engineering domain and the preliminary design of a translator which converts state-based RT/SA behavior models and other design factors into verification system input modules. During Phase I, a proof-of-concept translator will be built and integrated into an in-house R&D tool framework as a demonstration of technical feasibility.
* information listed above is at the time of submission.