Rewriting logic is a powerful and general, yet simple and intuitive, logic for specifying dynamic systems, and is particularly suitable to specify distributed computer systems in an object-oriented style. In rewriting logic, data types are defined by equational specifications (which operationally can be seen as rich term rewrite systems), while dynamic behaviors are specified by (possibly conditional) rewrite rules.

Maude is a programming/modeling language and high-performance analysis tool for rewriting logic. Maude supports a range of analysis methods
for distributed systems formalized in rewriting logic, including: (a) simulation by rewriting; (b) reachability analysis by search; (c) various forms of temporal logic model checking; (d) symbolic analysis; and (e) various forms of theorem proving using associated tools. In addition, Maude models can also be subjected to statistical model checking using the umaudemc tool, so that Maude can analyze both the correctness and performance of distributed systems, with good predictive power.

Maude has been successfully applied to a wide range of sophisticated systems, including: large transport protocols, industrial cloud-based distributed
transaction systems, biological systems, human cognition, programming and modeling language semantics and analysis, cyber-physical systems, and so on.

Maude’s generality and intuitive formalism also extends to real-time and cyber-physical systems, so that rewriting logic and Maude complements popular, but much less expressive, formalisms such as timed/hybrid automata and time(d) Petri nets, with the ability to formalize wide ranges of large real-time systems, as well as to provide formal semantics and analysis features to industrial modeling languages.  

This tutorial gives an introduction to specification and analysis in Maude for first distributed systems and then to real-time systems. It also provides a sample of applications of Maude to such systems.