Verification of periodically controlled hybrid systems: Application to an autonomous vehicle

This article introduces Periodically Controlled Hybrid Automata (PCHA) for modular specification of embedded 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. 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. For PCHAs with polynomial continuous vector fields, it is possible to check these conditions automatically using, for example, quantifier elimination or sum of squares decomposition. We examine the feasibility of this automatic approach on a small example. The proposed technique is also used to manually verify safety and progress properties of a fairly complex 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. © 2012 ACM.

Function propagation through nested systems

Concepts of function are central to design but statements about a device's functions can be interpreted in different ways. This raises problems for researchers trying to clarify the foundations of design theory and for those developing design support-tools that can represent and reason about function. By showing how functions relate systems to their sub-systems and super-systems, this article illustrates some limitations of existing function terminology and some problems with existing function statements. To address these issues, a system-relative function terminology is introduced. This is used to demonstrate that systems function not only with respect to their most local super-system, but also with respect to their more global super-systems. © 2012 Elsevier Ltd. All rights reserved.