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

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

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

The rewriting model of computation is simple, yet general and flexible. A system of any kind, for example, an algorithm, a database, a hardwaresystem, a programming language, a network protocol, a sensor network, orthe molecular biology dynamics of a cell, can be modeled by a set ofrewrite rules thatdescribe the systems behavior. The rewriting model of computation isintrinsically 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 networkor a cell, this means that at any given time thousands or millions ofconcurrent 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 wellas builtin search, unification, and model checking tools to supportexecution and analysis of systems specified in Maude. To realizeinherent concurrency of rewriting, the proposed project will develop animplementation of Maude called Distributed andConcurrent Maude (DCMaude) that will exploit the concurrency available in multicore/multiprocessor machines, and support distributed computingand systems programming. The rewriting semantics of Maude supportsseamless transition between concurrent and distributed execution of asystem: execution in one process, multiple processes/cores, or multiplemachines. In addition to built in strategies for concurrency, the designof DCMaude will include a means for the programmer to controlconcurrency 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 distributedsystems, including web-based systems and next-generation networks.Furthermore, by being directly based on rewriting logic, DCMaudewill close the gap between formal specifications and actualimplementations, making it possible to gain substantially higherassurance about the formal requirements, including the securityproperties, of such systems.The project will be carried our jointly by Drs. Jose Meseguer (UIUC)and Dr. Carolyn Talcott (SRI International). Both UIUC and SRI willtake joint responsibility for the DCMaude design. The DC Maudeimplementation will be the primary responsibility of SRI International,while the testing, benchmarking and development of DCMaude applicationswill be the primary responsibility of UIUC.

计算重写模型简单，但具有通用性和灵活性。任何类型的系统，例如算法、数据库、硬件系统、编程语言、网络协议、传感器网络或细胞的分子生物学动力学，都可以通过一组描述系统行为的重写规则来建模。计算的重写模型本质上是并发的，不需要显式的并发构造。应用于非重叠系统组件的任何规则集都可以并发执行。对于大型分布式系统（如网络或单元），这意味着在任何给定时间，可能有数千或数百万个并发转换并行发生。Maude是一种基于重写逻辑的语言。当前的Maude实现提供了一个高性能的重写引擎，以及内置的搜索、统一和模型检查工具，以支持Maude中指定的系统的执行和分析。为了实现重写的固有并发性，提议的项目将开发一种称为分布式和并发Maude （DCMaude）的Maude实现，该实现将利用多核/多处理器机器中的并发性，并支持分布式计算和系统编程。Maude的重写语义支持系统在并发和分布式执行之间的无缝转换：在一个进程、多个进程/核心或多台机器中执行。除了内置的并发策略外，DCMaude的设计还将包括一种方法，使程序员能够以声明的方式在高层次的抽象上控制并发性。DC Maude将提供新的方法和工具，可以显著改善开放式分布式系统的设计和实现，包括基于web的系统和下一代网络。此外，通过直接基于重写逻辑，dcmaude将缩小正式规范和实际实现之间的差距，使其有可能获得关于此类系统的正式需求（包括安全属性）的实质上更高的保证。该项目将由dr。Jose Meseguer （UIUC）和Carolyn Talcott博士（SRI International）。UIUC和SRI将共同负责DCMaude的设计。DC maude的实施将是SRI国际的主要责任，而dmaude应用程序的测试、基准测试和开发将是UIUC的主要责任。