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. Furthermore, by being directly based on rewriting logic, DCMaude will close the gap between formal specifications and actual implementations, making it possible to gain substantially higher assurance about the formal requirements, including the security properties, 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 will take joint responsibility for the DCMaude design. The DC Maude implementation will be the primary responsibility of SRI International, while the testing, benchmarking and development of DCMaude applications will be the primary responsibility of UIUC.
