2026-08-10T23:24:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5186 2024-03-06T10:36:01Z ddc:004 open_access

Executable Formal Models in Rewriting Logic (Invited Talk) Talcott, Carolyn Executable model formal analysis rewriting logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Carolyn Talcott 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.22 urn:nbn:de:0030-drops-51861 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.22 eng https://creativecommons.org/licenses/by/3.0/legalcode