In software terms, a `script' is a collection of commands to be performed in a particular order under various conditions. Imperative programming languages, such as assembly language, Java and the unix shell language are frequently used for scripting. These languages are used to control a collection of devices or to otherwise automate a process. They are unrestricted in expressibility and hence reasoning about their behaviour or their interaction with other such scripts is hard. When a script phrased in a decidable language controls and reacts to objects containing undecideable code (or exhibiting unpredicatable behaviour), the system becomes undecidable as a whole. Nonetheless, it is our belief that there are significant benefits from using decidable code at the highest levels - the level of application scripting. Model checkers are good at exploring system behaviour over all possible behaviours of the undecidable subsystems.
In our approach, complex, autonomous or undecidable behaviour is partitioned and placed in `pebbles' that interact using a constrained controlling language called Pushlogic. Pushlogic object level is a byte code, designed as an intermediate code for automated reasoning with respect to several execution models that vary in how fast a program can be checked and how accurately effects of message loss or delivery delay are included. Pushlogic source level looks like an unconstrained, imperative, multi-threaded OO-like language where the partitioning between decidable and undecidable constructs is not immediately apparent to the programmer.
Pushlogic object consists of bundles containing rules. Rules are either consistency assertions expressed in temporal logic or else executable rules that define a finite state machine or `mechanism.' Bundles run inside a domain of participation (DoP). Dynmaic storage allocation only occurs when new bundles of rules are loaded into a running DoP. Bundles arrive either when a new pebble that requires control arrives, or when a new application is started, expressed in Pushlogic. Before a bundle can be loaded, the union of the rules in the new bundle is formed against those already in the domain. If any of the rules are inconsistent or any of the temporal logic rules (existing or new) will not hold under the combined mechanism, the bundle cannot be loaded.
Pushlogic is a finite-state language, but the amount of state in a Pushlogic domain varies over time, as new bundles or pebbles enter and leave the DoP.
Instead of being executable, a bundle may be a plant bundle that models reactive and autonomous behaviour not programmed using Pushlogic. A world model mirrors the behaviour of the physical system or plant or other software agents. In many real systems, there are predictable effects from the output of actuators that may be detected by sensors. These feedback effects can cause undesirable effects, such as deadlock or oscillations, that Pushlogic can detect before they occur. Run-time monitoring of the conformance of the real system with its world model can also detect various faults and failures in sensors and actuators and so on.
We use the term `mechanism' for our combination of FSMs because it models not only the effect of inputs on outputs and internal state, but because a mechanical system of levers and cogs can sometimes be operated in reverse, with pressure applied to an output causing an `input' to change. Pushlogic implements a form of compensation where rules are executed in reverse. This is called a pushback. We believe this greatly reduces the effort required to handle errors and failures. To start with, less code needs to be written, but the real win is that error recovery procedures then add little overhead to the automated rule checking.
Pushlogic runs on real platforms under its own interpreter or compiled to native code (or in one extension, to .net bytecode). Two main execution platforms have been developed: a unix workstation application called pusher that also sports a GTK-based GUI if needed, and an embedded version that runs on Molly processor cards or on bare PC motherboards without OS. A geographical physical modelling system called vworld is currently being developed that enables a number of virtual, interacting pebbles to be visualised on a canvas.
For checking purposes, Pushlogic defines several execution models that successively decrease in level of modelling detail. All models are suitable for finite-state model checking. The aim is to enable a more-rapid check of a less-detailed execution model to be verified before proceeding to slower, yet more-detailed modelling.
Pushlogic has been developed for a year or so, and its first compiler and run time system are becoming stable. We are now implementing the DoP manager, that provides real-time checking of bundles joining the DoP, so that Pushlogic can provide a scripting language for safety-critical systems with a dynamic population of sensors, actuators and applications. We are also adding arrays and remote procedure call clients1.1
Figure 1.1 shows the Pushlogic toolchain. Source bundles are compiled with libraries to generate dry object bundles that do not refer to specific pebbles by name. A subsequent re-hydration stage implements such bindings, and a given bundle may join the DOP more than once, as illustrated, but using different bindings for each instance. Several bundles may run on a single execution platform, but the behaviour of the system is, as far as possible, the same as though they were distributed over the network. For a self-contained device using ROM'd code, such as the Heating Controller presented later, part of the re-hydration can be performed before canning the code to ROM, so that the code is bound to the local pebbles, and part of it can be done later, for instance to bind to other devices encountered in the domain at run time.
Ubiquitous computing architectures, such as those based on XML, UPnP and XMLRPC have matured in terms of their support for automatic registration in directory services and description of the command APIs offered by devices for asynchronous eventing and RPC. However, until now there has been little emphasis on automated description of the proactive behaviour of applications running in such an environment. These applications invoke operations at various APIs available on the local device or over the network. Without these applications, the APIs would remain unused and pointless. However, when dozens of applications are running at once in an environment like a home, car or hotel room, they are bound to interact and occasionally disagree about the current correct setting of some value, such as brightness of room lights or locked state of a door.
A solution to this problem is being explored within our AutoHAN project[5]. In our approach, each device must be architecturally componentised into some number of passive `Pebbles' and a set of `Pushlogic' rules that control these Pebbles. A Pebble can represent a fairly large chunk of functionality: it could be a hardware component, such as a wall-mounted keypad or a fire alarm sounder, or it could be an entirely virtual device, hosted somewhere on the network, such as a speech recogniser. Each Pebble is able to describe itself using a reflection API, such as that provided by UPnP or XMLRPC, and register itself with dynamic directory services of the form required for ad hoc computing. Together with MIT Project O2S we have developed a complete architecture for this sort of behaviour. However, most importantly, no Pebble is able to interact with any other Pebble under its own volition. Instead, all proactive and interactive behaviour must be held outside the Pebbles in small application scripts that actually cause something to happen.
For instance, consider a DVD player designed to operate with our
environment. As illustrated in figure ![[*]](file:/usr/share/latex2html/icons/crossref.png){kind=icon}
,
each of its major, internal components is a separate
Pebble (at the architectural modelling layer). The Keypad Pebble will
not make direct contact with the Mechanism Pebble. Instead, when the
`play' key on the keypad is pressed, the application script that glues
together the DVD components will convey the event to the Mechanism
Pebble to commence playing. Using dedicated wiring to carry the
output signals, as is common practice until now, the mechanism will
be connected directly to the physical output sockets on the back of the
unit. Accordingly, the application does not have to do anything to
convey the multimedia stream to its destination. In the future, the
media will also stream over a packet switched network using a virtual
connection. It is then the job of the application to set up the
connection parameters, although not to copy the data itself. In this scenario, the
embedded application is having a proactive effect on other Pebbles in
the local environment - for instance, it is routing audio and video to
them. We use the term `feature interaction' to describe the general
situation where independent application scripts try to perform
disagreeing operations on a Pebble at the same time. In the DVD
example, feature interaction would arise when two DVD players try to
route video to one display at once.
Using the Pushlogic approach, all application scripts within an environment of participating devices must either be implemented in Pushlogic, or else summarised in it. The various routes to using Pushlogic are illustrated in figure 1.1. A high-level language, such as Pushlogic Source, is compiled by the compiler to generate the Pushlogic object code. This is then canned in ROM for direct interpretation in the embedded target or further compiled to native code for a micro-controller. The latter approach may serve to use less RAM. In all routes, a Pushlogic form of each application is made available for checking in advance of the application being allowed to join the environment of participation. We use the term `code reflection' for the concept of application software being examinable in some for or another.
Pushlogic programs consist of `bundles' of rules. A bundle must be checked before it is allowed to commence execution and may also be `re-hydrated' before checking. A bundle contains rules and meta information.
Bundles have access to several namespaces.
A Pushlogic program executes in a domain of participation (DoP). A DoP typically encompasses some number of Pushlogic execution engines. DoPs may become merged or federated, as explained in section 8.3. Various agents may attempt to insert a bundle into a domain of participation. For instance, a starting bundle may be loaded by the agent that first set up the domain. Equally, when new devices are added to the system, an associated bundle is also typically offered. The presence of certain combinations of pebbles and bundles in a domain may trigger loading of further bundles: eg a fire alarm system might be automatically implemented whenever there both a smoke sensor and an alarm klaxon are present in the domain.
A bundle must be checked against all other rules already in the domain and if all rules hold, then the bundle joins and its rules start to take effect as well. A bundle may also be unloaded by deleting all of its rules at any time, provided it is not critical to ensuring a consistency rule that is not also unloaded at the same time.
A bundle might require parts of it to be loaded onto different execution platforms for efficiency, but the underlying tuplecore implementation means this is not strictly necessary, since all points of the tuplespace are nominally accessible from anywhere.
... operational model ...
A bundle of rules may be `re-hydrated' before being offered to the domain. This means expanding various hierarchic macros in the rules to produce flat Pushlogic Object code. The number of rules in a bundle may be increased or decreased during re-hydration. For instance, a complete bundle of standard rules may be copied out from a store where they are held in a `canned' form. Macro-generation is needed because Simple Pushlogic (SPL1) has no bindings, pointers, objects or dynamic storage allocation. The macro-generation ameliorates this by generating rules with static fields.1.2
Pushlogic rules may directly refer to fields with absolute path names (as part of a global tuple space), or to fields local to the current execution platform (generally the current device) or to the current domain of participation. In a general situation, this is not sufficient. Rules need to refer to locally bound devices, such as `front-door-bell'. Re-hydration provides such binding. It also provides guaranteed uniqueness for certain field names needed in applications that require the equivalent of `local variables'.
Research question: is it a good idea that the rules for rehydrating bundles to be implemented in the same language that is used within the bundles themselves? How do they need to differ and why? One clear distinction is that Pushlogic SPL1 is a finite-state language whereas dynamic rehydration changes the amount of state. This separation might be also most helpful in maintaining amenability to automated correctness checking.
