Home : Current Projects : EPOXI
 

EPOXI: Evolutionary Programming Over eXplicit Interfaces

Principal Investigators: Dr Dusko Pavlovic & Dr Douglas Smith

Sponsor: DARPA ISO/DASADA

Objective

The EPOXI project is about guaranteeing that complex software systems operate correctly through assured composition and evolution of software modules.

• Assured composition: in a complex software system, many modules must interact in an intricate manner. The modules may have been developed by different companies at different stages of the system's deployment. How can a system engineer know that the modules will work together correctly? APIs based on conventional technologies provide only signature information (i.e., what functions are available and what parameters they take). This is not enough to ensure module compatibility.
• System evolution: a complex software system may be in use for decades. Parts of the system may be upgraded. How can a system engineer know that upgrading a module will not cause the system to fail? Conventional APIs do not provide enough information.

Approach: Especs

The core of EPOXI's approach to composition and evolution is a technology called Especs (Evolving Specifications). Especs capture the essential information about the structure and behavior of modules:

• The structural specification of a module captures the logical functionality of a module (what the module achieves) using algebraic specifications and categorical diagrams.
• The behavioral specification of a module captures the operational method a module uses to achieve its functionality. One suitable formalism is coalgebraic transition systems.

A prime example of the need to capture both structure and behavior is a communication protocol: the structural specification talks about messages, authentication, encryption, etc., while the behavioral specification talks about the steps required to establish a secured channel, asyncrhonous vs. synchronous transmission, acknowledgements, etc.

If two modules are to interact via such a protocol, they must know what the protocol guarantees and what steps they must take to use the protocol. Similarly, if a system engineer is to directly replace one protocol with another, he must know that the replacement provides at least as much functionality using the same sequence of operational steps.

Glue Code and Evolution

However, the EPOXI project aims to go beyond just specifying structure and behavior: EPOXI aims to leverage these entirely formal specifications to enhance the flexibility of modules and complex software systems.

• If two modules are essentially compatible, but their implementations do not fit together perfectly, then glue code can, perhaps, be synthesized from the modules' especs: for example, the synthesized glue code may translate from the particular data representation used by one module to the representation used by the other.
• Similarly, a new version of a module is likely to differ in small ways from the version it is replacing: the functionality may have been enhanced or realized in a different manner. Glue code can be synthesized to ensure that when a module in a system is upgraded, the other (unchanged) modules interact correctly with the new version.

Performance Gauges

The final thread in EPOXI's approach is the synthesis of run-time performance gauges. Because especs address both the functionality of a module and the method for achieving that functionality, they can address how well the functionality is actually delivered at run-time. Gauges can be synthesized from suitable especs to monitor run-time performance and possibly trigger corrective action if the performance is too poor. (Corrective action might, for example, include replacing the module with an alternative that uses a different implementation method, one better suited to the particular run-time data encountered by the module.)

Current Research Themes

The EPOXI project is invesitigating the basic foundation of especs, compact and convenient formalisms for representing especs, and effective technology for exploiting especs.

• Especs are based on a coupling of algebraic and coalgebraic specifications: the algebraic captures the structure while the coalgebraic captures the behavior.
• The structure and behavior are related to each other through formal gauges.
• The representation of especs is based on category-theoretic hereditary diagrams, and on abstract state machines.
• The technology for composing modules is based on category-theoretic colimit operations.
• Glue code synthesis and evolution are based on formal refinement technologies, in the form of categoty-theoretic morphisms and interpretations.

Benefits

• True modularity: especs provide the essential information necessary to allow complex systems to be developed as modules by independent teams of programmers.
• Cost-effective evolution: modules will be upgraded while system functionality will be maintained. The costs of evolution, stemming from software inventories and quality assurance, will be slashed.

Papers

• D. Pavlovic, Towards semantics of self-adaptive software. In: "Self-Adaptive Software: First International Workshop", 17-19 April 2000, Oxford, England, pp 50-64, Paul Robertson, Howie Shrobe, Robert Laddaga (Eds.), Spinger 2000, LNCS vol. 1936, pp 50-65
• D. Pavlovic and D.R. Smith, System Construction via Evolving Specifications, in Complex and Dynamic Systems Architectures (CDSA 2001), Brisbane, Australia, 2001
• D. Pavlovic and D.R. Smith, Guarded Transitions in Evolving Specifications, in Proceedings of 9th International Conference on Algebraic Methodology And Software Technology (AMAST 2002), Eds. H. Kirchner and C. Ringeissen, Springer-Verlag LNCS, September 9-13, 2002, St. Gilles les Bains, Reunion Island, France.
• Matthias Anlauff, D. Pavlovic and D.R. Smith, Composition and Refinement of Evolving Specifications, invited paper to appear in Proceedings of Workshop on Evolutionary Formal Software Development, July 2002, Copenhagen, Denmark.

Presentations (powerpoint)

• Gauges for Specification-Carrying Software
• EPOXI: towards Specification Carrying Software
• EPOXI: Evolutionary Programmiong Over eXplicit Interfaces

- Back to Top -

- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -