تولید توالی های آزمون با استفاده از اجرای نمادین برای سیستم های رویداد محور زمان واقعی

Real-time software, often used to control event-driven process control systems, is usually structured as a set of concurrent and interacting tasks. Therefore, output values of real-time software depend not only on the input values but also on internal and nondeterministic execution patterns caused by task synchronization. In order to test real-time software effectively, one must generate test cases which include information on both the event sequences and the times at which various events occur. However, previous research on real-time software testing focused on generating the latter information. Our paper describes a method of generating test sequences from a Modechart specification using symbolic execution technique. Based on the notion of symbolic system configurations and the equivalence definitions between them, we demonstrate, using the railroad crossing system, how to construct a time-annotated symbolic execution tree and generate test sequences according to the selected coverage criteria.

Dependable real-time software must produce functionally correct results within the specified time intervals. Validation of real-time software can be particularly difficult since it often consists of cyclic and interacting tasks, exhibiting a large number of nondeterministic execution patterns for a given input set. Formal verification and testing is well-known and complementary software quality assurance approaches. Although formal verification made impressive technical advances to the degree that they are used on large and complex industrial projects [1] and [2], it does not eliminate the need for testing. It is our strong belief that testing will always remain an essential and indispensable component of any software quality assurance program. Many testing techniques have been proposed, but relatively few results are provided for real-time software. Input values alone are sufficient as test cases for sequential software, and input sequences which can exercise a sequence of synchronization are necessary for concurrent software. However, for typical event-driven real-time software, repeated runs using the same input values and sequences do not necessarily follow the identical execution paths and produce the same results. Therefore, both the event sequences and the time of each event occurrence must be included in test cases for real-time software. There are only a few works on the testing of the temporal behavior of real-time systems [3], [4] and [5]. In Ref. [3], a technique for generating test cases from TRIO specification is introduced. It extends the classical temporal logic to deal explicitly with time measures, and TRIO formulas can be automatically checked for satisfiability or validity. During the interpretation of a formula F specifying a property of a system, behaviors of the system compatible with F are generated: they are called histories. These histories are used as test cases. In Ref. [4], a system is modelled with a formally defined SA/SD-RT notation and translated into the time reachability tree for representing the behavior of the system. Each path from the root of the tree to its leaves represents a potential test case. In Ref. [5], a technique for testing timing constraints of real-time systems is presented. A constraint graph is used for describing the various timing constraints the system must satisfy. Timing constraints among various events are shown on the edges of the graph. For example, the constraint graph shown in Fig. 1indicates that the system is initially in the idle state and that the input event BC, indicating the detection of a train approaching the crossing, may occur at an arbitrary and unknown time [0,∞). It also shows that the system is required to generate the output event View the MathML source within 5 time units following the receipt of the BC. Similarly, at an arbitrary time in the future, an input event PASSED is expected to occur. However, the occurrences of the events BC and PASSED must be separated by at least 300 time units. Finally, it is a system requirement to generate the output event View the MathML source within 5 time units following the occurrence of the input event PASSED.Clarke [5] treated the time interval as another input domain and used traditional domain testing technique. While constraint graph-based approach is useful in generating test cases for real-time software, Clarke did not address how constraint graphs can be automatically generated from a formal specification. This paper bridges the gap by illustrating how such task can be accomplished on a Modechart specification [6] (Fig. 2).Some authors have proposed coverage criteria to the problem of testing real-time software [3], [4], [5] and [7]. In Ref. [7], test adequacy criteria based on coverage measures of Petri nets topology for concurrent and real-time systems are presented. Specifically, these criteria are based on firing or transition coverage over Petri nets. In Ref. [3], since the actual test case is a subset of the allowed traces of the system, some heuristic techniques are defined to select a subset of all possible test cases for a given specification. These criteria are based on the constructs of the TRIO specifications. Ref. [4] describes how to restrict test cases according to different coverage criteria because the time reachability graph would become large even for small-scale systems. In this paper, we propose coverage criteria designed to test Modechart specification and discuss how symbolic execution technique can be used to generate test cases. We choose Modechart because it provides a rich set of visual constructs with which one can represent various modes the system components can be in and timing constraints among them. We use symbolic execution technique, which treats the time as symbolic values, for generating test sequences. The notion of symbolic system configuration is defined, and a time-annotated symbolic execution tree (TSET) is generated by symbolically executing Modechart specification. Finally, the test sequences are generated from TSET based on the selected coverage criteria and represented as the constraint graph. The rest of our paper is organized as follows. Modechart specification language is briefly introduced in Section 2. Some coverage criteria of event-driven real-time systems are defined in Section 3, and procedures for constructing TSET are explained in Section 4. We demonstrate, using the railroad crossing system, how to generate constraint graphs. Section 5 concludes the paper.

In this paper, we proposed that various criteria can be defined for event-driven real-time software and that a set of constraint graph can be automatically derived. We used symbolic execution technique for generating the test sequences which include the exact timing intervals for each event. Clarke has previously shown how to generate test cases and test real-time software provided that various and complex timing dependencies have been captured in the constraint graphs. However, his approach failed to describe how accurate constraint graphs can be derived from specification. Our approach, utilizing well-established idea of symbolic execution, nicely complements the work done by Clarke. The combined approach convincingly demonstrates that it is possible to automatically generate test cases for real-time software to meet the specified coverage criteria. We do not claim in this paper that we solved state explosion problem. It is an inherent and fundamental problem all concurrent analysis encounter. For example, TSET would also face state explosion problem as the number of parallel modes and the overlapping intervals in the Modechart increase. However, several large scale industrial systems we have performed case studies on tend not to have complex timing constrains to the degree that test case generation based on the proposed approach would result in state explosion. Examples include digital TV software (800,000+lines of application code alone written in Java and C), shutdown system for a nuclear power plant (7000+lines of Modula code), or satellite controller (3 subsystems and a total of 40,000+lines of C code). Primary factor is that such systems, like most event-driven and time-critical software, require high assurance, and their design tend to be conservative, analyzable, and as simple as possible. Therefore, we feel that in practice, such state explosion problem is not as serious as one may fear. Primary contribution of this paper is not the state explosion problem, but it is the derivation of complex (and sometimes subtle) timing constraints that might not be adequately addressed if test cases are generated manually and informally. Once TSET is built and a set of constraint graphs is generated, one is expected to choose the criteria, one of those proposed in this paper, based on the resource available in testing and level of assurance desired. Modechart specification language provides a rich set of constructs to represent various timing requirements. Timeout is the only feature with one can represent timing requirements in Statecharts. Therefore, our approach can be easily applied to specifications written in Statecharts as well as other variant languages based on the finite state machine concept.