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

9900334 Meseguer，Jose GLarge软件系统越来越复杂和昂贵。 一个系统的设计、开发和维护可以通过其体系结构的良好文档得到很大的帮助，也就是说，它是如何被构造成有意义的子系统或组件的，以及这些子系统是如何粘合在一起形成整个系统的。 一个关键的未解决的问题是互操作性的问题，即，如何架构件和他们的多个和可能异构的语义描述对应于不同的视图适合在一起，使一个连贯的整体，以及这些不同的描述如何施加约束对方。 这个合作项目的主要目标是：（1）开发数学基础，以便以一种连贯和数学上严格的方式集成和互操作基于对象的分布式系统的各种体系结构描述、正式规范和可执行原型;（2）基于这些基础，开发系统设计、开发、和演化，支持不同的正式和非正式系统描述的无缝集成，并明确这些不同的系统视图相互施加的约束。 数学基础的发展将由大量的案例研究驱动，并将开始与广泛的符号和形式主义及其相互关系，似乎特别有希望在不同层次上描述系统的深入研究。 重写逻辑将发挥重要作用，不仅作为一个可执行的规格说明形式主义，而且作为一个反射元逻辑框架，在其中所选择的形式主义和它们的关系可以形式化。 这些形式化可以使用在Maude语言中开发的Meta工具来执行，这是重写逻辑的一种实现。 预计这些基础和实验方法将推动软件开发和发展的最新水平，并将导致新的工具和方法，如果使用得当，将大大减少软件开发和维护的成本和努力。

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.