SBIR-STTR Award

Integration of Formal Verification with Real Time Design
Award last edited on: 6/8/2021

Sponsored Program
SBIR
Awarding Agency
DOD : Navy
Total Award Amount
$59,115
Award Phase
1
Solicitation Topic Code
N93-138
Principal Investigator
George L Krasovec

Company Information

Advanced Systems Technologies Inc (AKA: Advanced System Technologies Inc)

12200 East Briarwood Avenue Suite 260
Englewood, CO 80112
   (303) 790-4242
   N/A
   N/A
Location: Single
Congr. District: 06
County: Arapahoe

Phase I

Contract Number: N00014-94-C-0036
Start Date: 2/1/1994    Completed: 7/31/1994
Phase I year
1994
Phase I Amount
$59,115
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

Phase II

Contract Number: ----------
Start Date: 00/00/00    Completed: 00/00/00
Phase II year
----
Phase II Amount
----