An account of classical Greek and Latin ideas of the Soul from antiquity to the nineteenth century.
Model-checkers have recently been suggested for automated software test-case generation. Several works have presented methods that create efficient test-suites using model-checkers. Ease of use and complete automation are major advantages of such approaches. However, the use of a model-checker comes at the price of potential performance problems. If the model used for test-case generation is complex, then model-checker based approaches can be very slow, or even not applicable at all. In this paper, we identify that unnecessary, redundant calls to the model-checker are one of the causes of bad performance. To overcome this problem, we suggest the use of temporal logic rewriting techniques, which originate from runtime verification research. This achieves a significant increase in the performance, and improves the applicability of model-checker based test-case generation approaches in general. At the same time, the suggested techniques achieve a reduction of the resulting test-suite sizes without degradation of the fault sensitivity. This helps to reduce the costs of the test-case execution.
Model-based regression testing is an important activity that ensures the reliability of evolving software. One of the major issues in this type of testing is the optimal selection of test-cases to test the affected portion of the software. In this paper, we present a UML based selective regression testing strategy that uses state machines and class diagrams for change identification. We identify the changes using the UML 2.1 semantics of state machines and class diagram. The changes are classified as Class-driven (obtained from class diagram) and State-driven (obtained from state machine). The Class-driven changes are important as these changes are not reflected on the state machines and they might be helpful in identifying some fault-revealing test cases. With the help of the identified changes, we classify the test cases of the test suite as Obsolete, Reusable, and Retestable. We apply the approach on a case study to demonstrate its validity.
Counterexamples produced by model checkers are frequently exploited for the purpose of testing. Counterexamples and test cases are generally treated as essentially the same thing, while in fact they can differ significantly. For example, it might take more than one test case to "cover" a given counterexample, because not all property violations can be illustrated with linear counterexamples. This paper presents a formal relationship between counterexamples and test cases in the context of the Computation Tree Logic (CTL), the logic of the popular model checker SMV. Given a test requirement as a CTL formula, we define what it means for a set of test cases to cover a counterexample associated with that requirement. This result can not only be used in the generation of a test set that satisfies a given test coverage criterion, but also in the determination of whether an extant test set satisfies the criterion. Our results can guide the production of counterexamples in model checkers explicitly intended to support testing.
Practitioners regard software testing as the central means for ensuring that a system behaves as expected. Due to the recent widespread adoption of model-driven development (MDD), code is no longer the single source for selecting test cases. Testing against original expectations can be done with model-based testing that adopts high-level models as the basis for test generation. In addition to test generation, challenges to model-based testing include creation and maintenance of traceability information among test-related artifacts. Traceability is required to support activities such as result evaluation, regression testing and coverage analysis. MDD and model transformation solutions address the traceability problem by creating relationships among transformed artifacts throughout the transformation process. This paper proposes an approach that leverages model transformation traceability techniques to create fine-grained relationships among model-based testing artifacts. Relationships are created during the test generation process. Their fine granularity enables the support for result evaluation, coverage analysis and regression testing.
We have devised a novel technique to automatically generate test cases for a software system, combining black-box model-based testing with white-box parameterized unit testing. The former provides general guidance for the structure of the tests in the form of test sequences, as well as the oracle to check for conformance of an application under test with respect to a behavioral model. The latter finds a set of concrete parameter values that maximize code coverage using symbolic analysis. By applying these techniques together, we can produce test definitions (expressed as code to be run in a test management framework) that exercise all selected paths in the model, while also covering code branches specific to the implementation. These results cannot be obtained from any of the individual approaches alone, as the model cannot predict what values are significant to a particular implementation, while parameterized unit testing requires manually written test sequences and correctness validations. We provide tool support, integrated into our model-based testing tool.
When integrating different system components, the interaction between different features is often error prone. Typically errors occur on interruption, concurrency or disabling/enabling between different features. Test case generation for integration testing struggles with two problems: the large state space and that these critical relationships are often not explicitly modeled. The approach presented in this paper is to use task models to describe the interaction between environment and system. This restricts the possible state space to a feasible size and enables the generation of task sequences, which cover the critical interaction scenarios. These task sequences are too abstract for testing the System-Under-Test (SUT), due to missing input- and expected output behavior. To overcome the different abstraction levels, the tasks are mapped to component behavior models. Based on this mapping, task sequences can be enriched with additional information from the component models and thereby executed to test the SUT.
In this paper, we adapt the abstraction refinement techniques of Clarke et al. [7] and Gulavani et al. [15] for systematic generation of model based test cases. Formal models are in general infinite state machines. We approximate such a formal model by a more abstract finite state machine. From the finite model, we obtain probable test cases through model checking, and then a guided symbolic execution is performed over the given formal model to check if this is a real test case. In case of failure, the finite abstract model is refined and the cycle is repeated. The two main results of this paper are: (a) better specification coverage is achieved, and (b) we obtain a more accurate coverage estimate. We explain our method by considering models in the specification language B.
Nowadays test engineers use various strategies for the design of test cases. Among others, test cases are designed on basis of structural coverage criteria or test cases are related to specific fault models. In this paper we evaluate these two techniques for test purpose design. We present a heuristic algorithm for the extraction of test cases from TGV's output, i.e., the test process. We discuss the problem of overlapping test purposes and illustrate improvements in terms of test execution time and in terms of number of test cases when minimizing this overlap. Furthermore, we present different strategies for the generation of fault-based test purposes. For our evaluation we apply the presented techniques to a Session Initiation Protocol (SIP) Registrar specification. All extracted test cases are executed against a commercial and an open source implementation of such a SIP Registrar.
This paper presents an original model-based testing approach that takes a UML behavioural view of the system under test and automatically generates test cases and executable test scripts according to model coverage criteria.This approach is embedded in the LEIRIOS Test Designer tool and is currently deployed in domains such as Enterprise IT and electronic transaction applications.This model-based testing approach makes it possible to automatically produce the traceability matrix from requirements to test cases as part of the test generation process.This paper defines the subset of UML used for model-based testing and illustrates it using a small example.
This paper is a contribution to the problem of getting confident in the fact that an implementation correctly meets a security policy assigned to it. To do so, we compute tests that exercise security properties issued from the security policy. We proceed by model based testing. Classically, we use a functional model that formalizes the functional specification. But we also use a second model, in the shape of security properties, that formalize a part of the security policy. Tests are computed from the security properties, with the formal functional model as an oracle. We first formalize the informal security requirements as regular expressions. Then we introduce mutations in the regular expressions as to reflect the specific situations in which we intend to test the security properties. These mutated regular expression are unfolded into abstract test sequences. We present a set of four mutation rules that apply to a class of properties that we call sequencing properties , and we experiment our method on a standard in the smart card domain named IAS, for Identification, Authentication and electronic Signature.
During regression testing, a modified system needs to be retested using the existing test suite. Since test suites may be very large, developers are interested in detecting faults in the system as early as possible. Test prioritization orders test cases for execution to increase potentially the chances of early fault detection during retesting. Most of the existing test prioritization methods are based on the code of the system, but model-based test prioritization has been recently proposed. System modeling is a widely used technique to model state-based systems. System models may not only be used to generate test cases but also to prioritize tests. In model-based prioritization, information collected during execution of a model is used to prioritize tests for execution. In this paper we present several model-based test prioritization heuristics. The major motivation to develop these heuristics was simplicity and effectiveness in early fault detection. We have conducted a small experimental study in which we experimentally compared model-based test prioritization heuristics. The results have shown that some simple heuristic methods can be as effective in early fault detection as more complex ones.
A regression test suite (RTS) is constructed to ensure that the changed parts of the system under test (SUT) behave as desired and that the unchanged parts of the SUT are not adversely affected. Model-based testing is a system testing technique in which systems are modeled by formal description languages, e.g., Extended Finite State Machine (EFSM) models. In this paper, a model-based RTS generation method based on EFSM dependence analysis is proposed. Twelve types of dependences are identified related to three types of elementary modifications (EMs), i.e., adding, deleting, and changing transitions in an EFSM model representing an SUT. These dependences capture the effects of the model on the EMs, the effects of the EMs on the model, and the side-effects of the EMs. The proposed method constructs an RTS by covering all occurrences of these dependences caused in a given EFSM model by a given set of EMs.
Interaction testing is widely used in screening for faults. In software testing, it provides a natural mechanism for testing systems to be deployed on a variety of hardware and software configurations. Several algorithms published in the literature are used as tools to automatically generate these test suites; AETG is a well known example of a family of greedy algorithms that generate one test at a time. In many applications where interaction testing is needed, the entire test suite is not run as a result of time or cost constraints. In these situations, it is essential to prioritize the tests. Here we adapt a "one-test-at-a-time" greedy method to take importance of pairs into account. The method can be used to generate a set of tests in order, so that when run to completion all pairwise interactions are tested, but when terminated after any intermediate number of tests, those deemed most important are tested. Computational results on the method are reported.
This paper presents an approach for the automatic generation of shortest Distinguishing Sequences (DS) with the Uppaal model checker. The presented method is applicable to a large number of extended finite state machines and it will find an optimal result, if a DS sequence exists for the considered automaton. Our approach is situated in an integrated testing environment that is used to generate checking sequences. The generation method is based on a DS model, which is derived from the same test model that is used for generating test cover sets. The problem of generating DS is reduced to the definition of a DS model and for this reason the complexity of our approach depends mainly on the used model checking algorithm. This means, that the presented method is automatically improved, when the model checking algorithm is improved. This includes the generation of optimal DS depending on the ability of the model checker to produce optimal results.
