Rosa Velardo, FernandoMarroquín Alonso, OlgaFrutos Escrig, David De2023-06-202023-06-202006Rosa Velardo, F., Marroquín Alonso, O. & Frutos Escrig, D. «Mobile Synchronizing Petri Nets: A Choreographic Approach for Coordination in Ubiquitous Systems». Electronic Notes in Theoretical Computer Science, vol. 150, n.o 1, marzo de 2006, pp. 103-26. DOI.org (Crossref), https://doi.org/10.1016/j.entcs.2005.12.026.1571066110.1016/j.entcs.2005.12.026https://hdl.handle.net/20.500.14352/52853The term Ubiquitous Computing was coined by Mark Weiser almost two decades ago. Despite all the time that has passed since Weiser’s vision, ubiquitous computing still has a long way ahead to become a pervasive reality. One of the reasons for this may be the lack of widely accepted formal models capable of capturing and analyzing the complexity of the new paradigm. We propose a simple Petri Net based model to study some of its main characteristics. We model both devices and software components as a special kind of coloured Petri Nets, located in locations, that can move to other locations and synchronize with other co-located nets, offering and requesting services. We obtain an amenable model for ubiquitous computing, due to its graphical representation. We present our proposal in a progressive way, first presenting a basic model where coordination is formalized by the synchronized firing of pairs of compatible transitions that offer and request a specific service, and ad hoc networks are modeled by constraining mobility by the dynamic acquisition of locality names. Next, we introduce a mechanism for the treatment of robust security properties, namely the generation of fresh private names, to be used for authentication properties.engAtribución-NoComercial-SinDerivadas 3.0 Españahttps://creativecommons.org/licenses/by-nc-nd/3.0/es/journal articlehttps://doi.org/10.1016/j.entcs.2005.12.026open access519.1MobilityPetri netsSecuritySpecificationsUbiquitous ComputingAnálisis combinatorio1202.05 Análisis Combinatorio