The Domain Manager is an aggregation of services that
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.
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.
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 ...
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