Difference between revisions of "Temporal Logic Specifications for Control System Design in Automotive Systems"
From Murray Wiki
Jump to navigationJump to search
| Line 1: | Line 1: | ||
{{righttoc}} | {{righttoc}} | ||
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. | |||
{| cellpadding=0 cellspacing=0 width=80% | {| cellpadding=0 cellspacing=0 width=80% | ||
| Line 11: | Line 11: | ||
| | | | ||
Collaborators: | Collaborators: | ||
* Qiming Zhao (DENSO) | |||
Past participants: | Past participants: | ||
{{project past participants}} | {{project past participants}} | ||
| Line 17: | Line 17: | ||
== Objectives == | == Objectives == | ||
[[Image: | [[Image:denso16-cpm.png|right|400px]] | ||
# 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. | |||
== References == | == References == | ||
| Line 24: | Line 26: | ||
[[Category:Pending project]] | [[Category:Pending project]] | ||
[[Category:Subgroup projects]] | <1-- [[Category:Subgroup projects]] --> | ||
{{Project | {{Project | ||
|Title=Temporal Logic Specifications for Control System Design in Automotive Systems | |Title=Temporal Logic Specifications for Control System Design in Automotive Systems | ||
Revision as of 12:40, 11 June 2016
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:
Past participants:
|
Objectives
- 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.
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).
<1-- -->
|
|
|
