Hidden Algebra and Modular Distributed Concurrent Software

隐代数和模块化分布式并发软件

• 批准号: 9901002
• 负责人: joseph goguen
• 金额: $ 23.12万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-15 至 2002-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9901002&HistoricalAwards=false
• 关键词: Hidden; Algebra; Modular; Distributed; Concurrent

9901002 Goguen, Joseph A University of CaliforniaHidden Algebra and Modular Distributed Concurrent SoftwareTools, theory, case studies, and methods are being developed for hidden algebra, a new approach to specifying, prototyping, verifying, documenting and generating distributed concurrent software. Tools build on the Kumo proof assistant and website generator, by providing a new specification language, taking advantage of new web technology (XML, dynamic HTML, JavaCC, etc.), and using multiple inference engines, including the new CafeOBJ system. Hidden algebra extends the algebraic approach to abstract data types (ADTs) initiated by the PI, by encompassing state, behavioral abstraction, nondeterminism, concurrency, and first order sentences; like the algebraic theory of ADTs, it works well with modularization. More powerful proof principles are being developed, as well as better methods for documenting proofs. Long term goals are to develop tools, methods and theory for high quality software systems, and to advance our understanding of modular distributed concurrent systems. Semantics is important as a model for designing software tools, and providing correctness criteria for important relations like refinement, while experimentation is essential for ensuring that the approach can handle realistic problems and meet real needs.

9901002 Goguen，Joseph A 隐藏代数和模块化分布式并发软件的工具，理论，案例研究和方法正在开发的隐藏代数，一种新的方法来指定，原型，验证，文档化和生成分布式并发软件。 工具建立在Kumo证明助手和网站生成器的基础上，通过提供新的规范语言，利用新的Web技术（XML，动态HTML，JavaCC等），并使用多个推理引擎，包括新的CafeOBJ系统。 隐藏代数将代数方法扩展到PI发起的抽象数据类型（ADT），涵盖状态、行为抽象、非确定性、并发性和一阶句子;与ADT的代数理论一样，它与模块化配合得很好。 正在开发更强大的证明原则，以及更好的证明方法。 长期目标是开发高质量软件系统的工具，方法和理论，并提高我们对模块化分布式并发系统的理解。 语义作为设计软件工具的模型是很重要的，并为重要的关系提供正确性标准，如细化，而实验是必不可少的，以确保该方法可以处理现实的问题，并满足真实的需求。