SBIR Phase II: Advanced Formal Techniques for Dependable Reactive Systems

Reactive Systems Inc, Falls Church VA

Investigators

Abstract

This Small Business Innovation Research (SBIR) Phase II project will develop the automated tool support that will enable engineers to deploy powerful and mathematically rigorous, yet easy-to-use and cost-effective, techniques to model, analyze and implement correct and reliable reactive software systems. Such systems are intended to maintain an ongoing interaction with their environment in order to provide appropriate responses to stimuli the environment generates. Examples include the embedded software found in medical, automotive, aeronautical, consumer-electronic, e-commerce, and telecommunications applications. Many of these are safety- or business-critical. Providing an enabling technology for the cost-effective development of correctly functioning reactive systems would thus be of great social and economic benefit to the nation. The main tangible outcome of the proposed effort and the flagship product will be the React tool environment. React will allow reactive-system designers to create mathematical models of their systems; validate models via simulation and automatic verification; and automatically generate implementations or test suites from models. The key innovation of the proposed technology is its reliance on powerful formal techniques, developed by RSI for modeling systems and validating properties of these models in a fully automatic fashion.