{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T18:02:04Z","timestamp":1762624924481,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T00:00:00Z","timestamp":1669766400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T00:00:00Z","timestamp":1669766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014440","name":"ministerio de ciencia, innovaci\u00f3n y universidades","doi-asserted-by":"publisher","award":["RTI2018-099777-B-I00"],"award-info":[{"award-number":["RTI2018-099777-B-I00"]}],"id":[{"id":"10.13039\/100014440","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100010198","name":"Ministerio de Asuntos Econ\u00f3micos y Transformaci\u00f3n Digital","doi-asserted-by":"crossref","award":["TSI-063000-2021-11"],"award-info":[{"award-number":["TSI-063000-2021-11"]}],"id":[{"id":"10.13039\/501100010198","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["101016521","101016608"],"award-info":[{"award-number":["101016521","101016608"]}],"id":[{"id":"10.13039\/100010661","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2023,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The increasing integration of systems into people\u2019s daily routines, especially smartphones, requires ensuring correctness of their functionality and even some performance requirements. Sometimes, we can only observe the interaction of the system (e.g. the smartphone) with its environment at certain time points; that is, we only have access to the data traces produced due to this interaction. This paper presents the tool<jats:sc>STAn<\/jats:sc>, which performs runtime verification on data traces that combine timestamped discrete events and sampled real-valued magnitudes.<jats:sc>STAn<\/jats:sc>uses the<jats:sc>Spin<\/jats:sc>model checker as the underlying execution engine, and analyzes traces against properties described in the so-called event-driven interval temporal logic () by transforming each formula into a network of concurrent automata, written in<jats:sc>Promela<\/jats:sc>, that monitors the trace. We present two different transformations for online and offline monitoring, respectively. Then,<jats:sc>Spin<\/jats:sc>explores the state space of the automata network and the trace to return a verdict about the corresponding property. We use the proposal to analyze data traces obtained during mobile application testing in different network scenarios.<\/jats:p>","DOI":"10.1007\/s10515-022-00367-5","type":"journal-article","created":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T10:05:15Z","timestamp":1669802715000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["STAn: analysis of data traces using an event-driven interval temporal logic"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6399-6162","authenticated-orcid":false,"given":"Laura","family":"Panizo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3481-5307","authenticated-orcid":false,"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,30]]},"reference":[{"issue":"11","key":"367_CR1","doi-asserted-by":"publisher","first-page":"832","DOI":"10.1145\/182.358434","volume":"26","author":"J Allen","year":"1983","unstructured":"Allen, J.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832\u2013843 (1983)","journal-title":"Commun. ACM"},{"issue":"1","key":"367_CR2","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35\u201377 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1025","journal-title":"Inf. Comput."},{"key":"367_CR3","doi-asserted-by":"publisher","unstructured":"Awad, A., Tommasini, R., Kamel M.and Della\u00a0Valle, E., S., S.: D2IA: stream analytics on user-defined event intervals. In: Advanced Information Systems Engineering. CAiSE 2019, LNCS, vol. 11483 (2019). https:\/\/doi.org\/10.1007\/978-3-030-21290-2_22","DOI":"10.1007\/978-3-030-21290-2_22"},{"key":"367_CR4","doi-asserted-by":"publisher","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: B. Steffen, G. Levi (eds.) 5th Int. Conf. on Verification, Model Checking, and Abstract Interpretation,VMCAI 2004, LNCS, vol. 2937, pp. 44\u201357. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_5","DOI":"10.1007\/978-3-540-24622-0_5"},{"issue":"11","key":"367_CR5","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.H.: Formal analysis of log files. J. Aerosp. Comput. Inf. Commun. 7(11), 365\u2013390 (2010). https:\/\/doi.org\/10.2514\/1.49356","journal-title":"J. Aerosp. Comput. Inf. Commun."},{"issue":"3","key":"367_CR6","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from eagle to ruler. J. Log. Comput. 20(3), 675\u2013706 (2010). https:\/\/doi.org\/10.1093\/logcom\/exn076","journal-title":"J. Log. Comput."},{"issue":"2","key":"367_CR7","doi-asserted-by":"publisher","first-page":"15:1","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1-15:45 (2015). https:\/\/doi.org\/10.1145\/2699444","journal-title":"J. ACM"},{"issue":"9","key":"367_CR8","doi-asserted-by":"publisher","first-page":"8136","DOI":"10.1016\/j.eswa.2012.01.153","volume":"39","author":"JA Botia","year":"2012","unstructured":"Botia, J.A., Villa, A., Palma, J.: Ambient assisted living system for in-home monitoring of healthy independent elders. Expert Syst. Appl. 39(9), 8136\u20138148 (2012)","journal-title":"Expert Syst. Appl."},{"key":"367_CR9","doi-asserted-by":"crossref","unstructured":"Cameron, F., Fainekos, G., Maahs, D., Sankaranarayanan, S.: Towards a verified artificial pancreas: challenges and solutions for runtime verification, LNCS, vol. 9333, pp. 3\u201317. Springer Verlag, Cham (2015)","DOI":"10.1007\/978-3-319-23820-3_1"},{"key":"367_CR10","doi-asserted-by":"crossref","unstructured":"Chaochen, Z., Hansen, M.R.: Duration calculus\u2014a formal approach to real-time systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer (2004)","DOI":"10.1007\/978-3-662-06784-0"},{"key":"367_CR11","doi-asserted-by":"publisher","unstructured":"Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: Tessla: Temporal stream-based specification language. In: T.\u00a0Massoni, M.R. Mousavi (eds.) 21st Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2018, LNCS, vol. 11254, pp. 144\u2013162. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03044-5_10","DOI":"10.1007\/978-3-030-03044-5_10"},{"key":"367_CR12","doi-asserted-by":"publisher","DOI":"10.3390\/s20226652","author":"A D\u00edaz Zayas","year":"2020","unstructured":"D\u00edaz Zayas, A., Caso, G., Alay, O., Merino, P., Brunstrom, A., Tsolkas, D., Koumaras, H.: A modular experimentation methodology for 5G deployments: the 5GENESIS approach. Sensors (2020). https:\/\/doi.org\/10.3390\/s20226652","journal-title":"Sensors"},{"key":"367_CR13","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: N.\u00a0Sharygina, H.\u00a0Veith (eds.) 25th International Conference on Computer Aided Verification (CAV 2013), LNCS, vol. 8044, pp. 264\u2013279. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"367_CR14","doi-asserted-by":"crossref","unstructured":"D\u2019Souza, D., Matteplackel, R.M.: A compositional hierarchical monitoring automaton construction for LTL. In: A.\u00a0Roychoudhury, M.\u00a0D\u2019Souza (eds.) 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), LNCS, vol. 7521, pp. 16\u201329. Springer (2012)","DOI":"10.1007\/978-3-642-32943-2_2"},{"issue":"4\u20135","key":"367_CR15","doi-asserted-by":"crossref","first-page":"e1699","DOI":"10.1002\/stvr.1699","volume":"29","author":"AR Espada","year":"2019","unstructured":"Espada, A.R., Gallardo, M.M., Salmer\u00f3n, A., Panizo, L., Merino, P.: A formal approach to automatically analyze extra-functional properties in mobile applications. Softw. Test. Verif. Reliab. 29(4\u20135), e1699 (2019)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"367_CR16","doi-asserted-by":"publisher","first-page":"150369","DOI":"10.1109\/ACCESS.2019.2947361","volume":"7","author":"CV Espinosa","year":"2019","unstructured":"Espinosa, C.V., Martin-Martin, E., Riesco, A., Rodr\u00edguez-Hortal\u00e1, J.: FlinkCheck:property-based testing for apache flink. IEEE Access 7, 150369\u2013150382 (2019)","journal-title":"IEEE Access"},{"key":"367_CR17","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Schledjewski, M., Schwenger, M., Stenger, M., Tentrup, L., Torfah, H.: StreamLAB: Stream-based monitoring of cyber-physical systems. In: I.\u00a0Dillig, S.\u00a0Tasiran (eds.) 31st International Conference on Computer Aided Verification CAV 2019, LNCS, vol. 11561, pp. 421\u2013431. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_24","DOI":"10.1007\/978-3-030-25540-4_24"},{"issue":"6","key":"367_CR18","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1002\/stvr.1505","volume":"24","author":"MM Gallardo","year":"2014","unstructured":"Gallardo, M.M., Panizo, L.: Extending model checkers for hybrid system verification: the case study of SPIN. Softw. Test. Verif. Reliab. 24(6), 438\u2013471 (2014). https:\/\/doi.org\/10.1002\/stvr.1505","journal-title":"Softw. Test. Verif. Reliab."},{"key":"367_CR19","doi-asserted-by":"publisher","unstructured":"Gallardo, M.M., Panizo, L.: Trace analysis using an event-driven interval temporal logic. In: M.\u00a0Gabbrielli (ed.) 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), LNCS, vol. 12042, pp. 177\u2013192. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-45260-5_11","DOI":"10.1007\/978-3-030-45260-5_11"},{"key":"367_CR20","doi-asserted-by":"publisher","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: Nested monitors: Monitors as expressions to build monitors. In: L.\u00a0Feng, D.\u00a0Fisman (eds.) 21st Int. Conference on Runtime Verification, RV 2021, LNCS, vol. 12974, pp. 164\u2013183. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_9","DOI":"10.1007\/978-3-030-88494-9_9"},{"key":"367_CR21","doi-asserted-by":"publisher","unstructured":"Hall\u00e9, S.: When RV meets CEP. In: Y.\u00a0Falcone, C.\u00a0S\u00e1nchez (eds.) 16th International Conference on Runtime Verification, RV 2016, LNCS, vol. 10012, pp. 68\u201391. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_6","DOI":"10.1007\/978-3-319-46982-9_6"},{"key":"367_CR22","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D.: First-order timed runtime verification using BDDs. In: D.V. Hung, O.\u00a0Sokolsky (eds.) 18th International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), LNCS, vol. 12302, pp. 3\u201324. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_1","DOI":"10.1007\/978-3-030-59152-6_1"},{"issue":"1","key":"367_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-018-00327-4","volume":"56","author":"K Havelund","year":"2020","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 56(1), 1\u201321 (2020). https:\/\/doi.org\/10.1007\/s10703-018-00327-4","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"367_CR24","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using java pathfinder. STTT 2(4), 366\u2013381 (2000)","journal-title":"STTT"},{"issue":"5","key":"367_CR25","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"367_CR26","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"367_CR27","doi-asserted-by":"crossref","unstructured":"Kauffman, S., Havelund, K., Joshi, R.: nfer\u2013a notation and system for inferring event stream abstractions. In: International Conference on Runtime Verification (RV\u201916), LNCS, vol. 10012, pp. 235\u2013250. Springer (2016)","DOI":"10.1007\/978-3-319-46982-9_15"},{"key":"367_CR28","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/s10703-018-0317-z","volume":"53","author":"S Kauffman","year":"2018","unstructured":"Kauffman, S., Havelund, K., Joshi, R., Fischmeister, S.: Inferring event stream abstractions. Formal Methods Syst. Des. 53, 54\u201382 (2018)","journal-title":"Formal Methods Syst. Des."},{"issue":"2\u20133","key":"367_CR29","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.tcs.2004.09.023","volume":"331","author":"Y Kesten","year":"2005","unstructured":"Kesten, Y., Pnueli, A.: A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2\u20133), 397\u2013428 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2004.09.023","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"367_CR30","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247\u2013268 (2013)","journal-title":"STTT"},{"issue":"2","key":"367_CR31","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10009-019-00518-2","volume":"22","author":"L Panizo","year":"2020","unstructured":"Panizo, L., Diaz-Zayas, A., Garcia, B.: Model-based testing of apps in real network scenarios. Int. J. Softw. Tools Technol. Transf. 22(2), 105\u2013114 (2020). https:\/\/doi.org\/10.1007\/s10009-019-00518-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"367_CR32","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: J.\u00a0Misra, T.\u00a0Nipkow, E.\u00a0Sekerinski (eds.) 14th International Symposium on Formal Methods (FM 2006), LNCS, vol. 4085, pp. 573\u2013586. Springer (2006). https:\/\/doi.org\/10.1007\/11813040_38","DOI":"10.1007\/11813040_38"},{"key":"367_CR33","doi-asserted-by":"publisher","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: E.\u00a0\u00c1brah\u00e1m, K.\u00a0Havelund (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2014), LNCS, vol. 8413, pp. 357\u2013372. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24","DOI":"10.1007\/978-3-642-54862-8_24"},{"issue":"2","key":"367_CR34","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Rosu","year":"2005","unstructured":"Rosu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151\u2013197 (2005). https:\/\/doi.org\/10.1007\/s10515-005-6205-y","journal-title":"Autom. Softw. Eng."},{"issue":"1","key":"367_CR35","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/s10703-019-00343-y","volume":"55","author":"C S\u00e1nchez","year":"2019","unstructured":"S\u00e1nchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstic, S., Louren\u00e7o, J.M., Nickovic, D., Pace, G.J., Rufino, J., Signoles, J., Traytel, D., Weiss, A.: Correction to: a survey of challenges for runtime verification from advanced application domains (beyond software). Formal Methods Syst. Des. 55(1), 72 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00343-y","journal-title":"Formal Methods Syst. Des."},{"key":"367_CR36","doi-asserted-by":"publisher","unstructured":"Volanschi, N., Serpette, B.P.: AllenRV: An extensible monitor for multiple complex specifications with high reactivity. In: B.\u00a0Finkbeiner, L.\u00a0Mariani (eds.) 19th International Conference on Runtime Verification, RV 2019, LNCS, vol. 11757, pp. 393\u2013401. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_24","DOI":"10.1007\/978-3-030-32079-9_24"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-022-00367-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-022-00367-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-022-00367-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,2]],"date-time":"2023-12-02T06:09:59Z","timestamp":1701497399000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-022-00367-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,30]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,5]]}},"alternative-id":["367"],"URL":"https:\/\/doi.org\/10.1007\/s10515-022-00367-5","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2022,11,30]]},"assertion":[{"value":"26 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 October 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 November 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"3"}}