El autor Laura Panizo ha publicado 10 artículo(s):

Hybrid systems are characterized by combining discrete and continuous behaviors. Verification of hybrid systems is, in general, a difficult task due to the potential complexity of the continuous dynamics. Currently, there are different formalisms and tools which are able to analyze specific types of hybrid systems, model checking being one of the most used approaches. In this paper, we propose an extension of the discrete model checker Java Path Finder in order to analyze hybrid systems. We apply a general methodology which has been successfully used to extend SPIN. This methodology is non-intrusive, and uses external libraries, such as Parma Polyhedra Library, to abstract the continuous behavior of the hybrid system independent to the underlying model checker.

Autores: Laura Panizo / María-del-Mar Gallardo / 
Palabras Clave: Hybrid systems - JPF - Model checking

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

Alloy is both a modelling and specifying language of software systems, and a tool to automatically check the consistency of descriptions. Alloy uses sets and set relations to describe the high-level structure of systems, and a first-order relational logic to enrich models with more specific properties. A similar methodology is followed by software engineers when using OCL to complete the UML descriptions with more detailed features that improve the specifications. Alloy is able to construct and analyze the consistency of static specifications of complex systems, producing snapshots of possible model instances. In addition,Alloy can also describe dynamic specifications that show how the system may evolve over time when executing transitions. In this tutorial, we present the main features of the language and illustrate them by means of an example consisting in the specification and modelling of Software-Defined Networks. The example is sufficiently complex to permit the use of the most significant Alloy constructors.

Autores: María-Del-Mar Gallardo / Laura Panizo / 
Palabras Clave: Modelling language Alloy - SAT solvers - Software defined networks

Traditional testing methods for mobile apps focus on detecting execution errors. However, the evolution of mobile networks towards 5G will require additional support for app developers to ensure also the performance and user-experience. Manual testing in a number of scenarios is not enough to satisfy the expectations of the apps final users. This paper presents the testing framework developed in the TRIANGLE project1 that integrates a complete mobile network testbed and a model-based testing approach, which is based on model checking, to automatically evaluate the apps performance in different network scenarios.

Autores: Laura Panizo / Almudena Díaz / Bruno García / 
Palabras Clave: mobile network testbed - Model checking - model-based testing

The Timed Concurrent Constraint Language tccp is a declarative synchronous concurrent language, particularly suitable for modelling reactive systems. In tccp, agents communicate and synchronise through a global constraint store. It supports a notion of discrete time that allows all non-blocked agents to proceed with their execution simultaneously.
In this paper, we present a modular architecture for the simulation of tccp programs. The tool comprises three main components. First, a set of basic abstract instructions able to model the tccp agent behaviour, the memory model needed to manage the active agents and the state of the store during the execution. Second, the agent interpreter that executes the instructions of the current agent iteratively and calculates the new agents to be executed at the next time instant. Finally, the constraint solver components which are the modules that deal with constraints.
In this paper, we describe the implementation of these components and present an example of a real system modelled in tccp.

Autores: María del Mar Gallardo / Leticia Lavado / Laura Panizo / 
Palabras Clave: Abstract tccp instructions - Simulation tool - Timed Concurrent Constraint Language (tccp)

The language Hy-tccp was proposed as an extension of the Timed Concurrent Constraint paradigm (tccp) with continuous time and suitable mechanisms to handle continuous behaviors. This language provides a powerful model for hybrid and cyber-physical systems including concurrency and syn chronization features. In this paper, we propose a discretized operational semantics for Hy-tccp and an extension of the standard LTL to reason about temporal properties of Hy-tccp programs. The semantics and the logics will be the basis for the definition of formal verification and analysis tools, such as model checkers and theorem provers.

Autores: María del Mar Gallardo / Laura Panizo / Laura Titolo / 
Palabras Clave:

Nowadays, hybrid systems are present in many crucial tasks of our daily life. The hybrid character derives from the merge of continuous and discrete dynamics that are intrinsically related. The verification of critical properties of hybrid systems is of special importance, but sometimes it is not feasible due to their inherent complexity. In the last few years, several model-based testing and runtime verification techniques have been proposed to support the verification and validation of hybrid systems. In this paper, we present an interval logic that is suitable for specifying properties of event-driven hybrid systems. We introduce the syntax and semantics of the logic, and propose an automatic mechanism to transform each logic formula into a network of timed automata that can act as observers of the property in each test case using the UPPAAL tool.

Autores: Maria del Mar Gallardo / Laura Panizo / 
Palabras Clave: interval temporal logic - Timed automata - uppaal