Synthesizing Adaptable Components for COTS Runtime Environments

Objective

The objective of the project is to extend and use the Specware system to formally specify components for the Jini environment, and to automatically synthesize Java code from these specifications. Extensions to the Jini environment will be formally specified and synthesized supporting placement of mobile agents, enhanced security checking, enhanced scheduling and resource allocation, as well as resource monitoring. A specification will be composed of separate formalizations of properties (or aspects) of components. Code will be synthesized from the combination of these formalizations. This work will help enable DoD mission critical applications to utilize the new paradigm of network-centric computing.

Approach

Consider an application that analyzes sensor data. Network-centric computing environments such as Jini enable dynamic introduction of sensors as new services that are registered and made available to other components. These environments simplify the programming required to interact with such sensors by hiding details of the underlying communication mechanisms used by the network. But significant issues remain about insuring that sensors are not hostile, that sensor data is analyzed at a processor that optimizes the required communication, and that data collection tasks are allocated to sensors in an optimal fashion. This project will produce components that analyze code for conformance interface specifications, and provide scheduling and resource monitoring services that insure that services are allocated optimally and are utilized according to expectations.

The extended Jini components will be formally specified and synthesized using the Specware system, developed at Kestrel Institute. Specware specifications are written in a functional high-order logic and refined to code using a correct-by-construction refinement methodology. Existing Specware specifications and refinements for resource scheduling will contribute to this project. Furthermore Kestrel has previously formalized and synthesized a substantial part of the Java bytecode verifier.

However, to specify the new components, existing Jini components that they utilize or interact with must be wrapped with Specware specifications. Furthermore some components of the JVM, for example the bytecode verifier, may be enhanced with new functionality. Thus, the project will formalize aspects of existing Jini components including the Java Virtual Machine (JVM), Java class loading, remote method invocation (RMI), and the leasing model.

To specify these components Specware will be extended so that the specification and synthesis of aspects such as objects, states, events, concurrency, leasing and code/data distribution are directly supported. The work on aspect-oriented programming is relevant, but fundamental study is necessary to relate aspect-oriented concepts to specification and synthesis within Specware.

The project will develop extensions to Jini in three areas.

The first is support for placement of mobile agents and migrating objects. Services within a Jini system must be allocated among the available processing elements. Components that place services on processing elements close to data sources or sinks and so reduce network traffic will be developed. Mobile agents will depend on the JVM and RMI components in the Jini system.

The second extension is support for enhanced security. Code mobility introduces unique security threats and so users may require more security checking than what a Jini system provides. The enhanced security checks include conformance checks that are performed on incoming mobile code. Simple analysis techniques include signature checking, type correctness, and straightforward checking of resource usage. More complex techniques include determining whether interprocedural contracts are obeyed, whether code adheres to certain protocols, etc. Security checking will interact with JVM and Java dynamic loading. Kestrel’s synthesized bytecode verifier can be naturally extended to richer checking on mobile agents.

The third extension is support for enhanced scheduling and allocation of services. Components that statically or dynamically analyze and monitor the usage of services, and evaluate their progress and performance will be synthesized. Jini’s capacity to schedule services is based on a leasing model: a request to use a service carries a start and expiration time; the allocation of a service to a request terminates after the expiration time. The enhancements will enable Jini to optimize service usage by dynamically re-scheduling and re-allocating services. An unsatisfiable service request may then become satisfiable. Kestrel’s previous work on scheduling will be applied here.