TC: Medium: Collaborative Research: Rewriting Logic Foundations for Verification and Programming of Next-Generation Trustworthy Web-Based Systems

TC：媒介：协作研究：重写下一代可信赖网络系统验证和编程的逻辑基础

• 批准号: 0905607
• 负责人: Carolyn Talcott
• 金额: $ 29.99万
• 依托单位: SRI International
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-10-01 至 2014-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0905607&HistoricalAwards=false
• 关键词: TC; Medium; Collaborative; Research; Rewriting

Distributed Concurrent Maude ( DCMaude ) The rewriting model of computation is simple , yet general and flexible . A system of any kind , for example , an algorithm , a database , a hardware system , a programming language , a network protocol , a sensor network , or the molecular biology dynamics of a cell , can be modeled by a set of rewrite rules that describe the systems behavior . The rewriting model of computation is intrinsically concurrent , without any need for explicit concurrency constructs . Any set of rules that apply to nonoverlapping system components can execute concurrently . For a large distributed system such as a network or a cell , this means that at any given time thousands or millions of concurrent transitions may be happening in parallel . Maude is a language based on rewriting logic . The current Maude implementation provides a high performance rewrite engine , as well as builtin search , unification , and model checking tools to support execution and analysis of systems specified in Maude . To realize inherent concurrency of rewriting , the proposed project will develop an implementation of Maude called Distributed and Concurrent Maude ( DCMaude ) that will exploit the concurrency available in multicore/multiprocessor machines , and support distributed computing and systems programming . The rewriting semantics of Maude supports seamless transition between concurrent and distributed execution of a system : execution in one process , multiple processes/cores , or multiple machines . In addition to built in strategies for concurrency , the design of DCMaude will include a means for the programmer to control concurrency at a high level of abstraction in a declarative way . DC Maude will provide new methods and tools that can significantly improve both the design and the implementation of open distributed systems , including web-based systems and next-generation networks .

分布式并发Maude(DCMaude)计算的重写模型简单，但通用且灵活。任何类型的系统，例如算法、数据库、硬件系统、编程语言、网络协议、传感器网络或细胞的分子生物学动力学，都可以由描述系统行为的一组重写规则来建模。计算的重写模型本质上是并发的，不需要任何显式的并发构造。适用于非重叠系统构件的任何规则集都可以并发执行。对于大型分布式系统，如网络或蜂窝，这意味着在任何给定时间，数千或数百万个并发转换可能并行发生。莫德语是一种基于重写逻辑的语言。当前的Maude实现提供了高性能的重写引擎，以及内置的搜索、统一和模型检查工具，以支持Maude中指定的系统的执行和分析。为了实现固有的并发性重写，拟议的项目将开发一个称为分布式和并发Maude(DCMaude)的Maude实现，它将利用多核/多处理器机器中的并发性，并支持分布式计算和系统编程。Maude的重写语义支持系统的并发执行和分布式执行之间的无缝转换：在一个进程、多个进程/核心或多台机器中执行。除了内置的并发策略外，DCMaude的设计还将包括一种让程序员以声明性方式在高抽象级别控制并发的方法。DC Maude将提供新的方法和工具，可以显著改进开放式分布式系统的设计和实施，包括基于网络的系统和下一代网络。