共查询到20条相似文献,搜索用时 31 毫秒
1.
Mercedes G. Merayo Manuel Núez Ismael Rodríguez 《Software Testing, Verification and Reliability》2012,22(8):583-608
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. 相似文献
2.
Robert M. Hierons Mercedes G. Merayo Manuel Núñez 《The Journal of Logic and Algebraic Programming》2009,78(2):98-115
In this paper we present a method for testing a system against a non-deterministic stochastic finite state machine. As usual, we assume that the functional behaviour of the system under test (SUT) is deterministic but we allow the timing to be non-deterministic. We extend the state counting method of deriving tests, adapting it to the presence of temporal requirements represented by means of random variables. The notion of conformance is introduced using an implementation relation considering temporal aspects and the limitations imposed by a black-box framework. We propose a new group of implementation relations and an algorithm for generating a test suite that determines the conformance of a deterministic SUT with respect to a non-deterministic specification. We show how previous work on testing from stochastic systems can be encoded into the framework presented in this paper as an instantiation of our parameterized implementation relation. In this setting, we use a notion of conformance up to a given confidence level. 相似文献
3.
Some systems interact with their environment at physically distributed interfaces called ports and we separately observe sequences
of inputs and outputs at each port. As a result we cannot reconstruct the global sequence that occurred and this reduces our
ability to distinguish different systems in testing or in use. In this paper we explore notions of conformance for an input
output transition system that has multiple ports, adapting the widely used ioco implementation relation to this situation. We consider two different scenarios. In the first scenario the agents at the different
ports are entirely independent. Alternatively, it may be feasible for some external agent to receive information from more
than one of the agents at the ports of the system, these local behaviours potentially being brought together and here we require
a stronger implementation relation. We define implementation relations for these scenarios and prove that in the case of a
single-port system the new implementation relations are equivalent to ioco. In addition, we define what it means for a test case to be controllable and give an algorithm that decides whether this
condition holds. We give a test generation algorithm to produce sound and complete test suites. Finally, we study two implementation
relations to deal with partially specified systems. 相似文献
4.
5.
利用状态转换系统对Z语义模型进行分析。指出其三种不足;然后利用状态转换系统、有限状态转换系统和时序状态转换系统。对Z语义模型分别进行多样性、有效性和时序性扩充,定义多种数据实现关系和时序实现关系,导出相应的求精关系;并通过一个简单的实例说明Z语义模型扩充在多视点需求工程中的应用. 相似文献
6.
Finite State Machines (FSMs) are widely used for verification and testing of many reactive systems and many methods are proposed for generating tests from FSMs with the guaranteed fault coverage. However, some systems can only be properly described when time constraints are considered, advocating the adoption of models with the notion of time. In this paper, a method for deriving conformance tests with the guaranteed fault coverage from a Timed FSM (TFSM) with a single clock is presented. Test derivation is based on a given fault domain that allows the derivation of test suites with reasonable length. More precisely, the fault domain includes every possible faulty TFSM implementation with the known largest time constraints boundaries and minimal duration of time guards. Given a deterministic possibly partial TFSM specification, a complete test suite that guarantees the detection of all faulty implementations with respect to the above fault domain is derived. Experiments with randomly generated timed FSMs are conducted to determine length of obtained test suites and assess the impact of varying the TFSM specification parameters on length of obtained test suites. Further, experiments with both untimed and timed machines are conducted and these experiments show that similar patterns for timed and untimed machines are obtained with respect to varying the number of states, inputs, and outputs of machines. 相似文献
7.
8.
We advocate a fusion of property-oriented testing (POT) and model-based testing (MBT). The existence of a symbolic finite state machine (SFSM) model fulfilling the properties of interest is exploited for property-directed test data generation and to create a test oracle. A new test generation strategy is presented for verifying that the system under test (SUT) satisfies the same LTL safety conditions over a given set of atomic propositions as the model. We prove that this strategy is exhaustive in the sense that any SUT violating at least one of these formulae will fail at least one test case of the generated suite. It is shown that the existence of a model allows for significantly smaller exhaustive test suites as would be necessary for POT without reference models. As a corollary, the main theorem also generalises a known result about SFSM-based conformance testing for language equivalence. Our approach fits well to industrial development processes for (potentially safety-critical) cyber-physical systems, where both models and properties representing system requirements are elaborated for development, verification, and validation. 相似文献
9.
10.
Testing timed systems modeled by Stream X-machines 总被引:1,自引:0,他引:1
Mercedes G. Merayo Manuel N��?ez Robert M. Hierons 《Software and Systems Modeling》2011,10(2):201-217
Stream X-machines have been used to specify real systems where complex data structures. They are a variety of extended finite
state machine where a shared memory is used to represent communications between the components of systems. In this paper we
introduce an extension of the Stream X-machines formalism in order to specify systems that present temporal requirements.
We add time in two different ways. First, we consider that (output) actions take time to be performed. Second, our formalism
allows to specify timeouts. Timeouts represent the time a system can wait for the environment to react without changing its
internal state. Since timeous affect the set of available actions of the system, a relation focusing on the functional behavior
of systems, that is, the actions that they can perform, must explicitly take into account the possible timeouts. In this paper
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. 相似文献
11.
12.
We formalise a specialised database management system model for time series using a multiresolution approach. These special purpose database systems store time series lossy compressed in a space-bounded storage. Time series can be stored at multiple resolutions, using distinct attribute aggregations and keeping its temporal attribute managed in a consistent way.The model exhibits a generic approach that facilitates its customisation to suit better the actual application requirements in a given context. The elements, the meaning of which depends on a real application, are of generic nature.Furthermore, we consider some specific time series properties that are a challenge in the multiresolution approach. We also describe a reference implementation of the model and introduce a use case based on real data. 相似文献
13.
Song Z Ji Z Ma JG Sputh B Acharya UR Faust O 《Computer methods and programs in biomedicine》2012,108(2):656-664
An embedded decision making is a key feature for many biomedical systems. In most cases human life directly depends on correct decisions made by these systems, therefore they have to work reliably. This paper describes how we applied systems engineering principles to design a high performance embedded classification system in a systematic and well structured way. We introduce the structured design approach by discussing requirements capturing, specifications refinement, implementation and testing. Thereby, we follow systems engineering principles and execute each of these processes as formal as possible. The requirements, which motivate the system design, describe an automated decision making system for diagnostic support. These requirements are refined into the implementation of a support vector machine (SVM) algorithm which enables us to integrate automated decision making in embedded systems. With a formal model we establish functionality, stability and reliability of the system. Furthermore, we investigated different parallel processing configurations of this computationally complex algorithm. We found that, by adding SVM processes, an almost linear speedup is possible. Once we established these system properties, we translated the formal model into an implementation. The resulting implementation was tested using XMOS processors with both normal and failure cases, to build up trust in the implementation. Finally, we demonstrated that our parallel implementation achieves the speedup, predicted by the formal model. 相似文献
14.
针对回归测试过程中由于测试需求的变更导致测试用例规模不断扩大、测试成本不断增加的问题,提出一种基于变异分析的测试用例约简方法(RTM)。首先,以测试用例能否检测到指定变异体为依据,对测试用例进行划分并创建二进制数值形式的变异体事务集矩阵;然后,应用改进的关联挖掘算法获取测试用例间的关联关系;最后,根据这些关联关系有效约简测试用例。6个经典程序仿真实验结果表明,RTM能够使约简后的测试用例约简率达到37%,与传统贪心算法和启发式算法相比,测试用例约简率提高了6%,且在提高测试用例约简率的同时,保证了测试覆盖率,单个测试用例的测试覆盖率平均提高了11%。所提方法能够利用尽可能少的测试用例满足更多的测试需求,有效提高了测试效率,降低了测试成本。 相似文献
15.
Modeling and Analysis of Workflows Using Petri Nets 总被引:37,自引:0,他引:37
Nabil R. Adam Vijayalakshmi Atluri Wei-Kuang Huang 《Journal of Intelligent Information Systems》1998,10(2):131-158
A workflow system, in its general form, is basically a heterogeneous and distributed information system where the tasks are performed using autonomous systems. Resources, such as databases, labor, etc. are typically required to process these tasks. Prerequisite to the execution of a task is a set of constraints that reflect the applicable business rules and user requirements.In this paper we present a Petri Net (PN) based framework that (1) facilitates specification of workflow applications, (2) serves as a powerful tool for modeling the system under study at a conceptual level, (3) allows for a smooth transition from the conceptual level to a testbed implementation and (4) enables the analysis, simulation and validation of the system under study before proceeding to implementation. Specifically, we consider three categories of task dependencies: control flow, value and external (temporal).We identify several structural properties of PN and demonstrate their use for conducting the following type of analyses: (1) identify inconsistent dependency specifications among tasks; (2) test for workflow safety, i.e. test whether the workflow terminates in an acceptable state; (3) for a given starting time, test whether it is feasible to execute a workflow with the specified temporal constraints. We also provide an implementation for conducting the above analyses. 相似文献
16.
An approach to the problem of complete testing is proposed. Testing is interpreted as the check of an implementation’s conformance
to the given requirements described by a specification. The completeness means that a test suite finds all the possible implementation
errors. In practice, testing must end in a finite amount of time. In the general case, the requirements of completeness and
finiteness contradict each other. However, finite complete test suites can be constructed for certain classes of implementations
and specifications provided that there are specific test capabilities. Test algorithms are proposed for finite specifications
and finite implementations with limited nondeterminism for the case of open-state testing. The complexity of those algorithms
is estimated. 相似文献
17.
Gordon Fraser Angelo Gargantini Franz Wotawa 《The Journal of Logic and Algebraic Programming》2009,78(6):472-490
Model-based testing techniques often select test cases according to test goals such as coverage criteria or mutation adequacy. Complex criteria and large models lead to large test suites, and a test case created for one coverage item usually covers several other items as well. This can be problematic if testing is expensive and resources are limited. Therefore, test case generation can be optimized in order to avoid unnecessary test cases and minimize the test generation and execution costs. Because of this optimization the order in which test goals are selected is expected to have an impact on both the performance of the test case generation and the size of resulting test suites, although finding the optimal order is not feasible in general. In this paper we report on experiments to determine the effects of the order in which test goals are selected on performance and the size of resulting test suites, and evaluate different heuristics to select test goals such that the time required to generate test suites as well as their size are minimized. The test case generation approach used for experimentation uses model checkers, and experimentation shows that good results can be achieved with any random ordering, but some improvement is still possible with simple heuristics. 相似文献
18.
19.
《Information and Software Technology》2012,54(7):724-738
ContextTest suite reduction is the problem of creating and executing a set of test cases that are smaller in size but equivalent in effectiveness to an original test suite. However, reduced suites can still be large and executing all the tests in a reduced test suite can be time consuming.ObjectiveWe propose ordering the tests in a reduced suite to increase its rate of fault detection. The ordered reduced test suite can be executed in time constrained situations, where, even if test execution is stopped early, the best test cases from the reduced suite will already be executed.MethodIn this paper, we present several approaches to order reduced test suites using experimentally verified prioritization criteria for the domain of web applications. We conduct an empirical study with three subject applications and user-session-based test cases to demonstrate how ordered reduced test suites often make a practical contribution. To enable comparison between test suites of different sizes, we develop Mod_APFD_C, a modification of the traditional prioritization effectiveness measure.ResultsWe find that by ordering the reduced suites, we create test suites that are more effective than unordered reduced suites. In each of our subject applications, there is at least one ordered reduced suite that outperforms the best unordered reduced suite and the best prioritized original suite.ConclusionsOur results show that when a tester does not have enough time to execute the entire reduced suite, executing an ordered reduced suite often improves the rate of fault detection. By coupling the underlying system’s characteristics with observations from our study on the criteria that produce the best ordered reduced suites, a tester can order their reduced test suites to obtain increased testing effectiveness. 相似文献
20.
Jan Hendrik Hausmann Reiko Heckel Stefan Sauer 《Electronic Notes in Theoretical Computer Science》2003,72(3):133-144
UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams. 相似文献