Verification of Periodically Controlled Hybrid Systems: Application to An Autonomous Vehicle

Tichakorn Wongpiromsarn, Sayan Mitra, Richard M Murray, Andrew Lamperski
ACM Transactions on Embedded Computing Systems, 2009 (Submitted)

This paper introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of hybrid control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim, changing the set-point of the system. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set-point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. Checking these conditions can be automated using, for example, the constraint-based approach, quantifier elimination, or sum of squares decomposition.This paper introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of hybrid control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim, changing the set-point of the system. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set-point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. Checking these conditions can be automated using, for example, the constraint-based approach, quantifier elimination, or sum of squares decomposition. The proposed technique is used to verify safety and progress properties of the planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner generated pathsThis paper introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of hybrid control systems. In a PCHA, control actions that change the control input to the plant occur roughly periodically, while other actions that update the state of the controller may occur in the interim, changing the set-point of the system. Such actions could model, for example, sensor updates and information received from higher-level planning modules that change the set-point of the controller. Based on periodicity and subtangential conditions, a new sufficient condition for verifying invariant properties of PCHAs is presented. Checking these conditions can be automated using, for example, the constraint-based approach, quantifier elimination, or sum of squares decomposition. The proposed technique is used to verify safety and progress properties of the planner-controller subsystem of an autonomous ground vehicle. Geometric properties of planner generated paths are derived which guarantee that such paths can be safely followed by the controller.

Preprint
Downloading and printing FAQ