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.

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.

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.

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.

Abstract The timed concurrent constraint language (tccp) is a timed extension of the concurrent constraint paradigm.tccpwas defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined. On the basis of that semantic framework, this paper proposes an abstract semantics that, together with a widening operator, is suitable for the definition of different analyses fortccpprograms. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical (abstract) computational step of the program. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation.

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.

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.

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.

The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are barely supported by verification techniques because among other reasons, it is difficult to efficiently manage the pointer-based internal representation. This is a key aspect when the goal is to construct a verification tool based on model checking techniques, for instance. In addition, since new nodes may be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, it being difficult to detect errors such as, for instance, the non desirable sharing between two nodes. In this paper, we propose to use mu-calculus to describe and analyze, using model checking techniques, dynamic data such as lists, and non-linear data structures like trees. The expressiveness of mu-calculus makes it possible to naturally describe these structures. In addition, following the ideas of separation logic, the logic has been extended with a new operator able to describe the non-sharing property which is essential when analyzing data structures of this type.

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.

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.

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.