{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T17:21:09Z","timestamp":1740158469180,"version":"3.37.3"},"reference-count":31,"publisher":"Sociedade Brasileira de Computacao - SB","issue":"1","license":[{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T00:00:00Z","timestamp":1638316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["644178"],"award-info":[{"award-number":["644178"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Internet Serv Appl"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>With the emergence of the <jats:italic>Internet of Things<\/jats:italic> (IoT), application developers can rely on a variety of protocols and <jats:italic>Application Programming Interfaces<\/jats:italic> (APIs) to support data exchange between IoT devices. However, this may result in highly heterogeneous IoT interactions in terms of both functional and non-functional semantics. To map between heterogeneous functional semantics, middleware connectors can be utilized to interconnect IoT devices via bridging mechanisms. In this paper, we make use of the <jats:italic>Data eXchange<\/jats:italic> (DeX) connector model that enables interoperability among heterogeneous IoT devices. DeX interactions, including synchronous, asynchronous and streaming, rely on generic <jats:italic>post<\/jats:italic> and <jats:italic>get<\/jats:italic> primitives to represent IoT device behaviors with varying space\/time coupling. Nevertheless, non-functional <jats:italic>time semantics<\/jats:italic> of IoT interactions such as data availability\/validity, intermittent connectivity and application processing time, can severely affect response times and success rates of DeX interactions. We introduce timing parameters for time semantics to enhance the DeX API. The new DeX API enables the mapping of both functional and time semantics of DeX interactions. By precisely studying these timing parameters using timed automata models, we verify conditions for successful interactions with DeX connectors. Furthermore, we statistically analyze through simulations the effect of varying timing parameters to ensure higher probabilities of successful interactions. Simulation experiments are compared with experiments run on the <jats:italic>DeX Mediators<\/jats:italic> (DeXM) framework to evaluate the accuracy of the results. This work can provide application developers with precise design time information when setting these timing parameters in order to ensure accurate runtime behavior.<\/jats:p>","DOI":"10.1186\/s13174-021-00143-w","type":"journal-article","created":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T03:04:01Z","timestamp":1638327841000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Timed protocol analysis of interconnected mobile IoT devices"],"prefix":"10.5753","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0109-9527","authenticated-orcid":false,"given":"Georgios","family":"Bouloukakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaos","family":"Georgantas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ajay","family":"Kattepur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Valerie","family":"Issarny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3742","published-online":{"date-parts":[[2021,12,1]]},"reference":[{"issue":"3","key":"143_CR1","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1109\/TSC.2010.3","volume":"3","author":"D Guinard","year":"2010","unstructured":"Guinard D, Trifa V, Karnouskos S, Spiess P, Savio D. Interacting with the soa-based internet of things: Discovery, query, selection, and on-demand provisioning of web services. IEEE Trans Serv Comput. 2010; 3(3):223\u201335.","journal-title":"IEEE Trans Serv Comput"},{"key":"143_CR2","volume-title":"IEEE Global Communications Conference (GLOBECOM)","author":"K Fysarakis","year":"2016","unstructured":"Fysarakis K, Askoxylakis I, Soultatos O, Papaefstathiou I, Manifavas C, Katos V. Which iot protocol? comparing standardized approaches over a common m2m application. In: IEEE Global Communications Conference (GLOBECOM). Washington: IEEE: 2016."},{"key":"143_CR3","doi-asserted-by":"publisher","first-page":"1271","DOI":"10.1016\/j.future.2019.05.064","volume":"101","author":"G Bouloukakis","year":"2019","unstructured":"Bouloukakis G, Georgantas N, Ntumba P, Issarny V. Automated synthesis of mediators for middleware-layer protocol interoperability in the iot. Futur Gener Comput Syst. 2019; 101:1271\u201394. https:\/\/doi.org\/10.1016\/j.future.2019.05.064.","journal-title":"Futur Gener Comput Syst"},{"key":"143_CR4","volume-title":"ICSOC","author":"A Kattepur","year":"2015","unstructured":"Kattepur A, Georgantas N, Bouloukakis G, Issarny V. Analysis of timing constraints in heterogeneous middleware interactions. In: ICSOC. Goa: Springer: 2015."},{"issue":"2","key":"143_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill DL. A theory of timed automata. Theor Comput Sci. 1994; 126(2):183\u2013235.","journal-title":"Theor Comput Sci"},{"key":"143_CR6","unstructured":"Behrmann G, David A, Larsen KG. A tutorial on Uppaal 4.0: Department of computer science, Aalborg university; 2006."},{"key":"143_CR7","unstructured":"Schrank D, Eisele B, Lomax T. Tti\u2019s 2012 urban mobility report. 2012."},{"key":"143_CR8","unstructured":"ITS. Intelligent Transportation Systems. http:\/\/www.flir.co.uk\/traffic\/content\/?id=66601."},{"key":"143_CR9","unstructured":"XD. Traffic. http:\/\/inrix.com\/xd-traffic."},{"key":"143_CR10","volume-title":"ACM Mobisys","author":"J Yoon","year":"2007","unstructured":"Yoon J, Noble B, Liu M. Surface street traffic estimation. In: ACM Mobisys. PR: ACM: 2007."},{"key":"143_CR11","volume-title":"ACM SenSys","author":"P Mohan","year":"2008","unstructured":"Mohan P, Padmanabhan VN, Ramjee R. Nericell: rich monitoring of road and traffic conditions using mobile smartphones. In: ACM SenSys. Raleigh: ACM: 2008."},{"key":"143_CR12","doi-asserted-by":"crossref","unstructured":"Eugster P, Felber P, Guerraoui R, Kermarrec A. The many faces of publish\/subscribe. ACM Comput Surv (CSUR). 2003;114\u201331.","DOI":"10.1145\/857076.857078"},{"key":"143_CR13","volume-title":"OTM Confederated International Conferences\" On the Move to Meaningful Internet Systems\"","author":"L Aldred","year":"2005","unstructured":"Aldred L, van der Aalst W, Dumas M, ter Hofstede A. On the notion of coupling in communication middleware. In: OTM Confederated International Conferences\" On the Move to Meaningful Internet Systems\". Agia Napa: Springer: 2005."},{"key":"143_CR14","volume-title":"ESOCC","author":"N Georgantas","year":"2013","unstructured":"Georgantas N, Bouloukakis G, Beauche S, Issarny V. Service-oriented Distributed Applications in the Future Internet: The Case for Interaction Paradigm Interoperability. In: ESOCC. Managa: Springer: 2013."},{"key":"143_CR15","volume-title":"IEEE ICC","author":"G Bouloukakis","year":"2017","unstructured":"Bouloukakis G, Moscholios I, Georgantas N, Issarny V. Performance modeling of the middleware overlay infrastructure of mobile things. In: IEEE ICC. Paris: IEEE: 2017."},{"key":"143_CR16","volume-title":"ACM\/SPEC ICPE","author":"G Bouloukakis","year":"2017","unstructured":"Bouloukakis G, Georgantas N, Kattepur A, Issarny V. Timeliness Evaluation of Intermittent Mobile Connectivity over Pub\/Sub Systems. In: ACM\/SPEC ICPE. L Aquila: ACM: 2017."},{"key":"143_CR17","volume-title":"15th EAI International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous)","author":"G Bouloukakis","year":"2018","unstructured":"Bouloukakis G, Kattepur A, Georgantas N, Issarny V. Queueing network modeling patterns for reliable and unreliable publish\/subscribe protocols. In: 15th EAI International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous). New York: ACM: 2018."},{"issue":"2","key":"143_CR18","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke E, Emerson A, Sistla P. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst (TOPLAS). 1986; 8(2):244\u201363.","journal-title":"ACM Trans Program Lang Syst (TOPLAS)"},{"key":"143_CR19","doi-asserted-by":"crossref","unstructured":"Lee K, Lee J, Yi Y, Rhee I, Chong S. Mobile data offloading: how much can wifi deliver?. In: Proceedings of the 6th International COnference. ACM: 2010.","DOI":"10.1145\/1921168.1921203"},{"key":"143_CR20","unstructured":"Vernon M, Zahorjan J, Lazowska ED. A Comparison of Performance Petri Nets and Queueing Network Models: University of Wisconsin-Madison, Computer Sciences Department; 1986."},{"key":"143_CR21","volume-title":"IPDPS Workshops","author":"A Kattepur","year":"2015","unstructured":"Kattepur A, Nambiar M. Performance modeling of multi-tiered web applications with varying service demands. In: IPDPS Workshops. Hyderabad: IEEE: 2015."},{"key":"143_CR22","volume-title":"MMMECCS","author":"M Kwiatkowska","year":"2001","unstructured":"Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic symbolic model checker. In: MMMECCS. Aachen: Springer: 2001."},{"key":"143_CR23","volume-title":"VECoS","author":"A Nouri","year":"2016","unstructured":"Nouri A, Bozga M, Legay A, Bensalem S. Performance evaluation of complex systems using the sbip framework. In: VECoS. Montreal: Springer: 2016."},{"key":"143_CR24","doi-asserted-by":"crossref","unstructured":"Waszniowski L, Krakora J, Hanzalek Z. Case study on distributed and fault tolerant system modeling based on timed automata. J Syst Softw. 2009.","DOI":"10.1016\/j.jss.2009.04.042"},{"key":"143_CR25","doi-asserted-by":"crossref","unstructured":"Zhou Y, Ge J, Zhang P, Wu W. Model based verification of dynamically evolvable service oriented systems. Sci China Inf Sci. 2016.","DOI":"10.1007\/s11432-015-5332-8"},{"key":"143_CR26","volume-title":"FORTE","author":"F He","year":"2007","unstructured":"He F, Baresi L, Ghezzi C, Spoletini P. Formal analysis of publish-subscribe systems by probabilistic timed automata. In: FORTE. Tallinn: Springer: 2007."},{"key":"143_CR27","volume-title":"ICSE","author":"L Baresi","year":"2007","unstructured":"Baresi L, Ghezzi C, Mottola L. On accurate automatic verification of publish-subscribe architectures. In: ICSE. Minneapolis: IEEE Computer Society: 2007."},{"key":"143_CR28","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.adhoc.2015.05.013","volume":"36","author":"B Aziz","year":"2016","unstructured":"Aziz B. A formal model and analysis of an iot protocol. Ad Hoc Netw. 2016; 36:49\u201357.","journal-title":"Ad Hoc Netw"},{"key":"143_CR29","doi-asserted-by":"crossref","unstructured":"Basu A, Bensalem S, Bozga M, Caillaud B, Delahaye B, Legay A. Statistical abstraction and model-checking of large heterogeneous systems. 2010.","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"143_CR30","unstructured":"Kim M, Stehr MO, Talcott C, Dutt N, Venkatasubramanian N. Combining formal verification with observed system execution behavior to tune system parameters. Quebec: Springer: 2007."},{"key":"143_CR31","doi-asserted-by":"crossref","unstructured":"Kattepur A, Georgantas N, Issarny V. Qos analysis in heterogeneous choreography interactions. In: International Conference on Service-Oriented Computing. Springer: 2013.","DOI":"10.1007\/978-3-642-45005-1_3"}],"container-title":["Journal of Internet Services and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13174-021-00143-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1186\/s13174-021-00143-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1186\/s13174-021-00143-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,9]],"date-time":"2022-02-09T22:15:03Z","timestamp":1644444903000},"score":1,"resource":{"primary":{"URL":"https:\/\/jisajournal.springeropen.com\/articles\/10.1186\/s13174-021-00143-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["143"],"URL":"https:\/\/doi.org\/10.1186\/s13174-021-00143-w","relation":{},"ISSN":["1867-4828","1869-0238"],"issn-type":[{"type":"print","value":"1867-4828"},{"type":"electronic","value":"1869-0238"}],"subject":[],"published":{"date-parts":[[2021,12]]},"assertion":[{"value":"19 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 October 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 December 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"12"}}