Idle speed control synthesis using an assume-guarantee approach

The goal of an idle control for automotive engines is to maintain the engine speed within a given range, robustly with respect to load torque disturbances acting on the crankshaft. Mean value models have been used in the past to design idle control algorithms. However, the behavior of the torque generation process and the dynamics of the power train are not captured with enough accuracy to guarantee that the idle control specifications as given by car makers are met. We use a cycle-accurate hybrid model to overcome these obstacles. To tackle the complexity of the controller design, the system is decomposed in three parts. For each part in isolation, a control law is derived for a simplified model, assuming that the other parts can be controlled to yield appropriate inputs. The overall control strategy is then applied to the system. Hence, the correct interaction of the feedback loops is formally verified using an assume-guarantee approach, to ensure that the behavior of the controlled system meets the given specifications.