Navegación

Búsqueda

Búsqueda avanzada

El autor Pedro Merino ha publicado 3 artículo(s):

1 - Using Model Checking to Generate Test Cases for Android Applications

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 / 
Palabras Clave:

2 - River basin management with SPIN

This paper presents the use of the SPIN model checker as the core engine to build Decision Support Systems (DSSs) to control complex river basins during flood situations. Current DSSs in this domain are mostly based on simulators to predict the rainfall and the water flow along the river basin.
In this paper, we propose a scheme that integrates simulators in the water domain with additional logic in P ROMELA to represent basin elements, such as dams, their management rules, the evolution of dam parameters (e.g. level or discharge capacity), and user defined constraints in the whole basin over time. Then, we use the exploration capabilities of SPIN to find out which sequences of operations over the dams produce a global behaviour that mitigates the effect of floods according to user defined constraints along the river basin. Although the method is general for any river basin with dams, it has been evaluated in a real basin in the south of Spain.

Autores: María del Mar Gallardo  / Pedro Merino  / Laura Panizo  /  Alberto Salmerón / 
Palabras Clave:

3 - A characterisation of reliability tools for Software Defined Networks (Trabajo original)

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