Formal Methods for Integrating Knowledge Bases

摘要

The object of this effort is to demonstrate the effectiveness of formal specification and refinement techniques for constructing realistic mediators. Such techniques will enable the rapid and reliable construction of mediators in fast-breading situations. This report describes the problem of mediation and an approach to solving this problem, that includes a formal specification and refinement process for mediator generation. SPECWARE is a formal software development tool that is extended with a mediator generation capability. This effort describes the process of translating specifications to code in Lisp or C++. The facility described is used both for describing wrappers and generating mediation code. Formal wrappers were built in SPECWARE. The theoretical notion of patching provides a systematic way of handling multiple representations of the same concept which is a basic problem in mediation. Patching, and its implementation in SPECWARE, are the major contributions of this project to mediation technology. This report also describes three demonstrations and summarizes the results, and outlines future work.