Temporal Logic Specifications for Control System Design in Automotive Systems
This project is a collaboration with DENSO as part of the Control Performance Modeling (CPM) project. We are exploring methods for handling “mixed specifications” that are spread between the multiple layers of control in a complex system. We are making use of tools from control theory and formal methods to provide a rigorous framework for specification, verification and synthesis of complex networked control systems, with application to automotive systems.
- Identify methods for establishing contracts (design specifications) between different layers of the design that insure that the overall properties of the system are met with the individual specifications at each layer of abstraction are satisfied. This type of specification will establish a pair of “vertical contract” (one to the next layer down in the hierarchy and the other to the next layer up).
- Given a set of specifications at the various layers, identify and/or develop the design tools required at least layer of abstraction to satisfy the contracts. We anticipate that many of these tools, especially at the inner and outer loop levels would be existing design methods (frequency domain design, optimization-based design, etc) with appropriate specifications. New tools may be needed to link the supervisory layer with the lower layers (basically this is the discrete to continuous challenge of hybrid systems.
- Apply these methods (specification and design) to a proof-of-concept example of interest to DENSO.
- A modal interface contract theory for guarded input/output automata with an application in traffic system design (Tung Phan-Minh, Steve Guo, Bastian Schürmann, Matthias Althoff, and Richard M. Murray, Submitted, 2019 American Control Conference (ACC))
- Hiding variables when decomposing specifications into GR(1) contracts (Ioannis Filippidis and Richard M. Murray, Submitted, 2017 Conference on Decision and Control (CDC))