NSF-CNPq Collaborative Research: Mathematical and Engineering Foundations for Interoperability via Architecture

9900334 Mesguer，Jose GLarge软件系统日益复杂和昂贵。系统架构的良好文档可以极大地帮助系统的设计、开发和维护，也就是如何将其组织成有意义的子系统或组件，以及这些子系统如何粘合在一起形成整个系统。一个关键的悬而未决的问题是互操作性问题，即体系结构部分及其对应于不同视图的多个可能不同的语义描述如何结合在一起以形成一致的整体，以及这些不同的描述如何相互约束。这个协作项目的主要目标是：(1)开发数学基础，以便以一致和严格的数学方式集成和互操作基于对象的分布式系统的各种体系结构描述、形式规范和可执行原型，以及(2)基于这些基础，开发一种系统设计、开发和演化的方法，支持不同的正式和非正式系统描述的无缝集成，并明确系统的这些不同视图对彼此施加的约束。数学基础的发展将受到大量案例研究的推动，首先将深入研究各种符号和形式主义及其相互关系，这些符号和形式在描述不同层次的系统方面似乎特别有希望。重写逻辑将发挥重要作用，不仅作为一种可执行的规范形式主义，而且作为一种反思的元论框架，在其中所选择的形式主义及其关系可以被形式化。这些形式化可以使用用Maude语言开发的元工具来执行，Maude语言是重写逻辑的实现。预计这些基础和实验方法将推动软件开发和发展的最新水平，并将导致新的工具和方法，当适当使用时，将大大减少软件开发和维护的成本和工作量。

9900334 Meseguer, Jose GLarge software systems are increasingly complex and costly. The design, development, and maintenance of a system can be greatly helped by good documentation of its architecture, that is, of how it is structured into meaningful subsystems or components, and how those subsystems are glued together to form the overall system. A key unresolved problem is the interoperability problem, namely, how the architectural pieces and their multiple and possibly heterogeneous semantic descriptions corresponding to the different views fit together to make a coherent whole, and how these different descriptions impose constraints on each other. The main objectives of this collaborative project are (1) developing mathematical foundations for integrating and interoperating in a coherent and mathematically rigorous way diverse architectural descriptions, formal specifications, and executable prototypes of object-based distributed systems and (2) based on such foundations, developing a methodology for system design, development, and evolution that supports a seamless integration of the different formal and informal system descriptions and makes explicit the constraints that these different views of a system impose on each other. The development of mathematical foundations will be driven by substantial case studies and will begin with an in-depth study of a wide range of notations and formalisms and of their mutual relationships that seem particularly promising for describing systems at different levels. Rewriting logic will play an important role, not only as an executable specification formalism, but also as a reflective metalogical framework in which the chosen formalisms and their relations can be formalized. These formalizations can be executed using the meta tools developed in the Maude language, an implementation of rewriting logic. It is expected that these foundations and experimental methodology will advance the state of the art in software development and evolution, and will lead to new tools and methods that, when used properly, will substantially reduce the cost and effort of software development and maintenance.