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

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

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 .