The authors use the term “cyberphysical system” to describe an event-driven computer system where some events must be processed “as soon as possible.” Unlike real-time systems, these systems do not have explicit timing constraints. Instead, event handlers can be given a priority partial ordering, allowing higher priority handlers to preempt lower priority ones.

The paper uses as a working example an embedded automated insulin pump. In this case, the system has two main functions: deliver insulin and download delivery logs. A safety requirement on the system ensures that downloading does not occur during delivery.

The paper describes a programming language, E^#, that can facilitate the formal verification of safety and liveness for cyberphysical systems. An important feature of the language is the requirement that all event handlers be atomic. This simplifies the formal arguments, as it allows for the verification of each handler independently. The paper sketches the language and shows how E^# uses modal operators (“always” and “eventually”) to permit the specification of constraints such as the one above on download and delivery, but not specific timing constraints. Verification can be achieved using Hoare logic rules for language operations, graphs that encode the ways in which one event can cause others, and model checking.

In addition to the insulin pump, the paper considers a bridge traffic controller. In the paper’s one reference to timing considerations, the traffic controller uses timers to allow the bridge to empty. It is not clear how the language and methods would scale to a large system, nor is there any discussion of how to implement the language.

The paper is for people interested in the design of safe cyberphysical systems and students seeking applications of verification techniques.