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.

A trichordal temporal approach to digital coordination: the sociomaterial mangling of the CERN grid

This paper develops a sociomaterial perspective on digital coordination. It extends Pickering’s mangle of practice by using a trichordal approach to temporal emergence. We provide new understanding as to how the nonhuman and human agencies involved in coordination are embedded in the past, present, and future. We draw on an in-depth field study conducted between 2006 and 2010 of the development, introduction, and use of a computing grid infrastructure by the CERN particle physics community. Three coordination tensions are identified at different temporal dimensions, namelyobtaining adequate transparency in the present, modeling a future infrastructure, and the historical disciplining of social and material inertias. We propose and develop the concept of digital coordination, and contribute a trichordal temporal approach to understanding the development and use of digital infrastructure as being orientated to the past and future while emerging in the present.