The design and implementation of modern control systems involves different modes of operation within an uncertain environment, several physical and logical layers of continuous and discrete abstractions, heterogeneous and evolving hardware and software components, distribution across multiple (semi) autonomous agents, and real-time performance in possibly faulty computing and communication environments. The complexity inherent in these systems can currently be overcome only by overdesign, namely, by the overly conservative decoupling of functions, modes, components, agents, layers of abstraction, and time slices for design, and by reintegration using test. This methodology comes at considerable costs, both in design effort and system efficiency. We propose to address the dual problems of overdesign and system integration by developing tools that support all stages of a new, software-based design methodology. To avoid overdesign, we plan to put forward a collection of interoperable formal methods and tools that permit the accurate analysis of the interaction of different system perspectives, including tools for heterogeneous and hierarchical modeling, control synthesis and verification. To reduce the role of test in system integration, we put forward a collection of semi-formal methods and tools that support the suitable decomposition and interference-free recomposition of different system perspectives, including tools for decentralized and hierarchical control architectures, software analysis and simulation. As technology driver and testbed for the tools, we will use the scenario of multiple coordinating UAVs (uninhabited air vehicles). A second application area that will be explored is distributed, full authority, aeroengine control.
System decomposition, abstraction, and distribution lead naturally to subproblems that can be addressed using formal methods and tools, such as mathematical modeling, control law synthesis, and control implementation verification. We classify these methods and tools relying heavily on mathematical formulations of the underlying problem as ``formal.'' They will be complemented by ``semi-formal'' techniques that address the problem of system integration. Ultimately, control designs for individual components, modal views, levels of abstractions, and autonomous agents need to be integrated and function as a single complex system with multiple hardware (sensors, actuators, processors, networks) and software parts. Most of the cost in system development is currently spent on informal system integration techniques such as testing. The problem is exacerbated by an ever increasing reliance on software, whose functionality and implementation changes over time and whose real-time behavior is difficult to predict. Since a mathematically rigorous, wholistic approach to the design and analysis of a complex system quickly hits the limits of computation, we put forward a set of semi-formal techniques that aid in the integration of formally developed parts. These techniques include architectural principles, and software analysis and simulation tools for integrated control systems. Thus, in this project, we will develop tools for modeling, deriving, and verifying control laws and their computational realization (``formal tools''), as well as tools for integrating, analyzing, and simulating the software that realizes multi-modal, multi-level, distributed control designs (``semi-formal tools'').