Code Reflection and Application Digests

Code Reflection: Announcing the behaviour of a controlling entity before it takes control. Application Digest: meta-information, pre-computed and stored with an application, that supports rapid checking for potential interactions with other applications or system standing constraints.

The Problem

Although there are many technologies for device registration, API reflection and automated service discovery, little emphasis has previously been given to the equivalent problem for control software. However control software is an essential part of any system and when there are multiple concurrent applications each may be regarded as a component in the system. The problem is that we do not know whether these applications will interfere with each other: both might wish to use some resource at once or issue conflicting commands to the same actuator.

The Solution

The solution is to bundle the high-level, proactive part of any software application as a separate component and to make it describe itself to the registration services. We call this `code reflection' meaning that the code itself, or a digest of it, is made available for other entities to examine and check. A software bundle may be prohibited from running, or taking control of certain output devices, until it has been checked for consistency against the rest of the system and the system's standing rules.

Original Pushlogic Framework

We developed this idea within the Pushlogic programming language and tool flow that generated its own bytecode for execution and feature interaction checking. Also, the Pushlogic tool chain used model checking of a complete domain of participation, but this did not scale and cannot be done in real time for systems of hundreds of state variables.

Current Work Plan

• explore systems of domain representation, including a DL ontology using the Protege serve (this was Dr Atif Alvi's doctoral dissertation),
• migrate the reflection to encompass IL machine language (.net byte code),
• develop compositional or incremental model checking where as much as possible is pre-computed before bundles have to be checked against each other,
• use an automated assume/guarantee reasoning system to combine smaller results generated by model checking,
• combine the various forms of digest into a common storage, signature and retrieval framework: CARDs proposal.

Although Pushlogic remains a useful high-level language in itself, its legacy is in its definition of functional profiles on the structure of autonomous controller and application code: for instance, whether the code supports reversible operation under error or conflict conditions and whether the code is amenable to model checking or conversion to Prolog, etc..

Note: cf Proof-Carrying Code

It is helpful to point out the differences between code reflection and proof-carrying code. Proof-carrying code is useful for understanding the behaviour of the given program with respect to well-known system constraints, such as memory footprint or termination. Our application digests contain information helpful for checking interactions with other applications and constraints not known at compile time.

(C) 2008 University of Cambridge. END.