Person:
Núñez García, Manuel

First Name

Manuel

Last Name

Núñez García

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Informática

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 10 of 28

A formal framework to test soft and hard deadlines in timed systems
(Wiley-Blackwell, 2012-12) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael
This paper introduces a formal framework to specify and test systems presenting both soft and hard deadlines. While hard deadlines must always be met on time, soft deadlines can be sometimes met in a different time, usually greater, from the specified one. It is this characteristic (to formally definetextitsometimes) that produces several reasonable alternatives to define appropriate implementation relations, that is, relations to decide whether an implementation is correct with respect to a specification. In addition to introducing these relations, the paper also presents a formal testing framework to test implementations and provides an algorithm to derive sound and complete test suites with respect to the implementation relations previously defined. That is, an implementation conforms to a specification if and only if the implementation successfully passes all the tests belonging to the suite derived from the specification.
A logic for assessing sets of heterogeneous testing hypotheses
(Springer Verlag, 2006) García Merayo, Mercedes; Rodríguez Laguna, Ismael; Núñez García, Manuel
To ensure the conformance of an implementation under test (IUT) with respect to a specification requires, in general, the application of an infinite number of tests. In order to use finite test suites, most testing methodologies add some feasible hypotheses about the behavior of the IUT. Since these methodologies are designed for considering a fix set of hypotheses, they usually do not have the capability of dealing with other scenarios where the set of assumed hypotheses varies. We propose a logic to infer whether a set of observations (i.e., results of test applications) allows to claim that the IUT conforms to the specification if a specific set of hypotheses (taken from a repertory) is assumed.
THOTL: A timed extension of HOTL
(SPRINGER-VERLAG BERLIN, 2008) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael
THOTL represents a conservative extension of HOTL (Hypotheses and Observations Testing Logic) to deal with systems where time plays a fundamental role. We adapt some of the HOTL rules to cope with the new framework. In addition, we introduce several specific hypotheses and rules to appropriately express time assumptions. We provide a correctness result of THOTL with respect to a general notion of timed conformance.
An invitation to friendly testing
(Springer, 1998) Frutos Escrig, David de; Llana Díaz, Luis Fernando; Núñez García, Manuel
We present a new testing semantics, called friendly testing, whose main property is that the induced preorder between processes ⊑fr is consistent with the conformance relation, and so we have, for instance,a ⊕b ⊑fr a ⊑fr a +b. The new theory is strongly based on De Nicola & Hennessy’s work on testing. Friendly tests are defined exactly as in their work, except that internal actions are not allowed. However, in order to obtain the desired notion of friendly testing this restriction is not enough and we also have to relax the conditions to pass a test. Thus we obtain a new testing semantics and a new preorder between processes which is strictly weaker than the relation ⊑must. Moreover, we present an alternative characterization of our new testing semantics by defining a modification of acceptance sets.
Adaptación y ejecución de aplicaciones MPI en entornos de simulación para analizar el rendimiento de arquitecturas distribuidas
(2019-06-19) Núñez Covarrubias, Alberto; Pickin, Simon James; Lavín Puente, Víctor; Llana Díaz, Luis Fernando; Bartolomé Sandoval, Ana Isabel; Cerro Cañizares, Pablo; Cambronero Piqueras, María Emilia; Núñez García, Manuel; Vaca Vargas, Bryan Rául; Gómez-Zamalloa Gil, Miguel
Una parte fundamental de la asignatura PSD es el desarrollo de aplicaciones distribuidas. En concreto, la programación de aplicaciones paralelas utilizando MPI tiene un peso considerable, tanto en la parte práctica, como en la parte teórica de la asignatura. Las aplicaciones MPI desarrolladas en las prácticas de PSD pueden, normalmente, ejecutarse en un solo ordenador utilizando los distintos núcleos del procesador, lo cual se conoce como modo “stand-alone”. El objetivo principal del proyecto consiste en mitigar los problemas existentes para ejecutar las aplicaciones MPI, requeridas en las prácticas de PSD, en entornos distribuidos reales. Para ello proponemos el uso del simulador SIMCAN, el cual ya ha sido adaptado en el pasado para su uso docente. Concretamente, se propone utilizar SIMCAN para reproducir las trazas de ejecución de aplicaciones MPI en diferentes arquitecturas distribuidas, de forma que se alivien, en la medida de lo posible, aquellos aspectos de interés que se tratan con dificultad en la ejecución “stand-alone”, en particular, la visualización del funcionamiento distribuido y su rendimiento. De esta forma, se utilizarán distintas arquitecturas distribuidas, modeladas con el simulador SIMCAN, para ejecutar las aplicaciones MPI estudiadas en la asignatura.
Extending Stream X-Machines to specify and test systems with timeouts
(IEEE Computer Soc, 2008) García Merayo, Mercedes; Hierons, Robert M.; Núñez García, Manuel; Cerone, A; Gruner, S
Stream X-machines are a kind of extended finite state machine used to specify real systems where communication between the components is modeled by using a shared memory. In this paper we introduce an extension of the Stream X-machines formalism in order to specify delays/timeouts. The time spent by a system waiting for the environment to react has the capability of affecting the set of available outputs of the system. So, a relation focusing on functional aspects must explicitly take into account the possible timeouts. We also propose a formal testing methodology allowing to systematically test a system with respect to a specification. Finally, we introduce a test derivation algorithm. Given a specification, the derived test suite is sound and complete, that is, a system under test successfully passes the test suite if and only if this system conforms to the specification.
Metamorphic testing of OpenStreetMap
(Elsevier, 2021-05-17) Almendros Jiménez, Jesús M.; Becerra Terón, Antonio; García Merayo, Mercedes; Núñez García, Manuel
Context: OpenStreetMap represents a collaborative effort of many different and unrelated users to create a free map of the world. Although contributors follow some general guidelines, unsupervised additions are prone to include erroneous information. Unfortunately, it is impossible to automatically detect most of these issues because there does not exist an oracle to evaluate whether the information is correct or not. Metamorphic testing has shown to be very useful in assessing the correctness of very heterogeneous artifacts when oracles are not available. Objective: The main goal of our work is to provide a (fully implemented) framework, based on metamorphic testing, that will support the analysis of the information provided in OpenStreetMap with the goal of detecting faulty information. Method: We defined a general metamorphic testing framework to deal with OpenStreetMap. We identified a set of good metamorphic relations. In order to have as much automation as possible, we paid special attention to the automatic selection of follow-up inputs because they are fundamental to diminish manual testing. In order to assess the usefulness of our framework, we applied it to analyze maps of four cities in different continents. The rationale is that we would be dealing with different problems created by different contributors. Results: We obtained experimental evidence that shows the potential value of our framework. The application of our framework to the analysis of the chosen cities revealed errors in all of them and in all the considered categories. Conclusion: The experiments showed the usefulness of our framework to identify potential issues in the information appearing in OpenStreetMap. Although our metamorphic relations are very helpful, future users of the framework might identify other relations to deal with specific situations not covered by our relations. Since we provide a general pattern to define metamorphic relations, it is relatively easy to extend the existing framework. In particular, since all our metamorphic relations are implemented and the code is freely available, users have a pattern to implement new relations.
Formal testing of systems presenting soft and hard deadlines
(SPRINGER-VERLAG BERLIN, 2007) García Merayo, Mercedes; Núñez García, Manuel; Rodríguez Laguna, Ismael; Arbab, F; Sirjani, M
We present a formal framework to specify and test systems presenting both soft and hard deadlines. While hard deadlines must be always met on time, soft deadlines can be sometimes met in a different time, usually higher, from the specified one. It is this characteristic (to formally define sometimes) what produces several reasonable alternatives to define appropriate implementation relations, that is, relations to decide wether an implementation is correct with respect to a specification. In addition to introduce these relations, we define a testing framework to test implementations.
SQLab Extension: Laboratorio virtual lenguaje SQL
(2019-03-14) García Merayo, María de las Mercedes; Núñez García, Manuel; Estévez Martín, Sonia; Martínez Torres, Rafael; Ibias Martínez, Alfredo; Pareja Flores, Cristobal; Rincón Martínez, Santiago; Correas Fernández, Jesús
Extensión de la plataforma SQLab con nuevas funcionalidades que permitan a estudiantes de Bases de Datos evaluar sus conocimientos de diseño de instrucciones DML del lenguaje SQL y a los docentes hacer un seguimiento de la evolucion de sus alumnos.
Introducing friendly testing
(Univ. Vigo, 1997) Llana Díaz, Luis Fernando; Frutos Escrig, David de; Núñez García, Manuel; Fernández Iglesias, Manuel J.; Llamas Nistal, Martín; Pazos Arias, José Juan
We present a new testing semantics, called friendly testing, whose main property is that the induced preorder between processes v fr is consistent with the conformance relation, and so we have, for instance, a \Phi b v fr a v fr a + b. The new theory is strongly based on De Nicola & Hennessy's work on testing, and the structure of the paper closely follows that of Hennessy's book on the subject. Friendly tests are defined exactly as in his famous book, except that internal actions are not owed. However, this restriction is not enough and we also have to relax the conditions to pass a test in order to obtain the desired notion of friendly testing. Thus we obtain a new testing semantics and a new preorder between processes which is strictly weaker than the relation vmust . As a consequence, a fully abstract denotational semantics can be obtained as a quotient algebra of the corresponding construction for the must semantics, and the addition to the complete axiomatization of the latter of a single conformance axiom, gives us a complete axiomatization of our friendly testing semantics.