Búsqueda avanzada

El autor María del Mar Gallardo ha publicado 8 artículo(s):

1 - A discretized operational semantics for the implementation of Hy-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:

2 - 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:

3 - Testing Temporal Logic on Infinite Java Traces

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 /  Damián Adalid, Alberto Salmerón, María del Mar Gallardo and Pedro Merino / 
Palabras Clave: Model checking - runtime monitoring - Testing

4 - 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:

5 - A Simulation Tool for tccp Programs (Trabajo de alto nivel)

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)

6 - 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

7 - An Event-driven Interval Temporal Logic for Hybrid Systems (Trabajo en progreso)

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

8 -