This paper summarizes an approach for testing reactive and concurrent Java programs which combines model checking and runtime monitoring. We use a model checker for two purposes. On the one hand, it analyzes multiple program executions by generating test input parameters. On the other hand, it checks each program execution against a linear temporal logic (LTL) property. The paper presents two methods to abstract the Java states that allow efficient testing of LTL. One of this methods supports the detection of cycles to test LTL on potentially infinite Java execution traces. Runtime monitoring is used to generate the Java execution traces to be considered as input of the model checker. Our current implementation in the tool TJT uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as a plug-in for Eclipse and it has been successfully applied to complex public Java programs.
Autores: Damián Adalid / Alberto Salmerón / María del Mar Gallardo / Pedro Merino /
Palabras Clave: Model checking - runtime monitoring - Testing
The need to increase mobility and remove cables in industrial environments is pushing 5G as a valuable communication system to connect traditional deterministic Ethernet baseddevices. One alternative is the adoption of Time Sensitive Networking (TSN) standards over 5G Non-Public Networks (5G NPN) deployed in the company premises. This scenario presents several challenges, the most relevant being the configuration of the 5G part to provide latency, reliability and throughput balance suitable to ensure that all the TSN traffic can be delivered on time. Our research work addresses this problem from the perspective of automata learning. Our aim is to learn from the live network to build a smart controller that can dynamically predict and apply a suitable configuration of the 5G NPN to satisfy the requirements of the current TSN traffic. The article presents the main ideas of this novel approach. This paper is published in IEEE Network, vol. 36, no. 2, pp. 50-56, March/April 2022, DOI: 10.1109/MNET.006.2100442.
Autores: Francisco Luque-Schempp / Laura Panizo / Maria-Del-Mar Gallardo / Pedro Merino / Javier Rivas /
Palabras Clave: 5G - automata learning - Time Sensitive Networking
Software Defined Network (SDN) is a new paradigm in networking that introduces great flexibility, allowing the dynamic configuration of parts of the network through centralised programming. SDN has been successfully applied in field networks, and is now being applied to wireless and mobile networks, generating Software Defined Mobile/Wireless networks (SDWNs). SDN can be also combined with Network Function Virtualization (NFV) producing a software network in which the specific hardware is replaced by general purpose computing equipment running SDN and NFV software solutions. This highly programmable and flexible network introduces many challenges from the point of view of reliability (or robustness), and operators need to ensure the same level of confidence as in previous, less flexible deployments. This paper provides a first study of the current tools used to analyse the reliability of SDNs before deployment and/or during the exploitation of the network. Most of these tools offer some kind of automatic verification, supported by algorithms based on formal methods, but they do not differentiate between fixed and mobile/wireless networks. In the paper we provide a number of classifications of the tools to make this selection easier for potential users, and we also identify promising research areas where more effort needs to be made.
Autores: Leticia Lavado / Laura Panizo / María del Mar Gallardo / Pedro Merino /
Palabras Clave: Communication Networks - Model checking - Reliability - Runtime - Software Defined Network - Verification
The behavior of mobile devices is highly non deterministic and barely predictable due to the interaction of the user with its applications. In consequence, analyzing the correctness of applications running on a smartphone involves dealing with the complexity of its environment. In this paper, we propose the use of model-based testing to describe the potential behaviors of users interacting with mobile applications. These behaviors are modeled by composing specially-designed state machines. These composed state machines can be exhaustively explored using a model checking tool to automatically generate all possible user interactions. Each generated trace model checker can be interpreted as a test case to drive a runtime analysis of actual applications. We have implemented a tool that follows the proposed methodology to analyze ANDROID devices using the model checker SPIN as the exhaustive generator of test cases.
Autores: Ana Rosario Espada / María del Mar Gallardo / Alberto Salmerón / Pedro Merino /