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.

The distributed and disaggregated nature of 5G and beyond (B5G) networks has spurred interest in federated learning (FL) for empowering privacy-preserving collaborative network anomaly detection at the edge. However, FL is prone to catastrophic forgetting (CF), where prior knowledge is forgotten while sequentially learning new attack patterns from a stream of data. Few studies addressed CF issue in network anomaly detection using Continual Learning (CL), but focusing on centralized models rather than FL and overlooking integration in B5G. To fill this gap, we propose TenaxDoS, a novel framework that combines FL with a replay memory-based CL strategy to foster sustainable and cooperative network anomaly detection in an Open Radio Access Network (O-RAN) environment in B5G networks. The experimental results on a dataset from a real 5G test network show TenaxDoS's superior overall performance, stability and effective mitigation of CF, yielding a remembering of past knowledge of above 98.8%.

Tactile Internet refers to a network that enables real-time, high-reliability haptic communication and control between humans, machines, and objects over the Internet. Tactile Internet applications include the remote control of drones, cars or industrial tele-operation. In this context, the Multi-connection Tactile Internet Protocol (MTIP) is a novel multipath transport protocol designed to support the requirements of Tactile Internet applications in large, private mobile networks. The objective of this paper is to analyze and verify the correctness and performance of the MTIP protocol to ensure that the protocol functions correctly under different network scenarios and it is ready to meet the performance requirements of Tactile Internet applications. For that purpose, a two-step approach is employed to analyze and verify MTIP. In the first step, a formal model of MTIP is developed using timed automata and the uppaal tool is utilized to verify correctness properties represented as temporal formulas. In the second step, the performance of the protocol is analyzed using the statistical model checking features of uppaal (uppaal smc) in scenarios that are difficult and expensive to reproduce in a real network. The results indicate that MTIP’s model meets the specified temporal properties, and the performance evaluation showcases the potential and trade-off of using multiple paths to enhance the communication. Based on the analysis and verification results, the paper emphasizes the readiness of MTIP for real-world deployment and highlights its potential benefits for enhancing the performance of Tactile Internet applications.

Tactile Internet defines applications for remotely controlling and manipulating critical devices that require perceived real-time operation with additional demanding requirements like reliability. These use cases with stringent requirements demand adequate transport protocols to take advantage of the underlying possibilities. Traditional transport-layer solutions like TCP and UDP are no longer sufficient, hence novel protocols are being developed to support these applications. In this paper, we present an implementation and evaluation of the Multi-connection Tactile Internet Protocol (MTIP), a transport layer proposal to support these communications. MTIP uses application and network status information to perform an intelligent selection of paths in order to improve reliability and latency. In our evaluations, we study how the different configurations of the MTIP algorithm affect this selection and we see a direct trade-off where, with more restrictive thresholds, MTIP can increase the packets received correctly at the cost of sending extra duplicate packets.

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 describes PerformNetworks, which is an enhanced test and research facility for cutting edge mobile communications managed by the MORSE group in the University of Malaga. This facility is an evolution, containing key improvements introduced on top of the work presented in NOMS 2012 [1]. The test environment has been extended to support new features available in LTE-Advanced networks, power consumption measurements and channel emulation in uplink. The PerformNetworks testbed is a reference research platform that has been used in multiple experiments.

Voice services has been for a very long time the primary source of income for mobile network operators. Even with the increasing importance of the data traffic, voice services will keep playing a key role and will not disappear with the transition to a networking model based on the IP protocol. Moreover, the key industry players diagnosed years ago that mobile subscribers wouldn't accept a significant degradation in the quality of their voice services. Because of that, it becomes critical to ensure the Quality of Experience (QoE) in the transition to new generation networks based on packet switching communications. The work in the present thesis has aimed to analyze the behavior and the dependencies in the different voice services over IP (VoIP), as well as to identify optimal configurations, potential enhancements and methodologies to ensure acceptable quality levels while minimizing the costs.

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.

In this paper we address the support of wearable mHealth applications in LTE and future 5G networks following a holistic approach that spans across the elements of a mobile network. The communication requirements change from one application to another so we propose a measurement methodology to facilitate the selection of the user equipment to fulfil these requirements. We also discuss a new network architecture to support traffic prioritization, RAN programmability, low latency and group communications to over-the-top applications. Our proposal is validated using several realistic experimentation platforms and the results show that mHealth systems can benefit from our approach.

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs.

Railway transportation uses specific technologies such as GSM-R for traffic signaling purposes, but commercial networks could also provide added value services to passengers and transport companies such as CCTV or telemetry. Furthermore mobile users increasingly want to be always connected even when they are traveling. Although current deployed technologies such as 3G provide wide coverage in general, when it comes to high mobility scenarios such as the railway, further analysis is required to ensure appropriate user experience. In this paper we propose a methodology to collect and to organize traffic information related to the behavior of Internet services over commercial mobile networks (UMTS and HSDPA). We apply our method to conduct an extensive study on a high speed train line in the south of Spain. The measurement campaigns comprised hundreds of VoIP sessions, comparing different network providers over more than 155 kilometers. We conclude that the characterization method is useful to provide information for railway operators (for instance, to migrate from GSM-R to LTE), telecom operators (to fit their network deployments) and for mobile software developers (to adapt their applications to the high speed environment).

This demonstration shows a methodology to collect and analyze key performance indicators (KPI) directly from real devices running commercial mobile applications. The main objective of this methodology is to provide a complete multi-layer understanding of the performance of mobile applications and services from the user level, to the radio access through all the stack protocols.

The proliferation of mobile Internet services for smartphones makes it more necessary than ever to use measurement tools in mobile devices to monitor their connectivity performance. In this paper we introduce TestelDroid, a software tool for Android devices which provides advanced monitoring functionalities for analyzing multimedia services and applications specifically designed for smartphones. The beneficiaries of this tool are mobile operators, service providers and mobile developers, as TestelDroid offers a unified and independent methodology to analyze performance parameters from the application level, taking into account underlying issues.

This application track paper describes an experimental test setup composed to verify the communication performance of internet applications over LTE (Long Term Evolution) networks.

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.

Abstract Software model checking consists in applying the most powerful results in formal verification research to programming languages such as C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, such as SPIN. This paper focusses on the application of this approach to the avionics software constructed on top of the Application Executive Software (APEX) Interface, which is widely employed by manufacturers in the avionics industry. It presents a method to automatically extract PROMELA models from the C source code. In order to close the extracted model during verification, we built a reusable APEX‐specific environment. This APEX environment models the execution engine (i.e. an APEX compliant real‐time operating system) that implements APEX services. In particular, it explains how to deal with aspects such as real‐time and APEX scheduling. Time is modelled in such a way that the we save time and memory by avoiding the analysis of irrelevant steps. This model of time and the construction of a deterministic scheduler guarantees the scalability of our approach. The paper also presents a tool that can verify realistic applications, and that has been used as a novel testing method to ensure the correctness of our APEX environment. This testing method uses SPIN to execute official APEX test cases. Copyright © 2010 John Wiley & Sons, Ltd.

In this paper we present a study of the performance of handovers for live GPRS, UMTS and HSDPA networks from the point of view of data traffic. Specifically, our analysis focuses on an evaluation of the impact of handover at IP level during data connections (packet losses, jitter and outage duration). The results provided in this paper have been obtained from extensive field tests carried out on European commercial mobile networks.

Software model checking technology is based on an exhaustiveand efficient simulation of all possible execution paths in concurrent programs. Existing tools based on this method can rapidly detect execution errors, preventing malfunctions in the final system. However dealing with dynamic memory allocation is still an open trend. In this paper, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The method consists in defining a canonical representation of the heap that is based on moving most of the information from the state vector to a global structure. We give a formal semantics of the method in order to show its soundness. Our experimental results show that this method can be efficiently implemented in many well known model checkers, like CADP or SPIN.

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.

Traditionally, protocol engineers have to deal with the design and implementation of complex network services, spending considerable time and effort on creating robust and reliable final source code. Although approaches exist to assist engineers in the development of communication protocols which use several object-oriented frameworks, these do not benefit from new modelling guidelines developed in MDE and UML to exploit automatic code generation from graphical models. This paper introduces a new UML2 profile for communications which guides the construction of software for communications following the client-server architecture. The MDE process is then used to design suitable platform-specific models for the well-known Adaptive Communications Environment (ACE), a high performance C++ toolkit for implementing concurrent and network applications which relies heavily on architectural patterns

A current trend in the software engineering community is to integrate different tools in a friendly and powerful development environment for use by final users. This is also the case for tools based on formal methods, which are very valuable for increasing confidence in the reliability of software. This paper contributes to one promising approach to make this integration possible, the project FMICS-jETI. This project aims to obtain an active repository of tools based on formal methods in such a way that users can access and combine all the tools simply by defining a graph with the tools and the files they manage. In particular, the paper explains how two new modules of the well known toolset CADP are added to FMICS-jETI. These new modules, named C.Open and Annotator extend Cadp with functions to manage C programs in this toolset.

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.

SDL and other related ITU-T formal languages have been revealed as a valid approach to developing software for critical systems, such as telecommunication equipment. In this context, this paper presents the use of SDL to implement one of the most complex part of UMTS networks, the radio resource control protocol (RRC). SDL has been used at all the steps of the design and the implementation process, making use of the automatic code generation capabilities of well-known SDL tools. The resulting system will be integrated as a part of a conformance testing box for 3G mobile phones, namely MINT, a product developed by one of the certification leaders in the industry, CETECOM S.A. The main conclusion obtained from this project is that SDL (together with ASN.l) has good capabilities to design and implement realistic complex systems with a very limited use of external languages, like C. During the development, we have been able to take advantages of its formal basis and tool support for simulation and verification.

The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due to the presence of complex data structures. One recent and promising approach to deal with this problem is the construction of an abstract and correct representation of the global program state allowing to match visited states during program model exploration. In particular, one powerful method to implementabstractmatchingis to fill the state vector with a minimal amount of relevant variables for each program point. In this paper, we combine the on-the-fly model checking approach (incremental construction of the program state space) and the static analysis method called influence analysis (extraction of significant variables for each program point) in order to automatically construct an abstract matching function. Firstly, we describe the problem as an alternation-free value-based mu-calculus formula, whose validity can be checked on the program model expressed as a labeled transition system (LTS). Secondly, we translate the analysis into the local resolution of a parameterised Boolean equation system (PBES), whose representation enables a more efficient construction of the resulting abstract matching function. Finally, we show how our proposal has been elegantly integrated into CADP, a generic framework for both the design and analysis of distributed systems and the development of verification tools.

The application of model checking technology to real software seems to be a promising and realistic approach to increase its quality. There are some successful examples of tools for this purpose, mainly working with self-contained programs. However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend.In this paper, we give a method for using the tool SPIN to verify distributed software systems that use the API Socket and the network protocol stack TCPIP for communications. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker. We define and use a formal semantics of the API to conduct the correct construction of models. The whole modelling process is transparent to the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we ensure that the system only reports potential (non-spurious) errors.

Abstract. Semantics of description languages for complex systems are a central issue for implementing verification methods such as abstract model checking . This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool αspin as an extension of spin.

Taking maximum advantage of dynamic reconfiguration in the implementation of digital systems poses a number of challenging research problems. Specifically, techniques are needed to partition the system behavioral description into segments of computation (or "scheduling units"), and to define a reconfiguration schedule with respect to those units, so as to maximize the performance of the dynamically reconfigurable system, subject to the area constraints of the FPGA. We propose a methodology to: (1) perform a coarse-grained partitioning of the system behavioral description into a set of tasks, (2) determine which sub-set of tasks is to remain resident in the FPGA, and which sub-set is to be non resident, (3) generate a reconfiguration schedule for the non-resident tasks by specifying when such tasks should be loaded on to and erased from the FPGA.