Fiscal Year:
1994
Title:
Integration of Formal Verification with Real Time Design
Agency / Branch:
DOD / NAVY
Contract:
N/A
Award Amount:
$59,115.00
Abstract:
Formal 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.
Principal Investigator:
Mr. George L. Krasovec
3037904242
Business Contact:
Small Business Information at Submission:
Advanced System Technologies,
12200 E. Briarwood Avenue, Suite 260 Englewood, CO 80112
EIN/Tax ID:
DUNS:
N/A
Number of Employees:
Woman-Owned:
No
Minority-Owned:
No
HUBZone-Owned:
No