Domain Manager

The Domain Manager is an aggregation of services that

• delimit the domain boundary,
• manage domain name spaces, including network addresses and device names,
• allow new devices, bundles and pebbles to join the domain,
• fetch canned bundles in respsonse to trigger actions, re-hydrate them and attempt to insert them into the domain,
• allocate interpreted bundles to execution platforms,
• provide compute resources for soft pebbles,
• provide model checking over all rules in the domain to ensure all properties are satisfied, and
• support removal of devices, bundles and pebbles when no longed wanted.

The Domain Manager provides a few standard pebbles, used by Pushlogic in read-only mode, that provide domain status information.

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.

Using the compiler to check domains

It is planned that a number of compiled bundles can be read in during a compilation and the bundles being compiled are checked against them. Indeed, no source-level bundles are provided, the compiler will act as a static checker for a collection of object bundles. This has been implemented but no examples written up.

Incremental and Real-time Model Checking

We wish to design an object bundle file format that is as amenable as possible to rapid incremental model checking or assume/guarantee-style automated reasoning.

Real-time Model Checking ... is one of our main challenges being explored ...

Federation of Pushlogic DoPs

Pushlogic rules hold within a domain of participation (DoP). The DoP may cover multiple execution platforms, but all rules are shared in terms of consistency checking.^8.1