The goal of this project is to develop theory and technology for composing large embedded software applications subject to hard real-time constraints. Model-based integration will enable increased practical, achievable, reusable functionality for embedded systems and should decrease life-cycle cost for embedded software by an order of magnitude. Application domains of interest include weapon systems, embedded control system for transportation (such as airplanes and ground vehicles) and manufacturing/machine control systems.

The first issue that we try to solve is that a composition model and framework to support software integration of reusable components. Such components can be either home-made or off-the-shelf from different vendors. The second issue is a behavioral model to support implementation-independent behavior specifications and verifications. The third issue is timing verification of integrated software with considerations of underlying system performance.

Our approach to solve these issues combines object-oriented model, formal method and deadline distribution. A unified structure of reusable components with events as external interfaces is defined to support the structural integration. The behaviors of each component are modeled as a Finite State Machine (FSM), while the behaviors after integration are modeled as the Nested Finite State Machine (NFSM). The specification language based on NFSM is developed to support behavior specification and verification, and a FSM driver is designed for each component to support direct execution of the behavior specified in the specification language. The timing behaviors are specified in terms of end-to-end deadlines at different integration level, from component to system. The method we are using is deadline distribution, which is able to assign the system-level end-to-end deadline incrementally down to component-level with partial knowledge of timing performances. Since the same set of software components and configuration can have significant different timing performances on with different underlying supports (such as OS and network), we profile the timing behavior of underlying systems and use such information for timing verification.

A testbed constructed to evaluate the methodologies we develop is shown in the following figure.

(Big picture of the tes tbed)

We are going to develop both manufacturing/machine control applications and x-by-wire (engine control) applications with these methodologies and demonstrate the effectiveness.