2026-05-27T05:35:35Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/263662026-02-03T11:24:00Zcom_10630_2254col_10630_37953

00925njm 22002777a 4500 dc Panizo-Jaime, Laura author Gallardo-Melgarejo, María del Mar author 2022-11-30 The increasing integration of systems into people’s 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 STAn, which performs runtime verification on data traces that combine timestamped discrete events and sampled real-valued magnitudes. STAn uses the Spin model checker as the underlying execution engine, and analyzes traces against properties described in the so-called event-driven interval temporal logic (eLTL) by transforming each eLTL formula into a network of concurrent automata, written in Promela, that monitors the trace. We present two different transformations for online and offline monitoring, respectively. Then, Spin 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. Panizo, L., & Gallardo, M. D. M. (2023). STAn: analysis of data traces using an event-driven interval temporal logic. Automated Software Engineering, 30(1), 1-47. https://hdl.handle.net/10630/26366 10.1007/s10515-022-00367-5 Informática - Aplicaciones Teléfono Teledetección Soporte lógico - Verificación STAN: analysis of data traces using an event-driven interval temporal logic