Component-Based QoS-Driven Synthesis of High Assurance Embedded Software

Software is an integral part of many complex embedded systems, such as avionics, scientific exploration, and on-board systems. However, poor software reliability is a major impediment to the success of these mission-critical systems. Testing, formal verification, and code synthesis techniques have been proposed to achieve more reliable software, with automated code synthesis being the most promising method. But synthesizing a complex system from scratch is costly. A more practical approach is to synthesize systems from existing components, i.e., component-based system synthesis (CBSS). Existing research in CBSS focuses on synthesizing systems bottom-up, which has severe limitations. We propose to achieve CBSS by combining the top-down and bottom-up approaches. Specifically, we develop techniques to achieve automated system decomposition and semi-automated system architecture synthesis. The IDEAL decomposition technique decomposes a system into ``IDEAL'' units that are mathematically composable and can be developed and evolved independently. Consequently, the technique assures system reliability and enables on-the-fly feature/technology upgrades. The QoS-based architecture synthesis technique seeks to assure system QoS properties by synthesizing an architecture that optimizes QoS objectives. It also facilitates on-board system adaptation due to resource and power constraints. Combined with bottom-up techniques, such as Amphion and pattern-based code synthesis, a dramatic leap in automated CBSS capability can be achieved. The proposed research will lead to sophisticated automation for synthesizing highly reliable, multi-mission capable avionics and exploration systems.