Executable Formal Models in Rewriting Logic (Invited Talk)

Author Carolyn Talcott

Thumbnail PDF


  • Filesize: 200 kB
  • 1 pages

Document Identifiers

Author Details

Carolyn Talcott

Cite AsGet BibTex

Carolyn Talcott. Executable Formal Models in Rewriting Logic (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, p. 22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Formal executable models provide a means to gain insights into the behavior of complex distributed systems. Ideas can be prototyped and assurance gained by carrying out analyses at different levels of fidelity: searching for desirable or undesirable behaviors, determining effects of perturbing the system, and eventually investing effort to carry out formal proofs of key properties. This modeling approach applies to a wide range of systems, including a variety of protocols and networked cyber-physical systems. It is also emerging as an important tool in understanding many different aspects of biological systems. Rewriting logic (RWL) is a formalism that is well-suited to developing and working with formal executable models. In RWL term rewriting is used to represent both structure (equational properties and functions) and transformation / behavior. Logics and inference systems can be naturally represented in RWL, as can the structure and behavior of distributed systems both engineered and natural. Maude is a high performance realization of Rewriting Logic. Maude specifications are naturally executable and the Maude environment provides a variety analysis tools to reason about properties of models. These include reachability analysis, symbolic execution (narrowing), and model-checking. In addition, Maude is reflective. This provides a powerful mechanism for extension. The talk will present a sampling of executable specifications using Maude and its extensions.
  • Executable model
  • formal analysis
  • rewriting logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail