Embedded systems consist of a collection of components that interact with each other and with their environment through sensors and actuators. Embedded systems are characterized by the nature of resource limitations and constraints that need to be considered during development and deployment. Embedded systems have been developed traditionally in an ad-hoc manner by practicing engineers and programmers. The existing technology for embedded systems does not effectively support the development of reliable and robust embedded systems. The effective development of embedded systems requires a collection of tools to capture requirements, to construct, analyze and simulate specifications, to generate and test implementations, and to monitor and check implementations at run-time. Moreover, it should be possible to use these tools together in horizontally and vertically intergrated manner.
The goal of the proposed research is to develop a framework for the integrated use of a suite of methods and tools for the specification, analysis, development, testing, prototyping, simulation and monitoring of embedded software. The framework is called HASTEN (High Assurance Systems Tools and Environments) and will be based on systems that the proposers have been studying separately for some time and can also include systems that are developed elsewhere. The primary methods of interest are: formal specifications, test generation from specifications, automated verification, prototyping and simulation, and run-time monitoring and checking. Each of the methods has its own strengths. Taken within the context of an `end-to-end' view of the software life cycle they can achieve together more than any one of them could do. However, these methods apply to different representations of the system at different points in its development and deployment. Furthermore, some of these methods need be enhanced to handle the resource limitation and constraint characteristics of embedded systems. The significant effort of the proposed work will be to enchance individual methods to support embedded systems.
In order to make these methods interoperable, we will study abstraction techniques that will facilitate automated translation between the artifacts used by various formal methods as well as a unified interpretation of results obtained from them. While most of the analysis will be performed using a formally specified system design, we will use the techniques of testing and monitoring to relate these results to the implemented system from which high assurance is expected. We will evaluate the proposed techniques on a collection of Army and/or DoD embedded system applications to be chosen to represent domains requiring high assurance and real-time requirements.