TY - GEN
T1 - Programming Open Distributed Systems in Maude
AU - Durán, Francisco
AU - Eker, Steven
AU - Escobar, Santiago
AU - Martí-Oliet, Narciso
AU - Meseguer, José
AU - Rubio, Rubén
AU - Talcott, Carolyn
N1 - F. Dur\u00E1n has been partially supported by projects TED2021-130666BI00 and PID2021-125527NB-I00 funded by the Spanish government. S. Escobar has been partially supported by the grant PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe, by the grant CIPROM/2022/6 funded by Generalitat Valenciana, and by the grant number G6133 of theNATOScience for Peace and Security Programme. J. Meseguer and S. Escobar have been partially supported by INCIBE's Chair funded by the EU-NextGenerationEU through the Spanish government's Plan de Recuperaci\u00F3n, Transformaci\u00F3n y Resiliencia. N. Mart\u00ED and R. Rubio have been partially funded by the Spanish AEI through project ProCode (PID2019-108528RB-C22/AEI/10.13039/-501100011033).
PY - 2024/9/9
Y1 - 2024/9/9
N2 - Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.
AB - Maude is a high-performance logical framework based on rewriting logic and supporting formal specification, verification and declarative programming of concurrent systems. Since most concurrent open systems are made up of actor-like objects that communicate with each other through message passing, Maude provides special features to support their specification, verification and programming. Since open systems are heterogeneous, involving widely different kinds of objects such as sensors, actuators, devices, databases, graphical user interfaces, and so on, Maude supports declarative message-passing interaction between Maude objects and a wide variety of heterogeneous external objects. In this paper we explain and illustrate a methodology where an open system can first be designed and verified in Maude and then implemented as a distributed system of heterogeneous objects in a way that seamlessly bridges the gap between its formal specification and verification and its distributed implementation.
KW - Maude
KW - Open systems
KW - Rewriting logic
UR - http://www.scopus.com/inward/record.url?scp=85204918420&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85204918420&partnerID=8YFLogxK
U2 - 10.1145/3678232.3678237
DO - 10.1145/3678232.3678237
M3 - Conference contribution
AN - SCOPUS:85204918420
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Co-located with the 26th International Symposium on Formal Methods
PB - Association for Computing Machinery
T2 - 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, 26th International Symposium on Formal Methods and held in conjunction with LOPSTR 2024
Y2 - 10 September 2024 through 11 September 2024
ER -