Abstract Models play a critical role in supporting Verification and Validation activities. However, they are often unavailable in practice, such as for legacy systems or third-party components. Model learning addresses this gap through two main approaches: passive learning, which infers models from existing execution traces, and active learning, which interacts with the system under learning (SUL) to generate more general models, but at higher computational cost. In this work, we propose a novel application of Transformer architectures to implicitly learn generic system models from execution traces alone, combining the efficiency of passive learning with the generality of active learning. We design and evaluate two Transformer-based architectures: one focused on exploitation, achieving over $$\varvec{95\%}$$ valid trace generation; and another focused on exploration, generating approximately $$\varvec{60\%}$$ novel, previously unseen traces. Our methods outperform state-of-the-art model learning techniques, demonstrating that Transformers can achieve results comparable to active learning while requiring significantly fewer resources.

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.

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.

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.

Failed Error Propagation greatly reduces the effectiveness of Software Testing by masking faults present in the code. This situation happens when the System Under Test executes a faulty statement, the state of the system is affected by this fault, but the expected output is observed. Therefore, it is a must to assess its impact in the testing process. Squeeziness has been shown to be a useful measure to assess the likelihood of fault masking in deterministic systems. The main goal of this paper is to define a new Squeeziness notion that can be used in a scenario where we may have non-deterministic behaviours. The new notion should be a conservative extension of the previous one. In addition, it would be necessary to evaluate whether the new notion appropriately estimates the likelihood that a component of a system introduces Failed Error Propagation. We defined our black-box scenario where non-deterministic behaviours might appear. Next, we presented a new Squeeziness notion that can be used in this scenario. Finally, we carried out different experiments to evaluate the usefulness of our proposal as an appropriate estimation of the likelihood of Failed Error Propagation. We found a high correlation between our new Squeeziness notion and the likelihood of Failed Error Propagation in non-deterministic systems. We also found that the extra computation time with respect to the deterministic version of Squeeziness was negligible. Our new Squeeziness notion is a good measure to estimate the likelihood of Failed Error Propagation being introduced by a component of a system (potentially) showing non-deterministic behaviours. Since it is a conservative extension of the original notion and the extra computation time needed to compute it, with respect to the time needed to compute the former notion, is very small, we conclude that the new notion can be safely used to assess the likelihood of fault masking in deterministic systems.

Chess engines are computer programs that analyse chess positions. The goal of this analysis is to decide which player has an advantage and evaluate how big the advantage is. Using this analysis, chess engines are really powerful players who can consistently beat the best (human) players. Even though these programs are fantastic players, we cannot be sure that the code is fault free because it is very difficult to test them. In particular, we face the oracle problem: if the chess engine plays better than any potential tester, how can a tester claim that a certain evaluation is wrong or that a suggested move is not the best one? The main goal of our work is to provide a metamorphic testing tool to evaluate chess engines. In particular, we are interested in looking for inconsistent behaviours in the best publicly available chess engine, Stockfish, but we would also like to consider other chess engines. We developed a metamorphic testing solution to validate chess engines. First, we defined metamorphic relations that might reveal inconsistent behaviours. The underlying idea was that the evaluation of related positions should be the same. For example, if we consider a position and rotate all the pieces with respect to the central axis, then both positions should have the same evaluation. One of our main priorities was to have a fully automatised tool. Source inputs are obtained from available datasets while follow-up inputs are automatically computed by applying sound transformations to the source inputs with respect to the corresponding metamorphic rule. In order to assess the usefulness of our work, we applied it to analyse a dataset with more than 40,000 positions. Empirical evidence validates the usefulness of our work to analyse the best available chess engine, Stockfish. Our tool revealed non-negligible deviations from the expected behaviour in Stockfish for all the MRs. Additional experiments showed that our tool can be easily used to analyse other chess engines such as Komodo, Houdini and Gull. The experiments demonstrate the usefulness of our approach to identify issues in the latest version of the widely recognised to be the best chess engine: Stockfish (version 15, released in April 2022). Our tool is flexible and can be easily extended with metamorphic relations that can be defined in the future by either us or other users. Since all our metamorphic relations are implemented and the code is freely available, users can use them as a pattern to implement new relations.

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.

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.

The validation of a cloud system can be complicated by the size of the system, the number of users that can concurrently request services, and the virtualization used to give the illusion of using dedicated machines. Unfortunately, it is not feasible to use conventional testing methods with cloud systems. This article proposes a framework, called TEA-Cloud, that integrates simulation with testing methods for validating cloud system designs. Testing is applied on both functional and nonfunctional aspects of the cloud, like performance and cost. The aim of the framework is to provide a complete methodology to help users to model both software and hardware parts of cloud systems and automatically test the validity of these clouds using a cost-effective approach. Metamorphic testing is used to overcome the lack of an oracle that checks whether the behavior observed in testing is allowed. Metamorphic testing is based on metamorphic relations (MRs). We define three families of MRs, which target issues such as performance, resource provisioning, and cost. TEA-Cloud was evaluated through an empirical study that used fault seeding (mutation) and ten MRs for testing different cloud configurations. The results were promising, with TEA-Cloud finding all seeded faults.

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.

Mutation Testing is an effective testing technique that relies in the generation of mutants from the system under test. The main limitation of this technique is that the potential number of mutants is usually huge. Therefore, it is important to classify and select mutants in order to avoid repetitive, useless or excessive computations, and biased results. In this paper we focus on avoiding too many executions and/or biased results by classifying mutants into two categories: hard-to-kill and easy-to-kill mutants. We propose a new swarm intelligence algorithm to classify a set of mutants between those two classes and we show how our algorithm compares to other approaches.

Particle Swarm Optimization (PSO) has been successfully applied to find good solutions through a guided search. This optimization technique usually works with vectors as individuals of the population conforming the search space. Nevertheless, there exist problems such that the search space cannot be transformed into a vector search space. In this paper we propose a novel technique based on the intuition behind PSO but overcoming its limitations concerning search spaces. Specifically, we present a PSO framework where the individuals conforming the search space are tree-like structures. In particular, our framework naturally includes classical PSO but also search spaces where elements are structures that can be represented as trees (in addition to usual trees, linear structures such as lists, queues and stacks).

This paper presents an exact search-based technique to minimize test suites while maintaining their mutation coverage. The minimization of test suites is a hard problem whose solution is important both to reduce the cost of mutation testing and to precisely assess the quality of existing test suites. This problem can be addressed with Search-Based Software Engineering (SBSE) techniques, including metaheuristics and exact techniques. We have applied Integer Linear Programming (ILP) as an exact technique to reduce the effort of testing with very promising results. Our technique can be adapted to different formalisms but this paper focuses on testing WS-BPEL compositions, as it poses several interesting problems. Despite the fact that web service compositions are relatively small, as they just orchestrate web services, their execution can be very expensive because the deployment and execution of web services, and the underlying infrastructure, are not trivial. Therefore, although test suites for the compositions themselves are also usually small, it is fundamental to reduce, as much as possible and without losing coverage, their size.

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.

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.

Mutation testing is a method used to assess and improve the fault detection capability of a test suite by creating faulty versions, called mutants, of the system under test. Evolutionary Mutation Testing (EMT), like selective mutation or mutant sampling, was proposed to reduce the computational cost, which is a major concern when applying mutation testing. This technique implements an evolutionary algorithm to produce a reduced subset of mutants but with a high proportion of mutants that can help the tester derive new test cases (strong mutants). In this paper, we go a step further in estimating the ability of this technique to induce the generation of test cases. Instead of measuring the percentage of strong mutants within the subset of generated mutants, we compute how much the test suite is actually improved thanks to those mutants. In our experiments, we have compared the extent to which EMT and the random selection of mutants help to find missing test cases in C++ object-oriented systems. We can conclude from our results that the percentage of mutants generated with EMT is lower than with the random strategy to obtain a test suite of the same size and that the technique scales better for complex programs.

Abstract Formal methods are one of the most important approaches to increasing the confidence in the correctness of software systems. A formal specification can be used as an oracle in testing since one can determine whether an observed behaviour is allowed by the specification. This is an important feature of formal testing: behaviours of the system observed in testing are compared with the specification and ideally this comparison is automated. In this paper we study a formal testing framework to deal with systems that interact with their environment at physically distributed interfaces, called ports, and where choices between different possibilities are probabilistically quantified. Building on previous work, we introduce two families of schedulers to resolve nondeterministic choices among different actions of the system. The first type of schedulers, which we call global schedulers , resolves nondeterministic choices by representing the environment as a single global scheduler. The second type, which we call localised schedulers , models the environment as a set of schedulers with there being one scheduler for each port. We formally define the application of schedulers to systems and provide and study different implementation relations in this setting.

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.

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.

We consider the formal representation and analysis of systems with fuzzy-time information. First, we present a formalism to represent specifications. This model exploits the concepts of fuzzy set theory and uses a mathematical framework to get a more flexible approach. As it is usually assumed in industrial case studies, we consider that the original requirements of the specification may change. The implementation is built with respect to these changes but the specification is not upgraded. Thus, it may be outdated. In order to continue using the formal framework, the specification must be adapted with respect to these new requirements. We consider that this update process should be as non-intrusive as possible, that is, without using the source-code of the implementation. We present a novel methodology for self-evolving fuzzy-time systems, without interacting with the source code.

This paper aims to construct an evolutionary system, based on genetic algorithms, to solve the problem of univocally reaching a target state in a non-deterministic Finite State Machine. Our approach proposes the creation of an adaptive sequence, which is a tree of input and outputs that contains the possible behaviors of the non-deterministic Finite State Machine, through a Genetic Algorithm. Essentially, we will characterize the DNA of the individuals as an adaptive sequence and allow the population to evolve until a solution is found. To assure the validity of our approach, we compare it with other methodologies such as hillclimbing and random. We show that the Genetic Algorithm obtains a higher rate of success in creating the adaptive sequences.

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.

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.

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.

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.

In this paper we define simulation relations for distributed systems. Taking as starting point our previous work on the distributed testing architecture, we introduce novel simulation relations that can be used to define, given a specification, what a good implementation is. We approach the problem from two different perspectives. First, we consider that different ports of the system cannot share information. Thus, the decision to consider whether a system is correct has to be based only on local observations. We give some examples to show that this relation is very weak and propose a new one where we allow the different ports to {\it partially communicate}. Specifically, we do not implement a complex synchronization mechanism but allow entities to combine whole traces to obtain a verdict.

The language RTPA, Real Time Process Algebra, has been created to enable rigorous treatment of knowledge representation and manipulation in terms of to be I to have / to do in a formal and coherent framework. This language has been designed to cope with the three dimensions involved in the problem of software specification: (i) mathematical operations, (ii) event/process timing, and (iii) memory manipulation. In this paper we focus on giving a testing semantics to the second dimension: Process timing dimension. First, we will provide a SOS like operational semantics for the process relations of RTPA. Next, we will define what a test is and we will introduce a relation based on which tests are passed by processes. Finally, we will obtain an operational characterization that can be used as a first step to define a denotational sematics sound and complete with respect the testing semantics.

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.

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.

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.

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.

This paper presents a generic formal framework to specify and test autonomous e-commerce agents. First, the formalism to represent the behaviour of agents is introduced. The corresponding machinery to define how implementations can be tested follows. Two testing approaches are considered. The first of them, which can be called active, is based on stimulating the implementation under test (IUT) with a test. The peculiarity is that tests will be defined as a special case of autonomous e-commerce agent. The second approach, which can be called passive, consists of observing the behaviour of the tested agent in an environment containing other agents. As a case study the framework is applied to the e-commerce system Kasbah. Copyright © 2005 John Wiley & Sons, Ltd.

Abstract. In this paper we present a design framework containing a process algebra and the concurrent functional programming language Eden. In order to study properties of a specification written in our process algebraic notation, we provide a translation mechanism to generate Eden programs. Once we have a translation, we may use the Eden tools to study the performance of the (simulation of the) system. In order to add expressiveness to our design language we use a very powerful process algebra. First, we allow the specification of delays induced by general random variables. We also consider value passing. Finally, the communication between concurrent processes is asynchronous. The usefulness of our framework is presented by two examples featuring all the characteristics of our process algebraic model, we give the corresponding translations, and we provide some performance measures obtained by using Eden tools.

In this paper we present a construction smoothly integrating pattern matching with abstract data types. We review some previous proposals [19, 23, 20, 6, 1] and their drawbacks, and show how our proposal can solve them. In particular we pay attention to equational reasoning about programs containing this new facility. We also give its formal syntax and semantics, as well as some guidelines in order to compile the construction efficiently.