Temporal Logic Specifications for Control System Design in Automotive Systems

From Murray Wiki
Jump to navigationJump to search

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:


  • Qiming Zhao (DENSO)

Past participants:


  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.


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