SPL1 Pushlogic is a scripting language for a dynamic population of devices (e.g. sensors, processors or actuators) and dynamic number of concurrent applications in a reliable or safety critical system. It is a constrained language, fully amenable to automated reasoning at various granularites. It defines re-hydration for dynamic binding of rules to new device instances and a load-time model checker that runs before a new bundle of rules may join a domain of participation. In a typical application of Pushlogic, complex embedded devices are partitioned into passive components known as `Pebbles'. API registration and reflection are then used to expose the interfaces offered by the Pebbles. All proactive and interactive behaviour between Pebbles or over the network must then be implemented with Pushlogic and `code reflection', as we call it, exposes this behaviour for automated reasoning. This report gives the syntax and semantics SPL1 Pushlogic. This work was carried out under the CMI Goals/Pebbles project [1].
This document is currently under preparation and is being changed every month or so...