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

点击翻译按钮获取中文摘要

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.