Búsqueda avanzada

El autor Alberto Salmerón ha publicado 2 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 - 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