{"id":1742,"date":"2026-06-14T21:01:07","date_gmt":"2026-06-14T21:01:07","guid":{"rendered":"https:\/\/synasc.ro\/2026\/?page_id=1742"},"modified":"2026-06-14T22:00:05","modified_gmt":"2026-06-14T22:00:05","slug":"formal-modeling-and-analysis-of-distributed-and-real-time-systems-in-maude","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2026\/tutorials\/formal-modeling-and-analysis-of-distributed-and-real-time-systems-in-maude\/","title":{"rendered":"Formal Modeling and Analysis of Distributed and Real-Time Systems in Maude"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"1742\" class=\"elementor elementor-1742\" data-elementor-post-type=\"page\">\n\t\t\t\t<div class=\"elementor-element elementor-element-3e0b8ee e-con-full e-flex e-con e-parent\" data-id=\"3e0b8ee\" data-element_type=\"container\">\n\t\t\t\t<div class=\"elementor-element elementor-element-a3ba736 elementor-widget elementor-widget-heading\" data-id=\"a3ba736\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Formal Modeling and Analysis of Distributed and Real-Time Systems in Maude<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-80ba9f5 elementor-widget elementor-widget-heading\" data-id=\"80ba9f5\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Peter Csaba \u00d6lveczky<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-7088b6b elementor-widget elementor-widget-text-editor\" data-id=\"7088b6b\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Department of Informatics, University of Oslo, Norway<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6af37d1 elementor-widget elementor-widget-image\" data-id=\"6af37d1\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img fetchpriority=\"high\" decoding=\"async\" width=\"212\" height=\"300\" src=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/csaba22ab-212x300.jpg\" class=\"attachment-medium size-medium wp-image-1723\" alt=\"\" srcset=\"https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/csaba22ab-212x300.jpg 212w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/csaba22ab-725x1024.jpg 725w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/csaba22ab-768x1085.jpg 768w, https:\/\/synasc.ro\/2026\/wp-content\/uploads\/sites\/28\/2026\/06\/csaba22ab.jpg 936w\" sizes=\"(max-width: 212px) 100vw, 212px\" \/>\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-6e257af elementor-align-center elementor-hidden-widescreen elementor-hidden-desktop elementor-hidden-tablet elementor-hidden-mobile elementor-icon-list--layout-traditional elementor-list-item-link-full_width elementor-widget elementor-widget-icon-list\" data-id=\"6e257af\" data-element_type=\"widget\" data-widget_type=\"icon-list.default\">\n\t\t\t\t\t\t\t<ul class=\"elementor-icon-list-items\">\n\t\t\t\t\t\t\t<li class=\"elementor-icon-list-item\">\n\t\t\t\t\t\t\t\t\t\t\t<a href=\"#\">\n\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-icon\">\n\t\t\t\t\t\t\t<svg aria-hidden=\"true\" class=\"e-font-icon-svg e-fas-globe\" viewBox=\"0 0 496 512\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\"><path d=\"M336.5 160C322 70.7 287.8 8 248 8s-74 62.7-88.5 152h177zM152 256c0 22.2 1.2 43.5 3.3 64h185.3c2.1-20.5 3.3-41.8 3.3-64s-1.2-43.5-3.3-64H155.3c-2.1 20.5-3.3 41.8-3.3 64zm324.7-96c-28.6-67.9-86.5-120.4-158-141.6 24.4 33.8 41.2 84.7 50 141.6h108zM177.2 18.4C105.8 39.6 47.8 92.1 19.3 160h108c8.7-56.9 25.5-107.8 49.9-141.6zM487.4 192H372.7c2.1 21 3.3 42.5 3.3 64s-1.2 43-3.3 64h114.6c5.5-20.5 8.6-41.8 8.6-64s-3.1-43.5-8.5-64zM120 256c0-21.5 1.2-43 3.3-64H8.6C3.2 212.5 0 233.8 0 256s3.2 43.5 8.6 64h114.6c-2-21-3.2-42.5-3.2-64zm39.5 96c14.5 89.3 48.7 152 88.5 152s74-62.7 88.5-152h-177zm159.3 141.6c71.4-21.2 129.4-73.7 158-141.6h-108c-8.8 56.9-25.6 107.8-50 141.6zM19.3 352c28.6 67.9 86.5 120.4 158 141.6-24.4-33.8-41.2-84.7-50-141.6h-108z\"><\/path><\/svg>\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-text\">Webpage<\/span>\n\t\t\t\t\t\t\t\t\t\t\t<\/a>\n\t\t\t\t\t\t\t\t\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-89d48db elementor-widget elementor-widget-heading\" data-id=\"89d48db\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">ABSTRACT<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-dd1252a elementor-widget elementor-widget-text-editor\" data-id=\"dd1252a\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>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.<br \/><br \/>Maude is a programming\/modeling language and high-performance analysis tool for rewriting logic. Maude supports a range of analysis methods<br \/>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.<br \/><br \/>Maude has been successfully applied to a wide range of sophisticated systems, including: large transport protocols, industrial cloud-based distributed<br \/>transaction systems, biological systems, human cognition, programming and modeling language semantics and analysis, cyber-physical systems, and so on.<br \/><br \/>Maude&#8217;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. \u00a0<br \/><br \/>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.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-8c706e9 elementor-widget elementor-widget-heading\" data-id=\"8c706e9\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">SHORT BIO<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-0b87dae elementor-widget elementor-widget-text-editor\" data-id=\"0b87dae\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p><strong>Peter Csaba \u00d6lveczky<\/strong> has been a full professor at the Department of Informatics, University of Oslo, since 2008. Before that, he was an assistant professor from 2001 and then associate professor at the same place from 2004.<\/p><p><strong>\u00d6lveczky<\/strong> received his Dr.Scient. degree from the University of Bergen in 2000, having performed his doctoral research at SRI International. He was a post-doctoral researcher at the University of Illinois at Urbana-Champaign (UIUC) 2002-2004, and was a part-time visiting researcher at UIUC 2005-2016.<\/p><p><strong>\u00d6lveczky<\/strong> is head of the bachelor and master study programs in &#8220;Programming and System Architecture&#8221; at the University of Oslo. He has chaired 18 international scientific conferences\/workshops\/symposia, has written a textbook &#8220;Designing Reliable Distributed Systems&#8221;, and is a member of the steering committees of FACS and WRLA. \u00d6lveczky has given tutorials at the International School on Rewriting in 2018, 2019, and 2022, and well as at a number of other venues.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Formal Modeling and Analysis of Distributed and Real-Time Systems in Maude Peter Csaba \u00d6lveczky Department of Informatics, University of Oslo, Norway Webpage ABSTRACT 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, [&hellip;]<\/p>\n","protected":false},"author":30,"featured_media":0,"parent":140,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1742","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1742","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/users\/30"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/comments?post=1742"}],"version-history":[{"count":7,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1742\/revisions"}],"predecessor-version":[{"id":1764,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/1742\/revisions\/1764"}],"up":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/pages\/140"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2026\/wp-json\/wp\/v2\/media?parent=1742"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}