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.
Benefit: The success of this work wil enable engineers involved in the development of critical software applications for DoD and commercial customers to produce highly reliable software. This technology will be applicable to any Navy development effort containing ultrareliable or life-critical components, such as the Aegis Battle Management System, the Trident Fire Control System, or the AN/BSY2 Submarine Control System. Commercial development efforts involving high reliability requirements such as in medical, industrial, and transportation system will benefit as well.
Keywords: Hard Real Time, Hard Real Time, CASE, Structured Analysis, Design View Translation, distributed systems, Meta Modeling, Formal Verification, CDIF
