The most recent technology in the evolution of mobile networks is 5G, which is aimed at offering differentiated quality of service (QoS) to specific groups of users or devices. Such groups could include public safety agencies, connected vehicles, citizens streaming video content, fixed Internet of Things devices, etc. Insofar as each group has different requirements in terms of bandwidth, latency, error rate, coverage or other relevant quality indicators, the network can be divided into multiple slices , with each slice supporting a group's requirements. Such network slicing is becoming a key feature for telecom operators, who need to face the challenge of validating its correct behavior. In this paper, we propose a monitoring system to check that a 5G network is offering slicing in the proper way. To this end, we use the tool STAn , a general purpose runtime verification tool where the requirements to be monitored are expressed using temporal formulae. The paper identifies first a list of requirements that define the expected behavior of network slicing. Then, we describe how the initial logic eLTL supported by STAn is extended to the so-called eXtended Event-driven Temporal Logic ( xeLTL ) in order to represent the slicing requirements. Finally, we validate that the new version of STAn and the catalogue of xeLTL formulae are suitable to monitor and check if real 5G networks properly support slicing. This way, we provide a complete new system for runtime monitoring of 5G network slicing.

Abstract 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 toolSTAn, which performs runtime verification on data traces that combine timestamped discrete events and sampled real-valued magnitudes.STAnuses theSpinmodel 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 inPromela, that monitors the trace. We present two different transformations for online and offline monitoring, respectively. Then,Spinexplores 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.

This paper presents a proposal for dynamic spectrum management concept from a pan-European research operator perspective. Dynamic spectrum management is one of the key enablers for the 5G and beyond communications systems. Regulatory concepts for sharing the spectrum have been developed, and they have been adopted for implementation in the standardization. The prevailing methods are currently Licensed Shared Access (LSA) in the European Union (EU) and Citizens Broadband Radio Service (CBRS) in the United States (US). In the EU, however, the final decisions of the spectrum usage are done by the national regulatory authorities, and therefore it is seen that harmonized spectrum usage is not going to happen at European level in the near future. In this paper, we describe the approach taken in EuWireless to gain access to the spectrum resources dynamically for the research use. In the proposal, the information about the spectrum resources across the Europe are stored the central Spectrum Repository (SR). The local instances of EuW Spectrum Manager (SM), operating under the licences and regulations in different areas, handle the communication with the MNOs via standardized procedures such as LSA or CBRS.

Summary This paper presents an integrated approach for testing mobile applications (apps) against a set of extra‐functional properties to be used by app developers. The approach starts with the (manual or automatic) extraction of the interaction model, that is, a formal model of the potential user interactions with the app. The model is constructed to allow a model checking tool to exhaustively extract the so‐called app user flows, that is, the sequences of user actions, that constitute the test cases. In the final step, the app user flows are executed on the app running on real devices. The resulting execution traces are enriched with different measures and verified against a set of extra‐functional properties of interest. The approach has been adapted to analyse several applications running at the same time with several devices supporting the applications. This paper presents the definition and formalization of both the modelling language for the interaction model and the specification language to represent the extra‐functional properties. It also describes a methodology for automatically extracting the model. Finally, it presents an implementation focused on Android apps, which is integrated in the TRIANGLE testing framework, and the evaluation of the approach. © 2019 The Authors. Software Testing, Verification & Reliability Published by John Wiley & Sons Ltd.

This paper presents the TRIANGLE testbed approach to score the Quality of Experience (QoE) of mobile applications, based on measurements extracted from tests performed on an end‐to‐end network testbed. The TRIANGLE project approach is a methodology flexible enough to generalize the computation of the QoE for any mobile application. The process produces a final TRIANGLE mark, a quality score, which could eventually be used to certify applications.

The evolution of mobile networks and the increasing number of scenarios for mobile applications requires new approaches to ensure their quality and performance. The TRIANGLE project aims to develop an integrated testing framework that allows the evaluation of applications and devices in different network scenarios. This paper focuses on the generation of user interactions that will be part of the test cases for applications. We propose a method that combines model-based testing and guided search, based on the Key Performance Indicators to be measured, and we have evaluated our proposal with an example. Our ultimate goal is to integrate the guided generation of user flows into the TRIANGLE testing framework to automatically generate and execute test cases.

SUMMARY A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Because of this combination of discrete and continuous dynamics, the behaviour of a hybrid system is, in general, difficult to model and analyse. Model checking techniques have been proven to be an excellent approach to analyse critical properties of complex systems. This paper presents a new methodology to extend explicit model checkers for hybrid systems analysis. The explicit model checker is integrated, in a non‐intrusive way, with some external structures and existing abstraction libraries, which store and manipulate the abstraction of the continuous behaviour irrespective of the underlying model checker. The methodology is applied to SPIN using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers. Copyright © 2013 John Wiley & Sons, Ltd.

Abstract Program synthesis with automated methods has been an active research area for many years; however, we still lack well‐known and accepted techniques for this software engineering task. In this case, the design space to be considered is infinite, even when the solution is restricted to software that meets the requirements. In this paper we propose the use of model checking (MC) techniques to automatically synthesize controllers. Given a goal in the evolution of a plant, MC can be used to search for acceptable software controllers that enable the plant to evolve as desired. We also develop a realistic application in the context of a joint project with a major water reservoir management company. This application generates controllers for dam management during flood seasons. The controllers give the proper orders (open or close the outflow elements) at precise times in order to avoid disasters and to preserve the water level in the dam. Copyright © 2011 John Wiley & Sons, Ltd.

In this paper, we study the adequacy of applying peer-to- peer techniques to mobile networks by conducting a series of experiments using smart phones as peers. We measure important parameters, such as jitter and packet losses, in static and dynamic scenarios, focusing on a video streaming service. Finally, based on the results obtained, we discuss the feasibility of these applications.

In this paper, we focus on analyzing video streaming service performance on real networks. We propose a non intrusive methodology based on mobile devices as clients, instead of using them as modems. Our objective is to provide a more realistic test environment using actual mobile devices in real conditions of network load and radio propagation while taking into account the intrinsic mobility of mobile subscribers. This solution allows us to follow the end to end performance even when handover between different access technologies is performed. Using this methodology we carry out a study of video streaming behavior over GPRS and UMTS networks. Outstanding results related with delays, jitter, lost packets and sequence errors have been obtained. Also other conclusions about video quality, such as PSNR, have been achieved. Moreover, we analyze the impact of mobility issues such as handover or cell reselection.