Mercedes G. Merayo

dblp:93/1152 · DBLP profile ↗
← Back
56ranked-venue papers
14as first author
9since 2021 · last 2026
0000-0002-4634-4082ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 35 · 11 first-author · 5 since 2021Artificial intelligence and machine learning · 15 · 3 since 2021Systems, architecture and hardware · 4 · 2 first-authorDatabases, data management, data science and information retrieval · 4Applied, interdisciplinary, general and emerging computing · 3 · 1 since 2021Computer networks · 2 · 2 first-authorHuman-computer interaction and ubiquitous computing · 1Theory of computation · 1
YearPublicationVenuePosition
2026 Combining sequential test cases into an equivalent set of adaptive test cases
abstract
When testing a state-based system one might use a set of (negative) test cases in which each test case is a sequence of events that should not occur. Testing then involves executing the system under test (SUT) in order to check whether any of these disallowed sequences can occur. While testing using such sequences can be effective, they introduce a source of inefficiency: if a test case expects the SUT to produce output a after observing a sequence σ and the SUT instead produces a different output a ′ after σ then testing with that test case did not show an error, because the SUT can autonomously produce outputs, and terminates because the test case only makes sense if the exact sequence is observed. This is a source of inefficiency if there is another test case that starts with σ followed by a ′ : we could have continued evaluating whether the application of this second test case leads to an error. This paper considers scenarios in which events represent inputs, outputs, or the passing of discrete time. We show how a set of sequential test cases can be converted into an equivalent set of adaptive test cases, with adaptivity addressing the above source of inefficiency. The proposed approach has the potential to improve efficiency when using any test generation technique that returns negative sequential test cases.
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
J. Log. Algebraic Methods Program.2
2024 Combining Metamorphic Testing and Machine Learning to Enhance OpenStreetMap
abstract
Metamorphic testing (MT) is a useful tool to test systems where an oracle is not available. MT relies on the definition of metamorphic relations (MR), that is, certain properties that relate a set of inputs and the set of outputs produced by the system under test (SUT) as response to these inputs. Usually, a violation of an MR implies that the SUT is faulty. However, some work on MT accepts, for certain SUTs, that the violation of an MRalmost alwaysis a symptom of an error but assumes the potential existence of false positives. This is the case, for instance, of our recent work where we applied MT to improve OpenStreetMap (OSM). Our MRs were able to uncover a large amount of errors in all the analyzed maps but we suffered the presence of a nonnegligible number of false positives. Therefore, an expert had to manually check the suspicious elements identified by our MRs. If we analyze large maps, then this manual task is unfeasible. In this article we solve the main limitation of our previous approach: we accurately and automatically discard false positives. Our new framework combines MT, along the same lines of our previous work, and machine learning. Specifically, we provide three models, one for each MR, based on the random forest model. The models were extensively trained with real data obtained from the application of MRs to maps of cities located in different continents. In order to evaluate the usefulness of our models, we tested them using different cities, in countries that were not considered in the training set. The results were very good: accuracy of the models is never lower than 0.90, it is usually much higher and in many situations reaches 1.0. The computation of the F1-scores yielded similar results.
Manuel Méndez, Antonio Becerra-Terón, Jesús Manuel Almendros-Jiménez, Mercedes G. Merayo, Manuel Núñez 0001
IEEE Trans. Reliab.4
2023 Long-term traffic flow forecasting using a hybrid CNN-BiLSTM model
abstract
The increase of road traffic in large cities during the last years has produced that long and short-term traffic flow forecasting is a critical need for the authorities. The availability of good traffic flow prediction methods is a must to make informed decisions concerning (punctual) traffic congestions. Previous work has shown that the accuracy of these methods decreases if we consider urban traffic and long-term predictions. In this paper we present a hybrid model, combining a Convolutional Neural Network and a Bidirectional Long–Short-Term Memory network, and apply it to long-term traffic flow prediction in urban routes. This model combines the capability of CNN to extract hidden valuable features from the input model and the capability of BiLSTM to understand the temporal context. In order to assess the usefulness of our model, we considered four streets of the city of Madrid with different characteristics and compared the results of our proposed model with the ones obtained by eight widely used baseline models. The results show that our hybrid model outperforms the baseline models with respect to three metrics commonly used in regression: mean absolute error, root mean squared error and accuracy.
Manuel Méndez, Mercedes G. Merayo, Manuel Núñez 0001
Eng. Appl. Artif. Intell.2
2023 Using Metamorphic Testing to Improve the Quality of Tags in OpenStreetMap
abstract
We present a metamorphic testing approach to validate the information included in OpenStreetMap, a collaborative effort to produce a free map of the world. We focus on the quality of the tags storing the information about the elements of the map. We identified metamorphic relations with the potential to detect different types of tagging errors. In particular, we carefully designed mechanisms to automatically generatefollow-up inputs, a fundamental component in the successful application of a metamorphic testing approach. The intrinsic nature of automatically analysing tags implies that we will detect real errors but some false positives as well. In order to obtain a good trade-off between real errors and false positives, we introducethresholds. Our MRs will raise an error associated with a certain value if, depending on the nature of the MR, we have a certain number of elements (not) fulfilling a given condition. In order to evaluate the goodness and versatility of our framework, we chose four cities in different continents with the goal of analysing very heterogeneous contributors adding information in different languages. The application of this framework to the analysis of the chosen cities revealed errors in all of them and in all the considered categories. In addition, around 66% of the errors found by our MRs in the analysed areas have not been previously reported byOsmose, the de facto standard OSM error checker.
Jesús Manuel Almendros-Jiménez, Antonio Becerra-Terón, Mercedes G. Merayo, Manuel Núñez 0001
IEEE Trans. Software Eng.3
2021 Using Genetic Algorithms To Select Test Cases For Finite State Machines With Timeouts
abstract
Testing software is an expensive and time consuming task. This drawback increases in the case that the system presents timeouts which affect the functional behaviour. In this case, it is necessary to invest more time to apply the test cases. Thus, it is desirable to diminish the amount of test cases to be applied and, consequently, the time devoted to test the system, as long as the fault detection capacity of the test cases is not affected. In this work, we introduce a genetic algorithm that selects a subset of test cases from an initial test suite for systems that present timeouts, with the goal of keeping a good level of effectiveness. We report on several experiments performed to compare the generated solutions with random selection and the original test suite.
Miguel Benito-Parejo, Mercedes G. Merayo
CEC2
2021 An Implementation of Formal Framework for Collective Systems in Air Pollution Prediction System
Rafal Palak, Krystian Wojtkiewicz, Mercedes G. Merayo
ICCCI3
2021 Metamorphic testing of OpenStreetMap
abstract
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. 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. 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. 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. 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.
Jesús Manuel Almendros-Jiménez, Antonio Becerra-Terón, Mercedes G. Merayo, Manuel Núñez 0001
Inf. Softw. Technol.3
2021 Wodel-Test: a model-based framework for language-independent mutation testing
Pablo Gómez-Abajo, Esther Guerra, Juan de Lara, Mercedes G. Merayo
Softw. Syst. Model.4
2021 CEViNEdit: improving the process of creating cognitively effective graphical editors with GMF
David Granada, Juan M. Vara, Mercedes G. Merayo, Esperanza Marcos
Softw. Syst. Model.3
2020 A Trading Framework Based on Fuzzy Moore Machines
Iván Calvo, Mercedes G. Merayo, Manuel Núñez 0001
ACIIDS (1)2
2020 An evolutionary algorithm for selection of test cases
abstract
Applying tests to an implementation to check its correctness is often expensive and may require an excessive amount of time. Hence, it is necessary to find a relatively small subset of tests able to detect as many errors as possible. In this paper, we study several approaches to choose such subsets of tests based on their capacity to detect faults. These faults are defined as mutation operators that are applied to the specification of the systems with the goal of simulating faulty versions called mutants. The different methods are evaluated to determine the ones that provide the best test suite according to the relevance of the tests, their capacity to detect fault and the number of inputs involved. All the algorithms proposed have been implemented in a tool freely available.
Miguel Benito-Parejo, Mercedes G. Merayo
CEC2
2020 An evolutionary technique for supporting the consensus process of group decision making
abstract
Discrepancies arise when experts have to decide the preference on alternatives for a problem. Henceforth, it is necessary to carry out a process during which they adjust their opinions in order to achieve an acceptable consensus. Usually, this process is coordinated by a moderator that makes suggestions to the participants regarding the most adequate changes. In order to simplify this process, we propose an evolutionary technique based on the search of the changes of the preferences that improve the consensus degree. We also consider that the opinions of the experts should stay closer to the original ones. Taking into account these two factors, we are able to provide useful feedback for the experts willing to get a consensus and measure how much improvement can be achieved.
Miguel Benito-Parejo, Mercedes G. Merayo, Manuel Núñez 0001
SMC2
2020 Guest Editorial: Special Section on ICTSS
Inmaculada Medina-Bulo, Mercedes G. Merayo, Robert M. Hierons
Inf. Softw. Technol.2
2019 Mutation testing for DSLs (tool demo)
abstract
Mutation testing (MT) is a well-known technique to evaluate and improve the quality of a given test-suite. While several MT tools exist for traditional programming languages, there is no common method to take advantage of MT in the case of domain-specific languages (DSLs). The current MT tools for DSLs are created ad-hoc, incurring in a high cost.
Pablo Gómez-Abajo, Esther Guerra, Juan de Lara, Mercedes G. Merayo
DSM@SPLASH4
2018 An Improved and Tool-Supported Fuzzy Automata Framework to Analyze Heart Data
Iván Calvo, Mercedes G. Merayo, Manuel Núñez 0001
ACIIDS (1)2
2018 Intelligent Collectives: Impact of Diversity on Susceptibility to Consensus and Collective Performance
Van Du Nguyen 0001, Hai Bang Truong, Mercedes G. Merayo, Ngoc Thanh Nguyen 0001
ICCCI (1)3
2018 Passive testing with asynchronous communications and timestamps
Mercedes G. Merayo, Robert M. Hierons, Manuel Núñez 0001
Distributed Comput.1
2018 A tool supported methodology to passively test asynchronous systems with multiple users
Mercedes G. Merayo, Robert M. Hierons, Manuel Núñez 0001
Inf. Softw. Technol.1
2018 Mutomvo: Mutation testing framework for simulated cloud and HPC environments
Pablo C. Cañizares, Alberto Nuñez, Mercedes G. Merayo
J. Syst. Softw.3
2018 A tool for domain-independent model mutation
Pablo Gómez-Abajo, Esther Guerra, Juan de Lara, Mercedes G. Merayo
Sci. Comput. Program.4
2018 Bounded Reordering in the Distributed Test Architecture
abstract
In the distributed test architecture, the system under test (SUT) interacts with its environment at multiple physically distributed ports and the local testers at these ports do not synchronize their actions. This presents many challenges and, in particular, apparently incorrect behaviors can be the consequence of an erroneous assumption about the exact order in which actions were performed at different ports. In previous work, we defined a conformance relation for the distributed test architecture. Essentially, the SUT is faulty if we observe a trace σ such that no admissible reordering of the actions in σ could have been produced by the specification. However, this notion can be weak if the compared traces might betoodifferent. This paper introduces conformance relations where, for a given metric, a reordering is only considered if the distance between the two traces is at most a certain boundk. We introduce two different metrics and provide algorithms to construct finite automata accepting theseclose, with respect to each metric, sequences. We also study the computational complexity of the two main problems associated with the new framework: deciding whether a trace is accepted by the new automaton and deciding whether one system conforms to a specification with respect to the new conformance relation.
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
IEEE Trans. Reliab.2
2017 Using fuzzy automata to diagnose and predict heart problems
abstract
In this paper we introduce a formalism to specify the behavior of biological systems. Our formalism copes with uncertainty, via fuzzy logic constraints, an important characteristic of these systems. We present the formal syntax and semantics of our variant of fuzzy automata. The bulk of the paper is devoted to present an application of our formalism: a formal specification of the heart that can help to detect abnormal patterns of behavior. Specifically, our model analyzes the heartbeats per minute and the longitude of the RR waves of a patient. The model takes into account the age and gender of the patient, where age is considered to be a fuzzy parameter. Finally, we use real data to analyze the reliability of the model concerning the diagnosis and prediction of potential illnesses.
Maria Azahara Camacho-Magrinan, Mercedes G. Merayo, Manuel Núñez 0001
CEC2
2017 Intelligent Collective: The Role of Diversity and Collective Cardinality
Van Du Nguyen 0001, Mercedes G. Merayo, Ngoc Thanh Nguyen 0001
ICCCI (1)2
2017 Preface: Special issue on software verification and testing
Mercedes G. Merayo, Gwen Salaün
J. Syst. Softw.1
2017 Introduction to the Software Engineering and Formal Methods 2013 special issue
Mario Bravetti, Robert M. Hierons, Mercedes G. Merayo
Softw. Syst. Model.3
2016 FARTHEST: FormAl distRibuTed scHema to dEtect Suspicious arTefacts
Pablo C. Cañizares, Mercedes G. Merayo, Alberto Nuñez
ACIIDS (1)2
2016 Controllability Through Nondeterminism in Distributed Testing
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
ICTSS2
2015 Passive testing of communicating systems with timeouts
Mercedes G. Merayo, Alberto Nuñez
Inf. Softw. Technol.1
2015 Introduction to the special issue on Mutation Testing
abstract
It is our pleasure to introduce this special issue on Mutation Testing. The special issue contains nine papers, including four extended versions of papers presented at the 7th International Workshop on Mutation Analysis and five new submissions. We have divided the special issue into three broad areas based on the topics covered. The first area focuses on the techniques for making mutation testing more efficient and practical; the second area revisits some fundamental questions about mutants, whilst the third area presents some advanced applications of mutation testing for model-based testing. Mutation Testing has been proven to be an effective way to measure the quality of a test suite in terms of its ability to detect faults 1. The history of mutation testing can be traced back to 1971 in a publication by Richard Lipton 2 as well as in publications from the late 1970s by DeMillo et al. 3 and Hamlet 4. In Mutation Testing, faults are deliberately seeded into the original program (by simple syntactic changes) to create a set of faulty programs called mutants, each containing a different syntactic change. The general principle underpinning Mutation Testing is that artificial faults can be used to represent common programming mistakes. By carefully choosing the location within the program and the types of faults, it is possible to simulate any test adequacy criteria whilst providing improved fault detection. A recent survey on mutation testing provides evidence to suggest that the approach is increasing in maturity and practical application 5. One reason why mutation testing has become a popular testing approach is that it is a straightforward process to apply. To assess the quality of a given test set, the generated mutants are executed against the input test set. If the result of running a mutant is different from the result of running the original program for any test cases in the input test set, the seeded fault denoted by the mutant is detected. One outcome of the Mutation Testing process is the mutation score, which indicates the quality of the input test set. The mutation score is the ratio of the number of detected faults over the total number of seeded faults. Mutation Testing has been widely adopted in the academic community as a means to evaluate software testing techniques 6, as well as to generate tests and test oracles 7, 8. However, it still suffers from a number of problems that prevent the wider industrial uptake of this effective testing approach. One problem that prevents Mutation Testing from becoming a practical testing technique is the high computational cost of executing a large number of mutants against a test set. Other problems are related to the amount of effort involved in identifying equivalent mutants. Each submission received three reviews from a board of 36 mutation testing experts. For all submissions extended from the mutation workshop, we have recruited at least one new reviewer to ensure wider accessibility to a non-mutation expert testing audience. The first area covers the topic of making mutation testing more efficient and practical. The three papers in this area introduce novel techniques to optimize mutant execution, to reduce redundant mutants and to detect equivalent mutants. In the first paper 'Reducing Mutation Costs Through Uncovered Mutants', Pedro Reales Mateo and Macario Polo Usaola propose an improved mutant schema, namely, 'MUSIC' to reduce the execution cost for mutation testing. The MUSIC approach records runtime information about structural and mutation coverage; it reduces the execution cost by removing mutant execution tasks, which are not covered by the test cases. The second paper 'Higher Accuracy and Lower Run Time: Efficient Mutation Analysis using Non-redundant Mutation Operators' by René Just and Franz Schweiggert attempts to reduce the number of mutants by applying only non-redundant mutation operators. The authors identified a set of operators that tend to not generate any redundant mutants, and their results show that 20% of the runtime cost could be saved using the selected operators. The third paper 'Employing Second-order Mutation for Isolating First-order Equivalent Mutants' by Marinos Kintis, Mike Papadakis and Nicos Malevris seeks to automatically identify equivalent mutants through higher order mutation. Their approach combines impact analysis for both first-order and second-order mutants, and it achieved an equivalent mutant classification precision of 73% and a classification recall of 65%. The three papers in the second area revisit some fundamental questions about mutants and explore a new application of mutation testing. The first paper 'Quality Metrics for Mutation Testing with Applications to WS-BPEL Compositions' by Antonia Estero-Botaro, Francisco Palomo-Lozano, Inmaculada Medina-Bulo, Juan José Domínguez-Jiménez and Antonio García-Domínguez attempts to discover what it means for mutants to be effective. They formally define a set of metrics to measure the quality of mutation operators and evaluate them using WS-BPEL applications. The second paper 'MuRanker: a Mutant Ranking Tool' by Akbar Siami Namin, Xiaozhen Xue, Omar Rosas and Pankaj Sharma proposes metrics to measure the mutant complexity based on how easy or hard they are to kill. They implemented a prototype tool, MuRanker, which can help testers to prioritize the analysis of mutants based on their killing ability. The third paper 'Metallaxis-FL: Mutation-based Fault Localisation' by Mike Papadakis and Yves Le Traon explores the application of mutation testing for fault localization. This approach combines code coverage and mutation information to rank suspicious statements. The results show that it outperforms other traditional coverage-based fault detection approaches. The third area covers some advanced applications of mutation analysis for model-based testing techniques. This is an under-studied area compared with traditional program mutation. The first paper 'Using Mutation to Assess Fault Detection Capability of Model Review' by Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene introduces a set of mutation operators for NuSMV Models. The mutant models simulate common behavioural faults and can be used to evaluate the fault detection ability of automated model review techniques. The second paper 'Towards an Automation of the Mutation Analysis Dedicated to Model Transformation' by Vincent Aranega, Jean-Marie Mottu, Anne Etien, Thomas Degueule, Benoit Baudry and Jean-Luc Dekeyser proposes to use mutation testing to test model transformations. They designed a set of mutation operators targeting three actions in model transformation: navigation, filtering and creation/modification. These are evaluated on the class2rdbms technique, which generates relational database management systems model from class diagrams. The third paper 'Model-based Mutation Testing from Security Protocols in HLPSL' by Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam, Ghazi Maatoug and Michael Rusinowitch proposes a set of mutation operators to generate mutants for HLPSL security protocols. It also demonstrates that concretization test data generation techniques can be used to construct test scripts to kill the mutants. We wish to thank the authors and reviewers for their contributions to this special issue and Rob Hierons and Jeff Offutt for helping to manage the review process.
Yue Jia 0001, Mercedes G. Merayo, Mark Harman
Softw. Test. Verification Reliab.2
2014 Timed implementation relations for the distributed test architecture
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
Distributed Comput.2
2013 Guest Editorial: Special Section from the 11th International Conference on Quality Software (QSIC 2011)
Robert M. Hierons, Mercedes G. Merayo
Inf. Softw. Technol.2
2013 Using genetic algorithms to generate test sequences for complex timed systems
Alberto Nuñez, Mercedes G. Merayo, Robert M. Hierons, Manuel Núñez 0001
Soft Comput.2
2012 Using Time to Add Order to Distributed Testing
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
FM2
2012 MAScloud: A Framework Based on Multi-Agent Systems for Optimizing Cost in Cloud Computing
Alberto Nuñez, César Andrés, Mercedes G. Merayo
ICCCI (1)3
2012 Implementation relations and test generation for systems with distributed interfaces
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
Distributed Comput.2
2012 Formal passive testing of timed systems: theory and tools
abstract
SUMMARY This paper presents a methodology to perform passive testing of timed systems. In passive testing, the tester does not interact with the implementation under test. On the contrary, execution traces are observed without interfering with the behaviour of the system. Invariants are used to represent the most relevant expected properties of the implementation under test. Intuitively, an invariant expresses the fact that each time the implementation under test performs a given sequence of actions, it must exhibit a behaviour in a lapse of time reflected in the invariant. There are two types of invariants: consequent and observational. The paper gives two algorithms to decide the correctness of proposed invariants with respect to a given specification and algorithms to check the correctness of a log, recorded from the implementation under test, with respect to an invariant. The soundness of this methodology is shown by relating it to an implementation relation. In addition to the theoretical framework, a tool called PASTE has been developed. This tool helps in the automation of the passive testing approach because it implements all the algorithms presented in this paper. PASTE takes advantage of mutation testing techniques in order to evaluate the goodness of an invariant according to its capability to detect errors in logs generated from mutants. An empirical study where PASTE was used to analyse a non‐trivial system is also reported. Copyright © 2012 John Wiley & Sons, Ltd.
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
Softw. Test. Verification Reliab.2
2012 A formal framework to test soft and hard deadlines in timed systems
abstract
SUMMARY 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. Copyright © 2011 John Wiley & Sons, Ltd.
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
Softw. Test. Verification Reliab.1
2011 Testing timed systems modeled by Stream X-machines
Mercedes G. Merayo, Manuel Núñez 0001, Robert M. Hierons
Softw. Syst. Model.1
2011 Scenarios-based testing of systems with distributed ports
abstract
SUMMARY Distributed systems are usually composed of several distributed components that communicate with their environment through specific ports. When testing such a system we separately observe sequences of inputs and outputs at each port rather than a global sequence and potentially cannot reconstruct the global sequence that occurred. Typically, the users of such a system cannot synchronize their actions during use or testing. However, the use of the system might correspond to a sequence of scenarios, where each scenario involves a sequence of interactions with the system that, for example, achieves a particular objective. When this is the case there is the potential for a significant delay between two scenarios and this effectively allows the users of the system to synchronize between scenarios. If we represent the specification of the global system by using a state‐based notation, we say that ait scenario is any sequence of events that happens between two of these operations. We can encode scenarios in two different ways. The first approach consists of marking some of the states of the specification to denote these synchronization points. It transpires that there are two ways to interpret such models and these lead to two implementation relations. The second approach consists of adding a set of traces to the specification to represent the traces that correspond to scenarios. We show that these two approaches have similar expressive power by providing an encoding from marked states to sets of traces. In order to assess the appropriateness of our new framework, we show that it represents a conservative extension of previous implementation relations defined in the context of the distributed test architecture: if we consider that all the states are marked then we simply obtain ioco (the classical relation for single‐port systems) while if no state is marked then we obtain dioco (our previous relation for multi‐port systems). Finally, we concentrate on the study of controllable test cases, that is, test cases such that each local tester knows exactly when to apply inputs. We give two notions of controllable test cases, define an implementation relation for each of these notions and relate them. We also show how we can decide whether a test case satisfies these conditions. Copyright © 2011 John Wiley & Sons, Ltd.
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
Softw. Pract. Exp.2
2010 MACRO-SYS: An Interactive Macroeconomics Simulator for Advanced Learning
César Andrés, Mercedes G. Merayo, Yaofeng Zhang
ACIIDS (2)2
2010 Multi-objective Genetic Algorithms: Construction and Recombination of Passive Testing Properties
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
SEKE2
2009 Analysis of the OLSR Protocol by Using Formal Passive Testing
abstract
In this paper we apply a passive testing methodology to the analysis of a non-trivial system. In our framework, so-called invariants provide us with a formal representation of the requirements of the system. In order to precisely express new properties in multi-node environments, in this paper we introduce a new kind of invariants. We apply the resulting framework to perform a complete study of a MANET routing protocol: The optimized link state routing protocol.
César Andrés, Stéphane Maag, Ana R. Cavalli, Mercedes G. Merayo, Manuel Núñez 0001
APSEC4
2009 A Statistical Approach to Test Stochastic and Probabilistic Systems
Mercedes G. Merayo, Iksoon Hwang, Manuel Núñez 0001, Ana R. Cavalli
ICFEM1
2009 Passive Testing of Stochastic Timed Systems
abstract
In this paper we introduce a formal methodology to perform passive testing, based on invariants, for systems where the passing of time is represented in probabilistic terms by means of probability distributions functions. In our approach, invariants express the fact that each time the implementation under test performs a given sequence of actions, then it must exhibit a behavior according to the probability distribution functions reflected in the invariant. We present algorithms to decide the correctness of the proposed invariants with respect to a given specification. Once we know that an invariant is correct, we check whether the execution traces observed from the implementation respect the invariant. In addition to the theoretical framework we have developed a tool, called PASTE, that helps in the automation of our passive testing approach. We have used the tool to obtain experimental results from the application of our methodology.
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
ICST2
2009 Applying Formal Passive Testing to Study Temporal Properties of the Stream Control Transmission Protocol
abstract
In this paper we present a formal passive testing framework and use it to analyze time aspects in the Stream Control Transmission Protocol (\SCTP). This protocol presents different phases where time aspects are critical. In order to represent temporal requirements we use so-called {\it timed invariants} since they allow us to easily verify that the traces collected from the observation of the protocol fulfill the corresponding timed constraints. In addition to introduce our theoretical framework, we report on the results obtained from the application of our techniques over (possibly mutated) traces extracted from runs of the SCTP.
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
SEFM2
2009 Using a Mining Frequency Patterns Model to Automate Passive Testing of Real-time Systems
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
SEKE2
2009 Mutation testing from probabilistic and stochastic finite state machines
Robert M. Hierons, Mercedes G. Merayo
J. Syst. Softw.2
2008 Passive Testing of Timed Systems
César Andrés, Mercedes G. Merayo, Manuel Núñez 0001
ATVA2
2008 Controllable Test Cases for the Distributed Test Architecture
Robert M. Hierons, Mercedes G. Merayo, Manuel Núñez 0001
ATVA2
2008 Extending Stream X-Machines to Specify and Test Systems with Timeouts
abstract
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.
Mercedes G. Merayo, Robert M. Hierons, Manuel Núñez 0001
SEFM1
2008 Formal testing from timed finite state machines
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
Comput. Networks1
2008 Extending EFSMs to Specify and Test Timed Systems with Action Durations and Time-Outs
abstract
In this paper we introduce a timed extension of the extended finite state machines model. On the one hand, we consider that (output) actions take time to be performed. This time may depend on several factors such as the value of variables. On the other hand, our formalism allows to specify timeouts. In addition to present our language, we develop a testing theory. First, we define ten timed conformance relations and relate them. Second, we introduce a notion of timed test and define how to apply tests to implementations. Finally, we give an algorithm to derive sound and complete test suites with respect to the implementation relations presented in the paper.
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
IEEE Trans. Computers1
2007 A Brief Introduction to THOTL
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
ATVA1
2007 Testing conformance on Stochastic Stream X-Machines
abstract
Stream X-machines have been used to specify real systems requiring to represent complex data structures. One of the advantages of using stream X-machines to specify a system is that it is possible to produce a test set that, under certain conditions, detects all the faults of an implementation. In this paper we present a formal framework to test temporal behaviors in systems where temporal aspects are critical. Temporal requirements are expressed by means of random variables and affect the duration of actions. Implementation relations are presented as well as a method to determine the conformance of an implementation with respect to a specification by applying a test set.
Mercedes G. Merayo, Manuel Núñez 0001
SEFM1
2007 Generation of optimal finite test suites for timed systems
abstract
One of the main problems to test timed systems is that the tester has to decide when to apply the next input to the system under test. Even though the tester could determine good sequences of inputs to find a big variety of errors, the quality of the test suite usually depends on the time when the different parts of the sequences are applied. In this paper we give a formal methodology to provide good time values to test timed systems. These values are computed by taking into account the time stability of the system, that is, if the system is more likely to remain in its current internal state during a given time interval then no input will be applied during that period. In other words, our method will (probabilistically) find those time values that are closer to a change of state in the system, being these values more suitable to apply the appropriate input to the system.
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
TASE1
2006 Extending EFSMs to Specify and Test Timed Systems with Action Durations and Timeouts
Mercedes G. Merayo, Manuel Núñez 0001, Ismael Rodríguez 0001
FORTE1