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.

Current participants: Additional participants:

Collaborators: Qiming Zhao (DENSO) Past participants: Ioannis Filippidis (Alumni, CDS) Josefine Graebener (Postdoc, Aero) Tung Phan (Alumni, ME)

Objectives

1. 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).
2. 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.
3. Apply these methods (specification and design) to a proof-of-concept example of interest to DENSO.

References

• Failure-Tolerant Contract-Based Design of an Automated Valet Parking System using a Directive-Response Architecture. Josefine Graebener, Tung Phan-Minh, Jiaqi Yan, Qiming Zhao, Richard M. Murray. Submitted, 2021 Conference on Decision and Control (CDC).
• Contracts of Reactivity. Tung Phan-Minh and Richard M. Murray. Submitted, Int'l Conf on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019.
• Towards Assume-Guarantee Profiles for Autonomous Vehicles. Tung Phan-Minh, Karena X. Cai, Richard M. Murray. Submitted, 2019 Conference on Decision and Control (CDC).
• 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).

Research supported by DENSO International America, Inc

Agency: DENSO Grant number:

Start date: 1 Jul 2016 End date: 30 Mar 2020

Support: 1 graduate student + travel Reporting: Quarterly reports