What is it about?
Modern engineered systems, ranging from aircraft and spacecraft to automobiles, operate under stringent safety and performance requirements. These systems must function reliably in all foreseeable environments, including harsh settings such as unpaved terrain, the upper atmosphere, and outer space. As engineering innovation accelerates, an ever-expanding range of functionalities has been integrated into these systems without compromising safety. For example, today’s vehicles feature adaptive cruise control, lane-keeping assistants, and real-time GPS navigation–functions that were unheard of previously. The next generation of these systems is poised to become fully autonomous, capable of operating with minimal human supervision. These systems tend to be designed hierarchically, beginning with high-level requirements, which are progressively mapped to lower-level subsystems and components. While current approaches tend to be heuristic-driven, these methods suffer from lack of verifiability, i.e., the ability to derive rigorous correctness guarantees on the operation of the overall stack. This paper introduces a rigorous mathematical framework for designing layered control architectures that bridge the gap between planning and safe control. We present novel mechanisms termed contract embeddings, which allow for the automatic and rigorous tracing of requirements across different layers. The approach is built on “contracts,” which are mathematical models enabling compositional system design with rigorous correctness guarantees. Contract embeddings allow contracts to be traced across heterogeneous levels of abstraction, thus enabling the design of layered control architectures that are full-stack verifiable from the top-level plan down to the physical control inputs.
Featured Image
Photo by Jack Dong on Unsplash
Why is it important?
Autonomous systems are an exciting new frontier, driven by the revolution in computing, sensing, and artificial intelligence. Managing the immense complexity of these systems requires a new approach to design. This work represents one of the first efforts to present a general, rigorous mathematical framework for layered control architectures. It addresses the need to model and analyze the interactions between heterogeneous components—from sensing and actuation to computation and communication. By moving away from ad hoc procedures for implementing and testing specific instances of hardware and software components, this framework facilitates system-level design space exploration. This allows engineers to develop architectures using repeatable processes that guarantee desirable properties, essential for the safe deployment of complex autonomous systems.
Perspectives
A critical hurdle in the design of control architectures—the “brains” responsible for making decisions that achieve system goals while strictly meeting requirements—is their typically layered organization, which must coordinate two distinct levels of operation: (i) planning, producing a sequence of high-level actions to satisfy a mission objective; and (ii) safe control, generating the low-level physical inputs required to implement that plan safely. For example, a lunar rover planner may dictate visiting a sequence of regions on the moon, while the controller manages position, velocity, and heading to execute that movement safely. The primary difficulty lies in guaranteeing consistency across these abstraction layers to provably satisfy mission objectives and safety requirements simultaneously. Our approach provides a rigorous, yet flexible design framework which can be adapted to different applications.
Nikhil Vijay Naik
Read the Original
This page is a summary of: Contract Embeddings for Layered Control Architectures, ACM Transactions on Embedded Computing Systems, September 2025, ACM (Association for Computing Machinery),
DOI: 10.1145/3764587.
You can read the full text:
Resources
Contributors
The following have contributed to this page
