extfieldsofstudy:
Computer Science
Engineering

text:
Minimal TestCase Generation for Object-Oriented Software with State Charts

Today statecharts are a de facto standard in industry for modeling system behavior. Test data generation is one of the key issues in software testing. This paper proposes an reduction approach to test data generation for the state-based software testing. In this paper, first state transition graph is derived from state chart diagram. Then, all the required information are extracted from the state chart diagram. Then, test cases are generated. Lastly, a set of test cases are minimized by calculating the node coverage for each test case. It is also determined that which test cases are covered by other test cases. The advantage of our test generation technique is that it optimizes test coverage by minimizing time and cost. The present test data generation scheme generates test cases which satisfy transition path coverage criteria, path coverage criteria and action coverage criteria. A case study on Railway Ticket Vending Machine (RTVM) has been presented to illustrate our approach.

INTRODUCTION
With continually increasing system sizes, the issue of automatic design of system test cases is assuming prime importance [28]. A properly generated test suite may not only locate the errors in a software system, but also help in reducing the high cost associated with software testing [17]. Many present day software solutions are state based. In such systems, the system behavior is determined by its state. In other words, a system can respond differently to the same event in different states. Therefore, unless a system is made to assume all its possible states and tested, it would not be possible to uncover state-based bugs. Adequate system testing of such software requires satisfactory coverage of system states and transitions. Generation of test specifications to meet these coverage criteria can be accomplished by using the state model of a system. However, it is a non-trivial task to manually construct the state model of a system. The state model of an actual system is usually extremely complex and comprises of a large number of states and transitions. Possibly for this reason, state models of complete systems are rarely constructed by system developers [28].
Testing of object-oriented software is a traditional activity that is part of the process of software quality assurance. Model-based testing technique has grown its importance. The models used represent the relevant features of the system under tests (SUT), and can also be used as a basis for generating test cases. The time and required effort to do sufficient testing grow, as the size and complexity of the software grows. Typical models that are used for representing system behavior are for instance the unified modeling language, finite state machines and state charts. Testing can be carried out earlier in the development process so that the developer will be able to find the inconsistencies and ambiguities in the specification. Hence it will be able to improve the specification before the program is written [12]. Testing activities consist of designing test cases that are sequences of inputs, executing the program with test cases, and examining the results produced by this execution. Unified modeling language (UML) has emerged as the de facto standard for modeling software systems and has received significant attention from researchers as well as practitioners.
UML models are popular not only for designing and documenting systems, the importance of UML models in designing test cases has also been well recognized. Even though UML models are intended to help reduce the complexity of a problem, with the increase in product sizes and complexities, the UML models themselves become large and complex involving thousands of interactions across hundreds of objects [16]. The important part of quality control in the software life-cycle is testing. As the complexity and size of software increase, the time and effort required to do sufficient testing grow. Manual testing is timeconsuming and error-prone. So, there is a pressing to automate the testing process. The testing process can be divided into three parts: test case generation, test execution, and test evaluation. The latter two parts are relatively easy to automate provided that the criteria for passing the tests are available. However, to determine which tests are required to achieve a certain level of confidence is not trivial [18]. Model-based testing [6] has grown in importance. Models are specified to represent the relevant, desirable features of the system under consideration (SUC). These models are used as a basis for (automatically) generating test cases to be applied to the SUC. Typical models that are used for representing system behavior are unified modeling language, finite state machines, statecharts etc. [4]. It is often desired that test data in the form of test sequences within a test suite can be automatically generated to achieve required test coverage. It helps mankind to save on time, money and helps in handling better situations in real time.
With this motivation, we aim our work at deriving the test sequence from state transition diagram and maximizing state or node coverage. Also our method minimizes the size of test, time and cost, while preserving test coverage. The rest of the paper is structured as follows: A brief discussion on UML diagrams, which are relevant to our paper is described in the Section 2. Then, we discuss some testing coverage criteria in Section 3. Section 4 represents some concepts, notations and definitions of state chart diagram. In Section 5, we explain the overview of our proposed method for construction of state-transition graph, generation of test sequence using state charts and how node coverage is calculated for each test case. Section 6 provides the working of our methodology with the RTVM (Railway Ticket Vending Machine) case study and implementation of our example. Section 7 discusses some comparison with related work. Finally, Section 8 presents the conclusion and future work of this paper.

AN OVERVIEW OF RELEVANT UML 2.0 DIAGRAMS
In this section, we discuss an overview of the UML diagrams, which will be used subsequently in our paper. UML is a modeling language using text and graphical notation and used for documenting specification, analysis, design, and implementation. It is a de-facto standard in industrial software development UML, Unified Modelling Language is a visual language that has been developed to support the design of complex object-oriented systems. Since its introduction in the late 90s, it has undergone several revisions. The latest release being UML version 2.0, which adds several new capabilities to UML 1.x. In this section, we restrict our review to only those developments that are directly relevant to our work. A typical software procedure incorporates all the three aspects: It uses data structure (class model), it sequences operations in time (state model), and it passes data and control among objects (interaction model). The three kinds of models separate a system into different views. The different models are not completely independent but a system is more than a collection of these independent parts. UML specification defines two major kinds of UML diagram: structural diagrams and behavioral diagrams. The elements in a structural diagram represent the meaningful concepts of a system, and may include abstract, real world and implementation concepts. Behavioral diagrams show the dynamic behavior of the objects in a system, which can be described as a series of changes to the system over time.

UML state chart diagram
In this section, we explain the few fundamentals on state chart diagram. The name of the diagram itself clarifies the purpose of the diagram and other details. It describes different states of a component in a system. The states are specific to a component or object of a system. A statechart diagram describes a state machine. Now to clarify it state machine can be defined as a machine which defines different states of an object and these states are controlled by external or internal events. Statechart diagram is one of the five UML diagrams used to model dynamic nature of a system. They define different states of an object during its lifetime. And these states are changed by events. So, Statechart diagrams are useful to model reactive systems. Reactive systems can be defined as systems that respond to external or internal events. Statechart diagram describes the flow of control from one state to another state. States are defined as a condition in which an object exists and it changes when some event is triggered. So, the most important purpose of Statechart diagram is to model life time of an object from creation to termination. Statechart diagrams are also used for forward and reverse engineering of a system. But the main purpose is to model reactive system. State diagrams are used to give an abstract description of the behavior of a system. This behavior is analyzed and represented in series of events, that could occur in one or more possible states. Hereby "each diagram usually represents objects of a single class and track the different states of its objects through the system". State diagrams can be used to graphically represent finite state machines. Followings are the main purposes of using statechart diagrams: (a) To model dynamic aspect of a system, (b) To model life time of a reactive system and (c) To describe different states of an object during its life time.   The fundamental components of a state chart diagram are -events, states and transitions. But it has some distinguishing characteristics for modeling dynamic nature. State chart diagram defines the states of a component and these state changes are dynamic in nature. So, its specific purpose is to represent the state changes triggered by events. Events are internal or external factors influencing the system. If we look into the practical implementation of Statechart diagram then it is mainly used to analyze the object states influenced by events. This analysis is helpful to understand the system behavior during its execution. The following are the basic notational elements that can be used to make up a diagram: 2.1.1. State: The state of an object is shown by rectangle with rounded corners. Top of the rectangle contains a name of the state. It can contain a horizontal line in the middle, below which the activities that are done in that state are indicated. A state in a state chart diagram can either be simple or composite type. A simple state does not have any sub-states.

Initial state:
A transition leading from an initial event shows the state that an object goes into when it is created or initialized. This is shown as a small black disk or filled circle. A statechart can have only one initial state.

Final state:
Like initial state the state diagram shows final state. It represents the state reached when an object is destroyed, switched off or stops responding to events. This is shown as a hollow circle containing a smaller filled circle or small black disk within a large circle. A state-chart may have more than one final state [24].

Transition:
Arrows, denote transitions. The name of the event (if any) causing this transition is written as the labels with the transition names or event names. A guard expression may be added before a "/" and enclosed in square-brackets ( eventName[guardExpression] ), denoting that this expression must be true for the transition to take place.

An event:
We call the event that causes the state transition the trigger. An event is an occurrence at a point of time. Events often correspond to verbs in the past tense e.g. (power turned on, alarm set) [5]. There are four types of events that can trigger a state transition: Signal event (when the system receives a signal from an external agent)

Call event (when a system operation is invoked) Timing event (when a timeout occurs)
Change event (when a system property is changed by an external agent) 2.1.6. Choice and Junction Points: A choice point allows a transition to branch to several different states depending on the value of a guard. A junction point indicates that several states can transition to the same state on a given event.

SOME BASIC DEFINITIONS
Here, in this section, we introduce a few basic concepts and definitions which we use while describing our aproach in the subsequent sections. There are many forms of state diagrams, which differ slightly and have different semantics. For a deterministic finite state machine (DFA), nondeterministic finite state machine (NFA), generalized nondeterministic finite state machine (GNFA), Mealy machine or Moore machine, the input is denoted on each edge. For a Mealy machine, input and output are signified on each edge, separated with a slash "/": "1/0" denotes the state change upon encountering the symbol "1" causing the symbol "0" to be output. For a Moore machine the state"s output is usually written inside the state"s circle, also separated from the state"s designator with a slash "/". There are also variants that combine these two notations.
It is assumed that a state chart STc is correct in the sense that for each state s ∈ S simple there exists a sequence of transitions t 1 , t 2 ..., t k so that source(t 1 ) ∈ Si and target(t k ) = s and for each state s ∈ S simple there exists a sequence of transitions t 1 , t 2 ..., t k so that source(t 1 ) = s and target(t k ) ∈ S f . The following terms will be used to describe our technique.

Definition 1.
A statechart can be a quadruple S c = (E, S t , H, T), where E is a finite set of events and St = (S, S i , S f ) is a triple of set of states with S as a finite set of states, S i ⊆ S denoting the entries (initial states) and S f ⊆ S the exits (final states), H ⊆ S × S is a hierarchy relation, a binary relation on the set S forming a tree. For an element (s, s′ ) ∈ H holds, that a state s is an immediate sub state of state S′.
T ⊆ S × E × S is a finite set T of transitions. The set of states S is composed of disjoint sets of simple states S simple and composite states S comp .

Scenario-intermediate state:
A scenario is executed, when the system is at a state (Si) may cause the system to transit from its current state (Si) to a next state (Sj ). Since a scenario may consist of a number of message exchanges among objects, a system may even change its state during the execution of a step (a message) in a scenario. Hence, execution of a single scenario may cause traversal of several states and transitions. All system states other than Si and Sj , through which the system transits during the execution of a scenario are considered to be scenariointermediate state. We can say, execution of a scenario may cause a system to transit from one state to another state, and all other intermediate states reached during execution of the scenario are scenario-intermediate states. It may be important that a scenario-intermediate state reached during execution of a scenario can also be a normal state, if it is either the initial or final state for execution of some scenario. Definition 2. A transition pair TP = (t, t′ ) with t, t′ belongs to T legal is a sequence of a legal incoming transition to a legal outgoing transition of a (simple) state so that ∃ s ∈ S simple : t ∈ in(s) U t′ ∈ out(s).

Definition 3.
A false transition pair FP = (t, t′ ) with t ∈ T legal and t ′ ∈ T faulty is a sequence of a legal incoming transition to a faulty outgoing transition of a (simple) state so that ∃ s ∈ S simple : t ∈ in(s) U t′ ∈ out(s).
denotes a valid transition pair for all i ∈ 1, ..., n -1 is called a transition sequence (T seq ) of length n. A transition sequence (t 1 , t 2 ..., t n ) is complete if it starts at the initial state of the state chart that is entered firstly and ends at a final state. In this case it is called a complete transition sequence (T sqcom ).

Definition 5.
A fault transition sequence T sqfault = (t 1 , t 2, ..., t n ) of length n consists of n -1 subsequent transitions, forming a (legal) transition sequence of the length n -1 plus a concluding, faulty transition t n ∈ T faulty . A faulty transition sequence is called complete if it starts at the initial state of the statechart, abbreviated as CFTS. The sequence (t 1 , t 2, ..., t n-1 ) is called a start sequence.

Definition 6.
A test case is the triplet [I, S, O], where I is the initial state of the system at which the test data is input, S is the test data input to the system and O is the expected output of the system [18], [19]. The output produced by the execution of the software with a particular test case provides a specification of the actual software behavior. A test case is also characterized by an ordered pair of an input and an expected output of the SUC.

Definition 7.
A test suite is a set of test cases. A single test case in most cases may satisfy more than one test obligation. For instance, a test case used to cover a certain state of interest may also cover other states during its execution. This then provides for a way to reduce the size of the final test suite by choosing a subset of test cases that preserves the coverage obtained by the full test suite [9]. Definition 8. k-transition coverage (k-TC) generates complete transition sequences that sequentially conduct all legal transition sequences of length k ∈ N.

Definition 9.
A single test case in most cases may satisfy more than one test obligation. For instance, a test case used to cover a certain state of interest may also cover other states during its execution. This then provides for a way to reduce the size of the final test suite by choosing a subset of test cases that preserves the coverage obtained by the full test suite [10]. A test suite is a set of test cases. Definition 8 guarantees that all possible (legal) transition sequences of length k will be tested. A test suite consisting of all transition sequences of a fixed length k does not necessarily cover a set of all sequences of length i ∈ 1, ... , k-1 as there may exist sequences of length i that cannot be expanded to length k. Typically, state based test generation methods focus on some form of coverage, for instance on covering transitions [19], [20] or on transition coverage and state identification [6], [14]. Our approach creates all transition sequences of length k including all shorter sequences of length 1, ..., k -1 that cannot be found in longer sequences.

TEST ADEQUECY CRITERIA
Typically, state based test generation methods focus on some form of coverage, for instance on covering transitions [20], [21] or on transition coverage and state identification [7], [15]. Our approach creates all transition sequences of length k including all shorter sequences of length 1, ..., k -1 that cannot be found in longer sequences. Testing coverage/adequacy criterion specifies the requirement of a particular testing and can be used as an objective measurement of the test case. In traditional software code testing, the definition of testing adequacy is defined as a measurement function. The case of UML state chart diagrams is different because it is in the form of model instead of code. Especially the coverage of state chart diagram is little bit complex. In our paper, we propose different types of coverage metrics as follows: State Coverage Criterion : The value of state coverage is the ratio between the covered states and all the states in the statechart diagram. It requires that all the state nodes in a state chart graph to be covered at least once. Action Coverage: To generate test cases with respect to action coverage we construct as many marked specifications as there are actions within the specification.
Transition Coverage : Given a graph and a test suite TS, s is said to achieve transition coverage, if it causes each transition t of the state graph to be exercised at least once. The value of transition coverage is the ratio between the checked transitions and all the transitions in the statechart graph.
Transition Path Coverage: Given a graph and a test suite TS, s is said to achieve transition path coverage, if it causes each elementary transition path p of the state graph to be exercised at least once. The value of path coverage is the ratio between the traversed paths and all the paths in the graph.

Condition coverage.
A single condition is covered, if it evaluates to both true and false at some point during test execution. Decision coverage has also been called branch coverage or predicate coverage. This means that 100% condition/decision coverage is achieved if all conditions evaluate to true and to false and if every decision also evaluates to true and to false during the test execution. A decision consists of conditions separated by logical operators (e.g. and, or).

TEGEMIOOSC-OUR PROPOSED APPROACH TO GENERATE AND MINIMIZE TEST SEQUENCE WITH STATECHARTS
In this section we discuss the overview of our proposed approach to generate test sequence from UML state chart diagram and then, we optimize the test node coverage while minimizing time and cost. We have named our approach, Test Generation and Minimization for O-O software with State Charts (TeGeMiOOSc). The schematic representation of our approach is shown in Figure. 2. Our proposed methodology involves the following steps.
Step-1. Analyze the real system which is to be tested and accepted by user.
Step-2. Construct State Chart Diagram Step-3. Convert the given State Chart Diagram into an intermediate graph. We named this intermediate graph a state transition graph.
Step-4. Starting from the first node, traverse remaining nodes, using DFS concept, in order to form test sequence.
Step-5. Obtain all the valid sequences of the application until final edge is reached.
Step-6. Minimize a set of test cases by calculating node coverage for each test sequence.
In the next Section, we discuss each step in detail, by using different algorithms for each step in different sections. Before that, we present some related definitions. In the next section, we discuss each step in detail, by using different algorithms for each step in different sections. Before that we present some related definitions.

Analyze the real system which is to be tested
A Railway Ticket Vending System (RTVM) dispenses tickets to passengers at a railway station. passengers use the front panel to specify their Boarding and destination place, details of passengers(number of adults and children) and date of travel. The machine displays the fare for the requested ticket. The passengers deposits cash in the bin provided and presses "accept cash". The machine checks the cash, if it is more; the balance cash is paid out. And the ticket requested is printed. And the report options also include the detailed report of transactions, summary report of the number of tickets sold for each destination, opening balance, each collected, cash dispensed and current balance in the machine. The total functionalities are shown by the use case diagram as shown in Fig. 3.

Construct the model of the SUT using state chart diagram
State chart diagram is a graph where nodes represent states end the directed arcs that interconnect states represent transitions. It also models dynamic behavior, and captures the different states that an object can be in, and its response to various events that may arise in each of its states. Statechart diagram is one of the 13 UML diagrams used to model dynamic nature of a system. They define different states of an object during its lifetime. The notation and semantics of UML state diagrams are substantially based on Statecharts modified to include object-oriented features [13]. The states and the transition of a system are important to set up a state diagrams from system. Fig. 4 shows a UML state diagram for a railway ticket vending machine system.

Convert the state chart diagram into state transition graph
Here, we convert the state diagram into state transition graph. A state transition graph TG = (V t , E d ).

Definition 10:
A transition graph TG = (V t , E d ) represents a directed graph consisting of a set of vertices (V t ), a set of directed edges (E d ). In TG, nodes represent states and edges represent transitions between states. Without any loss of generality, we assume that there is a unique node that corresponds to the initial state and that one or more nodes represent the final states. The initial state is represented as the root of the tree. States at each level of nesting are considered as a sub graph. We represent this step through an algorithm. connected with all transitions that may be triggered from the state belonging to the initial configuration. Transitions leading into a final state have to be connected with vertex tj . A simple transition coverage may be reached by visiting all vertices of the graph, based on a transition graph at least once by starting in vertex ti and ending in vertex tj . The problem of computing a route for visiting all vertices of a graph by minimizing the length of the route is well known as the traveling salesman problem (TSP). If visiting vertices and traversing edges more than once is allowed, it is called the graphical traveling salesman problem (GTSP) [25]. Also, by computing all complete transition sequences whose length is smaller than k and that cannot be expanded to longer sequences, a minimal test case set fulfilling k-transition coverage for all k ∈ 1, . . . , n is achieved. This procedure is described in Algorithm-1, in the next section.

Generating test cases
After, a transition graph is constructed based on a state chart Sc. If n = l, the graphical traveling salesman problem can be applied directly. If n is greater than 1 the transition graph has to be transformed k -1 times. The resulting graph represents all possible sequences of transitions of length k. Additionally, all sequences of length k-1 are computed that cannot be expanded to longer sequences. These sequences are characterized by the fact that the corresponding vertex representing that sequence is solely connected with vertices t i and t j. The functions indeg(v) := v′,(v′, v) ∈ A and outdeg(v) := v′(v, v′) ∈ A are used to compute these vertices. As these sequences are already complete, they can be added to the set TS.

14.
For k := 2 to n do

Minimizing the test cases
Here, in this section , we discuss how the generated test cases are reduced while maximizing test coverage. Though Wang"s algorithm [17] is widely used, but it does not cover other critical attributes, like defect id, dependency and automated test case indicator. In order to generate an effective size of generated test cases, this step contains two sub activities, which are calculate node coverage for each test case. Let NC(tc) = t 1 , t 2 ,...t n for NC(tc) to be a set of test cases that tc is covered by t 1 , t 2 ,...t n . Hence, if a number of testset tc is zero, then tc is included in the effective set of test cases. select effective test cases. Now, we present this step through an algorithm. Now, we select the effective testcases, which contains no testset. We present this step through an algorithm.

Problem statement
Buying ticket in RTVM (Railway Ticket Information Systems) is a system which receives the cash from the customer and returns back the balance and the ticket. The system has five components: Front panel, Ticket Transacter, Cash Transacter, Cash Handler and Ticket. Entire functions of the system are represented in the form of a usecase diagram. The customer deposits the cash. The system then passes the cash deposit intimation to ticket transacter. The ticket transacter then accepts cash and passes it to cash transacter and the cash transacter then transacts the cash to the cash handler. After receiving the cash, the cash handler sends an acknowledgment to the cash transacter. The cash transacter gives cash confirmation acknowledgement to the ticket transacter and also gives the balance amount to cash transacter. The cash transacter sends the acknowledgment for the cash received to the ticket transacter. Finally the ticket transacter prints the ticket with the help of ticket component and issues the ticket to the customer. The state diagram for the buy ticket in RTVM system is shown in Fig.  4.
Here, the object enters into idle state, when the power switch is on. Once the user selects a tickettype button in the menu, the object enters the ticketselected state. The user can select the destination, ticket type and the number of persons (n) to travel. The condition n ≤ 6 is inserted for the event tickettypeselected, as the ticket machine is not expected to issue a ticket for more than 6 persons in one transaction. Once the ticket type and number of persons required are selected, the object enters the collectmoney state. In this state, the object collects the amount of money (totalfair) the user has to enter into the ticket machine. Note that totalfair = ticket fare × number of persons. As the user inserts money (amount) into the machine, the machine object changes its state to busy. In the busy state, it calculates how much balance or change (chng) has to be returned to the user if any, where chng = (amount -totalfair). If the change balance is less than zero, the machine object changes its state again from busy to collectmoney as the money inserted is insufficient. If the change balance is equal to zero, the machine object goes to exactlypaid state and dispenses the ticket for requested number of persons. If the change balance is more than zero, then the machine object changes its state to overpaid state and then dispenses ticket as well as dispenses change. After constructing state chart diagram, we construct transition graph as shown in Fig 5. In next step, we traverse the graph and extract all required information from the state transition graph as described below.

Working Of the proposed Algorithm
The state model application saved as .mdl file is provided as input to the parser. The parser analyses and collects all the information about object states, actions / guards and transitions, which are represented as nodes and edges in a directed graph as shown in Fig. 5. In Table I, we represent the mapping of object states to its corresponding nodes in the graph and Table II shows actions or guard conditions to corresponding edges in the graph. Then, by using traversal algorithm we find all possible test sequences generated and are shown in Table III.  TABLE I  MAPPING INFORMATION TABLE FOR OBJECT STATES   Hence, the set of states are ST = {IN, IDL, TS, CM, OP, EP}, each ST i is a state or node  ID = {ID 1 , ID 2 , ID 3 , ID 4 , ID 5 , ID 6 }, each ID i is an input data OD = {OD 1 , OD 2 , OD 3 , OD 4 , OD 5 , OD 6 }, each OD i is an output value TR = {TR 1 , TR 2 , TR 3 , TR 4 , TR 5 , TR 6 , TR 7 }, each TR i is a transition between source and destination state, where each TR i = {ST p , ST q }, STp is a source state and ST q is a destination state. Hence, each transition can be extracted as follows:   Table IV.   TABLE III  TESTCASE GENERATED TABLE FOR RTVM

Implementation
In this section, we present some experimental results in order to verify the effectiveness of our approach. We have carried out a series of experiments. In our experiments we have considered different types of applications. All these systems are designed in UML 2.0 using Rational Rose Sostware. Here, we consider the example of Railway Ticket Vending Machine (RTVM). We can experiment with other applicatins namely Library Information System (LIS), Cell Phone System (CPS), Trading House Automation System (TAS) etc. First, the usecase diagram of RTVM is modelled using RationalRose software. then considering only the Purchase Ticket or Buy ticket usecase, we model it with State chart diagram and saved with .mdl extension. Next, the state chart diagram is converted into state chart graph. Now, the statechart graph is traversed applying DFS technique, considering pre and post conditions. Then, the graph is transformed into the sourcecode in JAVA. Hence, the designs are also implemented using JAVA and NetBeans IDE version 7.1.2. The screenshot of our Java sourcecode is shown in Fig.6. We have implemented our approach by using ModelJunit tool. ModelJUnit [1] is a Java library that extends JUnit to support model-based testing. It allows us to write simple FSM or EFSM models as Java classes, then generate tests from those models and measure various model coverage metrics. System models are extended finite state machines that are written in a familiar and expressive language: JAVA. ModelJUnit is an open source tool, which is released under the GNU GPL license. ModelJUnit is an openly available test case generation tool, using an extended finite state chart diagram. ModelJUnit searches the graph of an EFSM at runtime. It generates EFSM (Extended Finite State Machine) from source code. The screenshot of the generated EFSM for different conditions are shown in Fig. 7. EFSM models are graphically represented as graphs where states are represented as nodes and transitions as directed edges between states.

Figure. 7. EFSM generated for different conditions
The source and destination states as well as the prefix path conditions are displayed along with the test data. In our implementation, we have restricted the conditional expressions in state diagrams to have only integer and Boolean variables as these occur commonly. The GUI provides a friendly and efficient user interface to user to generate testing code and shows test coverages as shown in Fig. 8.

Figure 8. Test coverage through our implementation
We have implemented the sytem model by providing several inputs. Fig. 9

Test Reduction
There is hardly sufficient time for thorough testing activities within industrial projects, in practical situations. Hence, it is reasonable to try to reduce the size of generated test suites. However, the effect of the reduction on the fault detection ability of the test suites should be small. The techniques proposed in our paper can be used to apply reduction during test case generation. A single test case may cover more than the coverage item it has been generated for. When using a probe based technique as described in our paper it is easy to identify all items covered by a particular test case.

COMPARISON WITH RELATED WORK
A lot of research work have been investigated the effect of testset reduction on the size and fault finding capability of a test-set. In an early study, Wong et al. address the question of the effect on fault detection of reducing the size of a test set while holding coverage constant [29], [30]. They randomly generated a large collection of test sets that achieved block and all-uses data flow coverage for each subject program. For each test set they created a minimal subset that preserved the coverage of the original set. They then compared the fault finding capability of the reduced test-set to that of the original set. Their data shows that test minimization keeping coverage constant results in little or no reduction in its fault detection effectiveness. This observation leads to the conclusion that test cases that do not contribute to additional coverage are likely to be ineffective in detecting additional faults.
To confirm or refute the results in the Wong study, Rothermel et al. performed a similar experiment using seven sets of C programs with manually seeded faults [26]. For their experiment they used edge-coverage [8] adequate test suites containing redundant tests and compared the fault finding of the reduced sets to the full test sets. In this experiment, they found that [3] the fault-finding capability was significantly compromised when the test-sets were reduced and [27] there was little correlation between test-set size and fault finding capability. The results of the Rothermel study were also observed by Jones and Harrold in a similar experiment [11].
Prasanna M, et al. [23] proposed a technique for generating test cases using collaboration diagrams. They converted the diagram into an intermediate graph and from the graph, by applying Prim"s and Dijkstra"s algorithm, generated a set of test cases.
Offutt and Abdurazik [20], [21] proposes a technique for generating test cases from UML state diagrams. They have highlighted several useful test coverage criteria for UML state charts such as: (1) full predicate coverage, (2) transition coverage etc.
Kansomkeat and Rivepiboon [12] introduce a method for generating test sequences using UML state chart diagrams. They transformed the state chart diagram into a flattened structure of states called testing flow graph (TFG). From the TFG, they listed possible event sequences which they considered as test sequences. The testing criterion they used to guide the generation of test sequences is the coverage of the states and transitions of TFG.
Kim et al. [13] proposes a method for generating test cases for class testing using UML state chart diagrams. They transformed state charts to extended FSMs (EFSMs) to derive test cases. In the resulting EFSMs, the hierarchical and concurrent structure of states are flattened and broadcast communications are eliminated. Then data flow is identified by transforming the EFSMs into flow graphs, to which conventional data flow analysis techniques are applied.
In the experiment discussed in our paper, we attempt to highlight some additional issues. These different results are difficult to reconcile and the relationship among coverage criteria, testsuite size, and fault finding capability clearly needs more study.
Our work is different in some respects. First, we are not studying testing of traditional programs. We generate testcases for object oriented software. we are interested in test case generation as well as testcase minimization by calculating node coverage for each test case and testing of specifications. A single test-case in most cases may satisfy more than one test obligation. For instance, a testcase used to cover a certain state of interest may also cover other states during its execution. It provides a way to reduce the size of the final test-suite by choosing a subset of test-cases that preserves the coverage obtained by the full testsuite.

CONCLUSSION AND FUTURE WORK
In our approach, first, we built a state chart model of our system under test. Next, we derived state transition graph from state chart diagram. Then, all required information are extracted from the graph. Next, the test cases are generated by our algorithm. Lastly, a set of test cases are minimized by calculating node coverage for each test case. It is determined that which test cases are covered by other test cases. In this way, our paper introduces an efficient test generation approach to optimize the test coverage by minimizing time and cost. In our opinion, there is almost no degradation in terms of testsuite quality.
Further, we plan into testcase generation techniques by using any other UML diagram such as activity diagram. Experimental studies required to determine if such techniques can more reliably reduce the burden of the testing effort.


extfieldsofstudy:
Mathematics
Computer Science

text:
The size of a formula as a measure of complexity

We introduce a refinement of the usual Ehrenfeucht-Fra\"{\i}ss\'e game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure the size formulas needed for expressing a given property. We will give two versions of the game: the first version characterizes the size of formulas in propositional logic, and the second version works for first-order predicate logic.

Introduction
We propose a refinement of the usual Ehrenfeucht-Fraïssé game. The new game will help us make finer distinctions than the traditional one. In particular, it can be used to measure not only quantifier rank but also lengths of conjunctions and disjunctions needed for expressing a given property. Our game is similar to the game in [1] and in [5].
The most common measure of complexity of a first order sentence is its quantifier rank, and the method of Ehrenfeucht-Fraïssé games can be successfully used to prove lower bound results for this measure of complexity. However, the number of non-equivalent first order formulas of quantifier rank n is an exponential tower of height n with a polynomial depending on the vocabulary on the top. Thus we are not very close to knowing the formula if we merely know its quantifier rank. In this paper we measure complexity in terms of the number of symbols in the formula. The advantage of our measure is that there are only 2 P (n) non-equivalent formulas with n symbols, where P (x) is a polynomial depending on the vocabulary.
Let us consider the question of the complexity of deciding whether a binary string s 1 s 2 . . . s n = 10110010...01 (1) has a certain pattern. One approach to this is circuit complexity. For example, it is proved in [3] that constant depth circuits cannot decide the parity of (1), i.e. the question whether (1) has an even number of ones. Another approach is computational complexity, where the parity of (1) is easily decided in linear time. In so called descriptive complexity the question is posed, what is the logical complexity of the simplest formula in a given logic that expresses the property of (1) in question, for example parity. Concerning this type of problems, it was proved in [2] that the question whether a set R of n + 1-sequences (a 1 , . . . , a n+1 ) from a finite set {1, . . . , m} has an even cardinality cannot be expressed in existential second order logic, where the second order variables range over ≤ n-ary relations, that is, there is no sentence φ of such existential second order logic with the property that the structure ({1, . . . , m}, R) satisfies φ if and only if R has even cardinality. Let us return to (1). A natural setup of using logic to study the question of complexity of finding patterns in (1) is to use the propositional logic with propositional symbols p 1 , p 2 , . . . , p n with the meaning p i is true if and only if s i = 1.
Propositional logic gives rise to a variety of complexity measures. We focus here on the simplest of them, namely the number of occurrences of propositional symbols in a formula. Up to a constant factor this is the same as the number of symbols, that is, the length of the formula. The parity of (1) is naturally expressed by the propositional formula where which gives the upper bound 1 2 n2 n to the size of the smallest formula expressing parity. However, there is a shorter formula ψ defined as follows: ψ = φ 1,n , where for 1 ≤ i < j ≤ n and k = ⌊ i+j 2 ⌋ φ i,j = (φ i,k ∧ φ k+1,j ) ∨ (¬φ i,k ∧ ¬φ k+1,j ) and This gives (up to a constant factor) the upper bound n 2 for the shortest propositional formula expressing parity 1 . Krapchenko (see [6, p 258]) has proved in 1971 that this is optimal. We prove below the same result using our refinement of the Ehrenfeucht-Fraïssé game. For a slightly different complexity question, suppose we have n unary predicates: P 1 (x), . . . , P n (x).
We ask what is the length of the shortest formula in first order logic with the unary predicates (7) that expresses the property that every Boolean combination of the predicates is non-empty. This property can be written as the existential sentence: where, as above in (6), P A i (x) = P i (x) if i ∈ A, and P A i (x) = ¬P i (x) if i ∈ A. This gives the upper bound (n + 1)2 n to the size of the smallest sentence expressing the given property (we define the size of a formula to be the total number of atomic subformulas and quantifiers occurring in it). In Section 5, we show that this is optimal for existential sentences. If we give up existential sentences and allow a quantifier alternation, we have a smaller sentence φ defined as follows: where addition i + 1 is to be calculated modulo n. The size of φ is only 8n + 4, so this is really optimal (up to a constant factor) because we cannot have such a φ without mentioning each P i at least once.
In our final application, we consider the minimal size of a first-order sentence expressing that the length of a linear order is at least n. It is well known that this can be expressed by a sentence with quantifier rank ⌈log n⌉ + 1. Such a sentence φ n can be obtained as follows: define first recursively formulas θ k (x, y) by letting θ 2 (x, y) := x < y and θ k (x, y) := ∃z(θ l (x, z) ∧ θ m (z, y)), where l = ⌊k/2⌋ + 1 and m = ⌈k/2⌉, for k > 2. Thus, θ k (x, y) says that there are at least k elements in the interval [x, y]. Then φ n can be defined as ∃x∃yθ n (x, y).
Clearly the size of φ n is linear in n. However, with a clever trick of recycling quantified variables it is possible to define a variant φ ′ n of φ n that has size c⌈log n⌉, where c is a small constant. Moreover, φ ′ n can be chosen to be in the 4-variable logic FO 4 (see [4], Section 5). On the other hand, Grohe and Schweikardt prove in [4] that the minimal size of an equivalent sentence in FO 3 is at least 1 2 √ n. Their proof is based on a method which is related to the game we study in this paper, but it is not formulated in a game theoretic form.

A Game for Propositional Logic
We introduce now a game for measuring how long a propositional formula has to be to express a given property of binary strings where s i ∈ {0, 1}. We denote strings by s, r, t etc. Let n be the fixed length of the strings considered. We shall discuss nonempty sets S of such strings and call them string properties. For example, S could be the set of strings (9) where the cardinality of the set {i ∈ {1, . . . , n} : s i = 1} is even. Another example is the set of strings (9) with more ones than zeros. In an extreme case S can be a singleton, e.g. the singleton constant one string {111 . . . 1}. Propositional formulas are built up from propositional symbols (3) by means of ¬, ∧ and ∨. We use Greek letters φ, ψ etc to denote propositional formulas. The concept s |= φ of a string s satisfying a propositional formula φ is defined in the usual way: Definition 1 Suppose φ is a propositional formula and S a string property. We say that φ defines S if for all strings s s ∈ S ⇐⇒ s |= φ.
We define the size w(φ) of the propositional formula φ as follows: Note that w(φ) is just the number of occurrences of propositional symbols in φ. Up to a constant factor, this is the same as the number of symbols in φ.
Note that while there are, up to logical equivalence, 2 2 n propositional formulas over the propositional symbols p 1 , . . . , p n altogether, there are for each m, up to logical equivalence, only at most 2 m · (n + 2) 2m propositional formulas φ with w(φ) ≤ m.
A natural question now is: Question: Given a string property S, what is the size of the smallest propositional formula that defines S.
We shall define a game for the study of this question. In defining the game we follow mostly [1] and to a lesser degree [5]. This game resembles the usual Ehrenfeucht-Fraïssé game for the first order logic, but also the Ehrenfeucht-Fraïssé game for the independence friendly logic, presented in [5].
In the usual Ehrenfeucht-Fraïssé game we have two structures A and B and the game is about their similarity. Player II maintains that the structures are very similar. Player I maintains that there is a difference. During the game player I picks elements from either one of the models and player II tries to find similar elements in the other model.
In the new game we do not have just two models but instead two classes of models. Player II maintains that whatever features the models in one class have all in common, some member of the other class also has. The game to be defined is able to detect very minute differences in models and is in that sense finer than the usual Ehrenfeucht game. In particular, this game can detect differences in the size of conjunctions and disjunctions needed for separating the classes of models. This is a game of perfect information and the concept of winning strategy is defined as usual. Since the rank w m decreases in each move, the game always ends in a finite number of moves. Hence the game is determined: exactly one of the players has a winning strategy in EF w (S, R).
Note that if the players have reached a position (w m , S m , R m ) in the game EF w (S, R), then the continuation of the game from that position onwards can be seen as a play of the game EF wm (S m , R m ). Thus, player I (player II) has a winning strategy in the game EF w (S, R) from position (w m , S m , R m ) onwards if an only if player I (player II, respectively) has a winning startegy in the game EF wm (S m , R m ).
We say that a propositional formula φ separates string properties S and R, in symbols (S, R) |= φ, if s |= φ for all s ∈ S and r |= φ for all r ∈ R. (1) w Player I has a winning strategy in the game EF w (S, R).
(2) w There is a propositional formula φ of size ≤ w such that (S, R) |= φ.
Proof. We prove the equivalence of (1) w and (2) w by induction on w. Consider first the case w = 1. By Definition 2, there are no moves in the game EF 1 (S, R), and player I wins if and only if there is a proposition symbol p i such that either (S, R) |= p i , or (S, R) |= ¬p i . Since w(p i ) = w(¬p i ) = 1, we have (1) 1 =⇒ (2) 1 . On the other hand, if w(φ) ≤ 1, then φ is, up to logical equivalence, either a proposition symbol, or the negation of a proposition symbol. Thus, (2) 1 implies (1) 1 .
Let us then consider the case w > 1, and assume (1) v ⇐⇒ (2) v for all v < w as an induction hypothesis. To prove (1) w ⇐⇒ (2) w , assume first that player I has a winning strategy in the game EF w (S, R). We have the following two cases according to the type of the first move in the winning strategy of player I.
Case 1: Player I makes a left splitting move by choosing u, v, C and D such that 1 ≤ u, v < w, w = u + v and S = C ∪ D. Since this move is given by a winning strategy, player I has a winning strategy in both of the games EF u (C, R) and EF v (D, R). By induction hypothesis, there are formulas ψ and θ such that w(ψ) ≤ u, w(θ) ≤ v, (C, R) |= ψ and (D, R) |= θ. Thus, s |= ψ for all s ∈ C and s |= θ for all s ∈ D, whence s |= ψ ∨ θ for all s ∈ S. On the other hand, for all r ∈ R, r |= ψ and r |= θ, whence consequently Case 2: Player I makes a right splitting move by choosing u, v, C and D such that 1 ≤ u, v < w, w = u + v and R = C ∪ D. Since this move is given by a winning strategy, player I has a winning strategy in both of the games EF u (S, C) and EF v (S, D). By induction hypothesis there are formulas ψ and θ such that w(ψ) ≤ u, w(θ) ≤ v, (S, C) |= ψ and (S, D) |= θ. Thus, for all s ∈ S, s |= ψ and s |= θ, whence s |= ψ ∧ θ. On the other hand, r |= ψ for all r ∈ C and r |= θ for all r ∈ D, whence r |= ψ ∧ θ for all r ∈ R. It follows To prove the converse implication (2) w =⇒ (1) w , assume that there is a formula φ of size ≤ w such that (S, R) |= φ. We show that then player I has a winning strategy in the game EF w (S, R). We assume without loss of generality that φ is in negation normal form 2 . The strategy depends on φ as follows.
Case 1: φ is a proposition symbol or the negation of a proposition symbol. Then by the definition of the game EF w , player I wins without making any moves.
Case 2: φ is ψ ∨ θ. Let C be the set of strings s ∈ S such that s |= ψ, and let D be the set of strings s ∈ S such that s |= θ. Since s |= φ for every s ∈ S, we have S = C ∪ D. Moreover, since r |= φ for every r ∈ R, we have (C, R) |= ψ and (D, R) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (C, R) and EF v (D, R). Thus, using w = u + v, S = C ∪ D as his first move and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (S, R).
Let C be the set of strings r ∈ R such that r |= ψ, and let D be the set of strings r ∈ R such that s |= θ. Since r |= φ for every r ∈ R, we have R = C ∪ D. Moreover, since s |= φ for every s ∈ S, we have (S, C) |= ψ and (S, D) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (S, C) and EF v (S, D). Thus, using w = u + v, R = C ∪ D in his first move, and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (S, R). Q.E.D.
Corollary 4 Suppose K is a string property. Then the following conditions are equivalent: (2) Player I has a winning strategy in the game EF w (S, R) for all S and R such that S ⊆ K and R ∩ K = ∅.
Proof. Suppose K is defined by φ of size ≤ w. Let S and R be given so that S ⊆ K and R ∩ K = ∅. Thus every model in S satisfies φ and no model in R does, whence (S, R) |= φ. By Theorem 3, player I has a winning strategy in EF w (S, R). For the converse, suppose player I has a winning strategy in EF w (S, R) for all (S, R) with S ⊆ K and R ∩ K. This holds in particular if S is K and R is the complement of K. Thus for this choice of S and R we have We get the following method for showing that a string property K is not definable by a propositional formula of size ≤ w: We find classes S and R such that 3. Player II has a winning strategy in EF w (S, R).

The Propositional Complexity of Parity
We shall now prove that the parity of a binary string of n bits cannot be expressed with a propositional formula smaller than n 2 . The result has been proved in [6] with a method which is very similar to ours, even if it does not explicitly use games. We present the proof as an example of the use of our game.
Suppose S and R are disjoint sets of binary strings of length n. Let The density of the pair (S, R) is defined to be the pair Proof. Suppose s > 1 and i ∈ {1, . . . , n}. Then there are f ∈ S and , then there is a string in R satisfying p i (¬p i , respectively). It follows that neither p i , nor ¬p i separates the sets S and R. In As above, we conclude that neither p i , nor ¬p i separates the sets S and R. Q.E.D.
Proof. We prove (a); the proof of (b) is similar. Clearly r 0 + r 1 = r and r 0 s 0 + r 1 s 1 = r s . Since the harmonic mean is never greater than the arithmetic mean 3 , we have and the claim follows. Q.E.D.
Lemma 7 Suppose D(S, R) = (s, r) and w < sr. Then player II has a winning strategy in EF w (S, R).
Proof. The proof is by induction on w. In the case w = 1, the assumption w < sr implies that either s > 1 or r > 1. By Lemma 5, there is no proposition symbol p i such that (S, R) |= p i or (S, R) |= ¬p i . Since the game EF 1 (S, R) ends in its initial position (1, S, R), this means that player II automatically wins this game. Assume then that w > 1. Using Lemma 5 again, we see that player I does not win the game EF w (S, R) without making moves. Suppose then that player I makes a left splitting move w = u + v and S = C ∪ D. Let S 0 ⊆ C and S 1 ⊆ D be sets such that S = S 0 ∪ S 1 and S 0 ∩ S 1 = ∅.
Let D(S 0 , R) = (s 0 , r 0 ) and D(S 1 , R) = (s 1 , r 1 ). Then by Lemma 6(a), contrary to the assumption. If s 0 r 0 > u, then by induction hypothesis, player II has a winning strategy in the game EF u (S 0 , R), whence, a fortiori, he has a winning strategy in EF u (C, R). Otherwise, s 1 r 1 > v, and by the same argument, player II has a winning strategy in the game EF v (D, R). Thus, in any case, player II can make his move in such a way that he is guaranteed to win.
The case of a right splitting move w = u + v and R = C ∪ D is proved in the same way by using Lemma 6(b). Q.E.D.
We are now ready to prove the promised lower bound for parity of binary strings.
Corollary 8 ( [6]) If φ is a propositional formula expressing the parity of strings s ∈ {0, 1} n , then the size of φ is at least n 2 .
Proof. Let S be the set of all strings f ∈ {0, 1} n such that |{i : f i = 1}| is even, and let R be the complement of S. Thus, |S| = |R| = 2 n−1 . Furthemore, for each string f ∈ S, there are n different strings g ∈ {0, 1} n such that |{i : f i = g i }| = 1, and all these strings are in R. Thus, we have |E| = 2 n−1 n, and consequently D(S, R) = (n, n). By Lemma 7, player II has a winning strategy in the game EF w (S, R) whenever w < n 2 , and we conclude that S is not definable by any formula of size less than n 2 . Q.E.D.
As noted in the introduction, the parity of strings in {0, 1} n can be expressed by a formula of size at most (n + 1) 2 . Thus, the lower bound n 2 cannot be essentially improved.

A Game for Predicate Logic
We shall next define a game that can be used for measuring the size of a first-order sentence needed for expressing properties of models. For the sake of simplicity, we will only consider models with relational vocabulary.
We need to fix some notation first. The universe of a model A is denoted by A, of B by B, etc. We use x j , j ∈ N, to denote variables. A variable assignment for a model A is a finite partial mapping α : N → A. The finite domain of α is denoted by dom(α). If φ is a formula, then (A, α) |= φ means that the assignment α satisfies the formula φ in the model A. For this to be meaningful the domain of the assignment α has to include all the j for which the variable x j is free in φ.
We shall discuss classes A of structures (A, α), where A is a model and α is an assignment. We assume that whenever (A, α), (B, β) ∈ A, then A and B have the same vocabulary, and α and β have the same domain, which we denote by dom(A). If α is an assignment on A, a ∈ A and j ∈ N, then α(a/j) is the assignment that maps j to a and agrees with α otherwise. If F is a choice function on A, that is, F is a function defined on A such that This is a game of perfect information and the concept of winning strategy is defined as usual. The game is determined by the Gale-Stewart theorem.
We define the size w(φ) of the formula φ of predicate logic as follows: Note that there are for each w, up to logical equivalence, only finitely many formulas of size ≤ w. (1) w Player I has a winning strategy in the game EF w (A, B).
(2) w There is a formula φ of predicate logic of size ≤ w such that (A, B) |= φ.
Proof. We prove the equivalence of (1) w and (2) w by induction on w. Consider first the case w = 1. By Definition 9, there are no moves in the game EF 1 (A, B), and player I wins if and only if there is an atomic formula φ such that either (A, B) |= φ or (A, B) |= ¬φ. Since w(φ) = w(¬φ) = 1, we have (1) 1 =⇒ (2) 1 . On the other hand, if w(φ) = 1, then φ is, up to logical equivalence, either an atomic formula, or the negation of an atomic formula. Thus, (2) 1 implies (1) 1 .
Let us then consider the case w > 1, and assume (1) v ⇐⇒ (2) v for all v < w as an induction hypothesis. To prove (1) w ⇐⇒ (2) w , assume first that player I has a winning strategy in the game EF w (A, B). We have the following four cases according to the type of the first move in the winning strategy of player I. Case 3: Player I makes a left supplementing move by choosing a natural number j and a choice function F for A. The next position in the game is then (w − 1, A(F/j), B(⋆/j)). Since this move is given by a winning strategy, player I has a winning strategy in the game EF w−1 (A(F/j), B(⋆/j)). By induction hypothesis there is a formula ψ such that w(ψ) ≤ w − 1 and (A(F/j), B(⋆/j)) |= ψ. Let φ be the formula ∃x j ψ. Then w(φ) = w(ψ) + 1 ≤ w, and it suffices to show that (A, B) |= φ. Note first that for all (A, α) ∈ A, (A, α(a/j)) |= ψ, where a = F ((A, α)). Thus we have (A, α) |= φ for all (A, α) ∈ A. On the other hand, for all (B, β) ∈ B and all b ∈ B, we have (B, β(b/j)) |= ψ, whence (B, β) |= φ.
Case 4: Player I makes a right supplementing move by choosing a natural number j and a choice function F for B. The next position in the game is then (w − 1, A(⋆/j), B(F/j)). Since this move is given by a winning strategy, player I has a winning strategy in the game EF w−1 (A(⋆/j), B(F/j)). By induction hypothesis there is a formula ψ such that w(ψ) ≤ w − 1 and (A(⋆/j), B(F/j)) |= ψ. Let φ be the formula ∀x j ψ. Then w(φ) = w(ψ) + 1 ≤ w, and it suffices to show that (A, B) |= φ. Note first that for all (A, α) ∈ A and all a ∈ A, we have (A, α(a/j)) |= ψ. Thus we have (A, α) |= φ for all (A, α) ∈ A. On the other hand, for all (B, β) ∈ B, (B, β(b/j)) |= ψ, where b = F ((B, β)). Thus we have (B, β) |= φ for all (B, β) ∈ B.
To prove the converse implication (2) w =⇒ (1) w , assume that there is a formula φ of size ≤ w such that (A, B) |= φ. We show that then player I has a winning strategy in the game EF w (A, B). As in the case of propositional logic, we can assume without loss of generality that φ is in negation normal form. The strategy of player I depends on φ as follows.
Case 1: φ is an atomic formula or the negation of an atomic formula. Then by Definition 9, player I wins the game EF w (A, B) without making any moves.
Case 2: φ is ψ ∨ θ. Let C be the class of structures (A, α) ∈ A such that (A, α) |= ψ, and let D be the class of structures (A, α) ∈ A such that (A, α) |= θ. Since (A, α) |= φ for every (A, α) ∈ A, we have A = C ∪ D. Moreover, since (B, β) |= φ for every (B, β) ∈ B, we have (C, B) |= ψ and (D, B) |= θ. Finally, as w(φ) ≤ w, there are u and v such that w = u + v, w(ψ) ≤ u and w(θ) ≤ v. Note that u, v < w, and so, by induction hypothesis, player I has a winning strategy in the games EF u (C, B) and EF v (D, B). Thus, using w = u + v, A = C ∪ D as his first move and these winning strategies in the rest of the game, player I is guaranteed to win the game EF w (A, B).
Corollary 11 Suppose K is a class of models of the same vocabulary. Then the following conditions are equivalent: (1) K is the class of models of a first order sentence φ of size ≤ w.
(2) Player I has a winning strategy in the game EF w (A, B) for all A and B such that A ⊆ K and B ∩ K = ∅.
Proof. Suppose K is the class of models of φ and w(φ) ≤ w. Let A and B be given so that We get the following method for showing that a model class K is not definable by a first order sentence of size ≤ w: We find classes A and B such that 3. Player II has a winning strategy in EF w (A, B).

A Game for Existential Formulas
The game EF w can be used for solving questions of the type Given a property of P models, what is the size of the smallest first order formula that defines P?
But in some applications we are interested in definability by some restricted type of of formulas, rather than arbitrary first order formulas. For example, if a property P of models is known to be definable by an existential formula, it is natural to ask, what is the size of the smallest existential formula defining P. We will now define a variant of the game EF w that can be used in studying this question.
Here we say that a first order formula is existential if it is in negation normal form, and it does not contain any universal quantifiers. In other words, existential formulas are built from atomic formulas and negations of atomic formulas by using the connectives ∨, ∧ and the quantifier ∃.
Intuitively, in the definition of the game EF w , left and right splitting moves correspond to the connectives ∨ and ∧, while left and right supplementing moves correspond to the quantifiers ∃ and ∀. Thus, we obtain a game for existential formulas simply by dropping right supplementing moves. (1) w Player I has a winning strategy in the game EF ∃ w (A, B).

Definition 12 Let
(2) w There is an existential formula φ of size ≤ w such that (A, B) |= φ.
Proof. The claim is proved by a straightforward adaptation of the proof of Lemma 10. In the proof of (1) w =⇒ (2) w it suffices to note that omitting Case 4, the formula φ separating the classes A and B will always be existential. Similarly, in the proof of the opposite implication, Case 5 never occurs as the separating formula φ is existential, whence the winning strategy of player I does not use right supplementing moves. Q.E.D.
As in the case of the full first order game EF w , we get again a method for showing that a model class K is not definable by an existential formula of size ≤ w: We find classes A and B such that

The Existential Complexity of Non-Emptiness of Boolean Combinations
We observed in the introduction that non-emptiness of all Boolean combinations of n unary predicates can be defined with a sentence of size 8n + 4 if a quantifier alternation is allowed. If only existential sentences are allowed, this can be expressed with a sentence of size (n + 1)2 n . We use now our game for existential formulas to show that (n + 1)2 n is the best possible value. For each binary string s ∈ {0, 1} n , let B s be the {P 1 , . . . , P n }-structure such that for each r ∈ {0, 1} n , the Boolean combination of P Bs 1 , . . . , P Bs n corresponding to r contains exactly two elements, b r and c r , except that the combination corresponding to s is empty. Furthermore, let A be the structure in which each Boolean combination contains exactly one element; let a r be the element in the Boolean combination corresponding to r ∈ {0, 1} n . Let We will show that player II has a winning strategy in the existential game EF ∃ w (A 0 , B 0 ) for all w < (n + 1)2 n . Since the game is existential, in any position (u, A, B), the set A contains only one structure (A, α), where α is the variable assignment that results from the moves of player I. We say that a structure (B s , β) is flawless (with respect to α), if dom(β) = dom(α), and for all j ∈ dom(α) and all r ∈ {0, 1} n , we have Note that if a s ∈ ran(α), then there is no β such that (B s , β) is flawless. On the other hand, if a s ∈ ran(α), then there is a unique β such that (B s , β) is flawless; we denote this β by β s,α . Furthermore, we say that a structure (B s , β) is good enough (with respect to α), if it is not flawless, but dom(β) = dom(α), and (10) holds for all j ∈ dom(α) and all r = s, and there is a string t ∈ {0, 1} n with |{i : for all j ∈ dom(α). Thus, if a s ∈ ran(α), then for each t ∈ {0, 1} n with |{i : s i = t i }| = 1 there is a unique β such that (B s , β) is good enough; we denote this β by β s,t,α . Assume then, that (B s , β s,t,α ) and (B s ′ , β s ′ ,t ′ ,α ) are two distinct good enough structures in B. Let φ be an atomic formula. If φ is an identity x j = x k (with j, k ∈ dom(α)), then it follows easily from (10) and (11) that (A, α) |= φ ⇐⇒ (B s , β s,t,α ) |= φ. Thus, φ does not separate A and B.
Thus, we see that if B does not contain a flawless structure of the form (B r , β r,α ), then f (B ′ ) = f (B) and g(B ′ ) = g(B), whence the claim is true.
Assume finally, that there is a flawless structure (B r , β r,α ) in B. Since α ′ (j) = a r , no structure (B r , β) is flawless with respect to α ′ . On the other hand, for each t ∈ {0, 1} n with |{i : r i = t i }| = 1, there is a new good enough structure (B r , β r,α (c t /j)) = (B r , β r,t,α ′ ) in B ′ . Thus, in this case Consider now the classes A 0 and B 0 defined in the beginning of this section. Since the variable assignment in the only structure in A 0 is empty, all the 2 n structures (B s , ∅) in B 0 are flawless. Thus, M(B 0 ) = (n+1)f (B 0 )+ g(B 0 ) = (n + 1)2 n , and by Lemma 16, player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) whenever w < (n + 1)2 n . As all Boolean combinations of the predicates P 1 , . . . , P n are non-empty in A, but each structure in B 0 has an empty Boolean combination, we get the desired lower bound result: Corollary 17 If φ is an existential first order sentence expressing the property that all Boolean combinations of n unary predicates are non-empty, then the size of φ is at least (n + 1)2 n .
Q.E.D. 6 The Existential Complexity of the Length of Linear Order As we noted in the introdution, for each n there is first order sentence φ n of logarithmic size with respect to n which expresses the property that the length of a linear order is at least n. However, the sentence φ n has an unbounded number of quantifier alternations. In this section we show that 2n−1 is the minimum size of an existential sentence expressing this property.
Clearly ψ n is true in a linear order if and only if its length is at least n, and an easy induction shows that w(ψ n ) = 2n − 1.
To prove the lower bound, we will use again the existential game EF ∃ w . Let where B is a linear order of length n − 1. Our aim is to show that player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) for all w < 2n − 1. Consider a position (u, A, B) in the game EF ∃ w (A 0 , B 0 ). Since the game is existential, A consists of a single structure (A, α). Let a 1 < A · · · < A a l be the elements in ran(α), and let a 0 and a l+1 be the least and the largest element in A, respectively. We say that a variable assignment β in B is acceptable (with respect to α) if dom(β) = dom(α), there are elements b 1 ≤ B · · · ≤ B b l such that ran(β) = {b 1 , . . . , b l } and for all i ∈ {1, . . . , l} and all j ∈ dom(α) In other words, β is acceptable if and only if the mapping α(j) → β(j), j ∈ dom(α), preserves the relation ≤. Furthermore, we say that β is nice (with respect to α), if it is acceptable, and in addition |{i ≤ l : d(a i , a i+1 ) = d(b i , b i+1 )}| = 1, where d(x, y) is the distance between x and y in the given linear order, and b 0 and b l+1 are the least and the largest element in B, respectively. The distance from defect of β is defined by . Note also, that for each i ≤ l there is exactly one nice β such that i(β) = i.
For the rest of this section, we assume that A is a singleton set {(A, α)} and B is a set of structures of the form (B, β). The niceness measure of B is defined to be where N is the set of all nice variable assignments β such that (B, β) ∈ B. Proof. If N(B) > 1, then either there is a nice assignment β ∈ N such that δ(β) ≥ 1, or there are two distinct nice assignments β, β ′ ∈ N . Assume first that β is a nice assignment in N , and δ(β) ≥ 1. Then there are elements a 1 , . . . , a l , b 1 , . . . , b l such that ran(α) = {a 1 , . . . , a l }, ran(β) = {b 1 , . . . , b l }, a 1 < A · · · < A a l and b 1 ≤ B · · · ≤ B b l . Since β is nice, d(b i , b i+1 ) = δ(β) ≥ 1 for i = i(β), and d(b i , b i+1 ) = d(a i , a i+1 ) ≥ 1 for all other i ≤ l. Thus, we have b 1 < B · · · < B b l . It follows easily from condition (12) that (A, α) and (B, β) satisfy the same atomic formulas, whence no atomic formula separates A and B. Assume then that β, β ′ ∈ N , and β = β ′ . As noted above, this means that i(β) = i(β ′ ). Let a 1 , . . . , a l be as above, and let ran(β) = {b 1 , . . . , b l } and ran(β ′ ) = {b ′ 1 , . . . , b ′ l } with b 1 ≤ B · · · ≤ B b l and b ′ 1 ≤ B · · · ≤ B b ′ l . As above, we see that b i < B b i+1 for all i ≤ l except i = i(β), and similarly b for all i ≤ l except i = i(β ′ ). Moreover, since i(β) = i(β ′ ), for all i, j ≤ l, we have either ( . Using condition (12), it is now easy to see that no atomic formula separates the sets A and B.
Q.E.D. (b) Let N and N ′ be the sets of nice β such that (B, β) is in B and B ′ , respectively. Let ran(α) = {a 1 , . . . , a l } with a 1 < A · · · < A a l , where α is the assignment such that A = {(A, α)}. As usual, we denote by a 0 and a l+1 the least and the largest element in A, respectively. Furthermore, we denote F ((A, α)) by c.
Assume next that c = a 0 or c = a l+1 . Then as above, we see that β ∈ N ⇐⇒ β(d/j) ∈ N ′ , where d is the least or the largest element in B, respectively, and δ(β(d/j)) = δ(β). Thus, also in this case we conclude that N(B ′ ) = N(B).
Assume finally, that c ∈ {a 0 , . . . , a l+1 }. Then there is an index h ≤ l such that a h < A c < A a h+1 . Let β be a nice assignment in N , and let ran(β) = {b 1 , . . . , b l } with b 1 ≤ B · · · ≤ B b l . As noted earlier, there is exactly one nice assignment β h such that i(β h ) = h. If β = β h , then d(b h , b h+1 ) = d(a h , a h+1 ), whence there is an element d such that d(b h , d) = d(a h , c) and d(d, b h+1 ) = d(c, a h+1 ). This means that δ(β(d/j)) = δ(β), and clearly β(d/j) is in N ′ .
Lemma 20 If w < N(B), then player II has a winning strategy in EF ∃ w (A, B).
Proof. The proof is verbatim the same as for Lemma 16; just replace M(B) by N(B). Q.E.D.
The proof of the lower bound result is also similar to that in the previous section. Consider the sets A 0 = {(A, ∅)} and B 0 = {(B, ∅)}. Clearly δ(∅) = n − 1, and so N(B 0 ) = 2(n − 1) + 1 = 2n − 1. Thus, by Lemma 20, player II has a winning strategy in the game EF ∃ w (A 0 , B 0 ) for all w < 2n − 1. Since the length of the linear order A is n, while the length of B is less than n, we have proved Corollary 21 If φ is an existential first order sentence expressing the property that the length of a linear order is at least n, then the size of φ is at least 2n − 1. Q.E.D.


On Extracting Unit Tests from Interactive Programming Sessions

Software engineering methodologies propose that developers should capture their efforts in ensuring that programs run correctly in repeatable and automated artifacts, such as unit tests. However, when looking at developer activities on a spectrum from exploratory testing to scripted testing we find that many engineering activities include bursts of exploratory testing. In this paper we propose to leverage these exploratory testing bursts by automatically extracting scripted tests from a recording of these sessions. In order to do so, we wiretap the development environment so we can record all program input, all user-issued functions calls, and all program output of an exploratory testing session. We propose to then use machine learning (i.e. clustering) to extract scripted test cases from these recordings in real-time. We outline two early-stage prototypes, one for a static and one for a dynamic language. And we outline how this idea fits into the bigger research direction of programming by example.

I. INTRODUCTION
Software engineering methodologies propose that developers should capture their efforts in ensuring that programs run correctly in repeatable and automated artifacts, such as unit tests [1]. However, when looking at developer activities on a spectrum from exploratory to scripted testing we find that many engineering activities include bursts of exploratory testing [2], for example when developers execute selected features of a program on the REPL 1 to ensure some sample input yields correct results, but also when engineers instrument programs with print statements during debugging sessions.
In this paper we propose to leverage these exploratory testing efforts by automatically extracting scripted tests from a recording of these sessions. We call our approach REX, which is short for REPL Extraction. In order to do so, we plan to wiretap the development environment so we can record all program input, all user-issued functions calls, and all program output of an exploratory testing session. We propose to then use machine learning (i.e. clustering) to extract scripted test cases from these recordings in real-time.
The remainder of the paper is structured as follows. In section II we provide a motivating example. In section III we discuss related work. In section IV we outline the proposed approach and two proof-of-concept prototypes. In section V we close with concluding remarks. 1 REPL, abbr. for Read Evaluate Print Loop: interactive live programming interface that is commonly found in the toolbox of dynamic languages. Similar tools exist for static languages in development environments like Eclipse (Java) and VisualStudio (C#), but other than REPLs they tend to be rarely used by practitioners from the respective language communities.

II. REPL EXTRACTION IN A NUTSHELL
In this section we provide a motivating example of test case extraction. Below we show the log file of an interactive programming session that explores Ruby's rational number API. The sessions explores whether adding two numbers returns a reduced representation of the result (user input is set in bold for better readability): To generate the test case, the recorded session is partitioned into three phases: setup (the require statement), interaction (creating the two rational numbers) and assertion (checking that the final print statement is as recorded). Also some filtering happens: Illegal operations are common in interactive sessions and we thus filter them out. In the same line, intermediate output has been discard and only the final output used in the should match assertion. For a discussion of how to accommodate for the possibility that illegal operations or intermediate output are actually the developer's intended assertion under test, please refer to section IV.

III. RELATED WORK
There is a rich body of research on test case and test data generation. However most of this work deals with generating test through program analysis, or by using record-and-replay of interactions at the level of the program's user interface. For a good coverage of test generation the reader is referred to the proceedings of the international conference on Automated Software Engineering (ASE). However, to our best knowledge there is little to no work on automatically extracting unit tests from interactive REPL sessions.
More closely related to the ideas of this paper is work on programming by example, as for example Edward's work on example-centric programming [3]. He presents a development environment with a two editor view: one view shows the stack trace of the current program and the other view shows the source code. Both views can be edited and update one another. And also related is the work by Brad Myers et.al.
where they built systems in which the user defines behaviors by demonstration [4]; in some of them, the system uses AI algorithms, such as inferring complex behavior from a few examples; in others, the user has to provide the full specification, and the examples are used primarily to help the user understand the programming situation.
Smalltalk and LISP, as well as their modern incarnations Pharo 3 and Clojure 4 are also related work, at least in the spirit of standing on the shoulder of giants, as they pioneered the idea of live programming on which this paper relies.

IV. VISION AND APPROACH
With this paper we not only outline a novel tooling approach but also a novel development methodology, inspired by the idea of "tests as examples" [5]. Example-driven development regards unit tests not just as artifacts of scripted testing, but also as documentation and as resumable program state. Documentation in the sense that the source code of a test captures idiomatic use of the unit under test, and resumable program state in the sense that a test's return value can serve as the initial state for either a live programming session or as the setup of another test. Figure 1 illustrates example-driven development: On the left are REPL sessions on the right test cases, here referred to as examples. REPL sessions can be started using a test's return value as initial state (top of the circle) and the proposed REX approach extracts test cases from REPL sessions (bottom of the circle). Thus the circle closes.
We conjecture that in a REX-enabled develop environment most of the programming happens in interactive sessions that are started by selecting from existing examples, similar to development practices in Smalltalk where most programming is known to happen in the debugger rather then the editor. In particular once we extend the REX approach to extract not just test cases but also functions. Such a system would eventually enable users to program the computer by providing 3  This is a far reaching goal, hence the focus of this paper is on the design of a system that extracts test cases form example interactions during a live programming session. We hope that a system like that will support and encourage practitioners in industry in curating better and more complete test suites of their systems. In particular in industries with a "big-P" process where the role of writing software and the role of testing software are possibly assigned to separate people. The capability to capture the exploratory activity of engineerings roles and passing it on as a starting point to testing roles could bring considerable benefits to such settings.
The design space of test case extraction from programming sessions is large. For a first exploration of the design space we decided to go for languages with interactive REPL environment (think Ruby, Javascript tools in modern web browsers, but also Eclipse's Scrapbook and Display views) as it is easy to acquire a transcript of these sessions. We imagine that future designs could also, for example, listen to print statements that developers add during debugging sessions or even record the developer's interaction with a GUI-based debugger and then extract test cases from these recordings. In the following, we are going to describe two proof-of-concept prototypes that aim for the most simple thing that could possibly work, one for the Ruby language and one for the Java language.

A. REX Prototype for irb, the Interactive Ruby Console
The interactive Ruby console, irb, as shown in Figure 2, is a classic read-evaluate-print loop that prompts for user input, evaluates the input and prints the result. Our current prototype works in three steps 1) capturing of the REPL's transcript, 2) At the moment we capture a transcript of the interactive sessions by manually saving a dump of the terminal session. We customized the prompt of irb to include the current system time. These timestamps are used to partition the transcript into bursts of exploratory testing. We use hierarchical clustering and cut it off at a threshold of 90 seconds. This is based on the assumption that exploratory testing happens in bursts where for during exploration session no two instruction are separated by more than 90 seconds, while the sessions themselves are separated by more then 90 seconds. We further group the session by dependencies to global variables (when using a REPL global variables are used to store state).
The previous step results in a hierarchical tree of partitioned REPL instructions. We then turn this tree into an RSpec test suite of the following format: RSpec allows test cases and their setup to be grouped in nested contexts, we can thus transform the tree of extracted test cases without having to flatten it down. So for example, assumed all test cases depend on variable a and some depend on either variable b or variable c, then all test cases would be grouped in one describe context that sets up the initialization of variable a, and nested within that context would be a context each for variable b and variable c. Individual test cases are put in it blocks. Using nested contexts is encouraged best practice when using RSpec [6]. When emitting source code for the test suite, instructions that have lead into an error are excluded. We do not exclude them from the previous clustering step as they might still provide hints that are useful to group the test cases by variable dependency. For each test case we emit a should match assertion for the textual output of the final command. This is based on the assumption that engineers finish an exploratory testing session after having seen a correct output.
If the last instruction resulted in an error we initially used to add an assertion that checks for the presence of this error, but we found that these tests often tended to fail when running the test suite so we currently do not emit any assertion for these test cases. The value of test cases without assertion is debatable, but they might still serve as smoke tests.
Obviously, asserting against the printed representation of an object is fragile with regard to changes to its print method (for Ruby to_s and inspect, for Java toString), however we conjecture that print method change less frequently than other methods of an object. This conjecture is based on a recent study on the use of print methods in object-oriented systems [7]. The idea of striving for simplicity and testing a system by its output rather than deep inspection is also applied in the Sikuli tool, which matches selected screenshots against the current display on the screen to test user interfaces [8].
While dogfooding 6 our prototype we found several gotchas to be covered when matching against textual object representations. For example, some representations (e.g. Ruby's default Object#inspect method) include hash values that differ between program runs. For the same reason, ordering of sets/hash or any data that has been passed through a set or hash might be different. Time might be different. If live data is fetched from the web, that might be different. One possible strategy to alleviate this is to rerun the recorded transcript, and then use regular expressions that exclude those letters that have differed between the original and the repeated REPL sessions. So for example: To summarize test cases and contexts we use a very simple approach. For contexts we name them after all class names (i.e. names starting with an uppercase letter) that appear in their body. And for test cases we use all methods names that appear in their body and prepend them with the verb "should" as it is convention for RSpec tests. There is work on more elaborate test case summarization [9] that we could leverage here.

B. REX Prototype for Eclipse's Scrapbook view
The Eclipse debugger features an interactive programming tool as well, the Scrapbook view, shown in Figure 3. This view is akin to Smalltalk's workspaces, that is a text editor where programmers can evaluate selected text and the results of the evaluation is inserted into the editor after the end of the selection. Again as with the Ruby prototype, our prototype works in three steps 1) capturing of the Scrapbook's content, 2) clustering of the content into a tree of hierarchical test cases (not yet implemented due to limitations of the Scrapbook interface, see discussion below), 3) emitting the source code of a JExample 7 test suite.
To accommodate for the lack of a linear reading sequence in Eclipse's Scrapbook view, our current prototype is limited to coding sessions where all instruction are written one below the other, and all evaluation output is on separate lines. We found that these constraints do not limit the usefulness of the Scrapbook for interactive programming. The content of the Scrapbook is then automatically captured by our REX plugin. We do not currently cluster the content automatically due to limitation of the Scrapbook view, which neither offers a customizable prompt nor global variables. For future work we intend to write our own interactive Java REPL based on the scrapbook's internal interpreter that would be free of such limitations; and even allow us to extract tests in real-time as we are getting a real-time interaction signal.
Eventually we emit source code for a JExample test suite. At the moment these test suites are minimal due to the limitation of our current Java tooling, however in the future REX will allow us to emit source code to hierarchical test suites. JExample allows test cases to be composed into a 7 http://scg.unibe.ch/jexample dependency tree, and offer the option to reuse a test's return value as fixture for dependent tests [10].
While the current Java prototype is not impressive, it proves that interactive coding sessions are possible in static languages and that there is the potential to write an interactive REPL for Java using the internal interpreter of Eclipse 8 .

V. CONCLUDING REMARK
In this paper we presented an approach to extract unit tests from interactive programming sessions. We outlined our ideas for this line of research, which we hope will eventually lead to a programming-by-example system where not only test cases but also functions are extracted from live programming sessions. We presented two prototypes, one in Ruby and one in Java, as a proof of concept of our idea. We would like to extend these prototypes in future work to improve their stability, applicability and usefulness. In the near future we hope to provide benefits to developers in both engineering and testing roles, by providing them with means to automatically capturing their exploratory testing efforts as scripted tests.


Acquisition probability of multi-user UWB systems in the presence of a novel synchronization approach

In this paper, to synchronize Ultra Wideband (UWB) systems in ad-hoc multi-user environments, we propose a new timing acquisition approach for achieving a good performance despite the difficulties to get there. Synchronization constraints are caused by the ultra-short emitted waveforms nature of UWB signals. Used in [1, 2] for single-user environments, our timing acquisition approach is based on two successive stages or floors. Extended for multi-user environments, the used algorithm is a combination between coarse synchronization based on timing with dirty templates (TDT) acquisition scheme and a new fine synchronization scheme developed in [3-6] which conduct to an improved estimate of timing offset. In this work, we develop and test this method in both data-aided (DA) and non-data-aided (NDA) modes. Simulation results and comparisons are also given to confirm performance improvement of our approach (in terms of mean square error and acquisition probability) compared to the original TDT algorithm in multi-user environments, especially in the NDA mode.

INTRODUCTION
UWB systems have received a great attention in the last years. Furthermore, the interest for commercial UWB technology is growing fast especially in the areas of high-data rate shortrange wireless multimedia applications, as well as for low-data rate sensor networks [7]. One of these benefits comes from the large number of users allowed access with Time Hopping (TH) codes, and potential to overlay existing narrowband systems such as IEEE 802.11 and Bluetooth [8]. Hence, the idea of this work is to extend the timing acquisition approach previously developed in [1,2] for multi-user environments this time.
Nevertheless, to exploit these benefits, one of the most important challenges (at least at the physical layer) is to obtain an accurate timing synchronization and more specifically timing offset estimation. In general, synchronization is usually achieved in two stages [9]. The first stage realizes coarse synchronization to within a realistic amount of precision in a short time, and is well-known as the acquisition stage. For this, we use the Timing with Dirty Templates (TDT) acquisition scheme introduced in [10] and developed in [11][12][13][14]. The TDT approach is an attractive technique for UWB systems, which is specified d by its low complexity and rapid acquisition in the DA mode. It's based on correlating adjacent symbol-long segments of the received waveform.
To improve the acquisition probability and the performance of multi-user UWB systems, we propose in the second stage a novel fine synchronization approach known as tracking stage which is responsible for preserving synchronization through clock drifts tacking place in the transmitter and the receiver. Tracking is usually accomplished with a delay locked loop (DLL) [9]. Timing acquisition is an enormous difficulty caused by UWB systems. Compared with the original TDT synchronizer, simulation results show that our new based-TDT-synchronizer can achieve a higher acquisition probability than the original TDT in both NDA and DA modes for multi-user environments.
The rest of this paper is organized as follows. The ensuing Section 2 describes the UWB TH-PAM system in multi-user environments. The Section 3 outlines our novel acquisition algorithm based on two stages. In Section 4, the simulations are carried out to corroborate our analysis in comparison with the original TDT approach. And finally, the conclusions are given in Section 5.

SYSTEM MODEL FOR MULTI-USER LINKS
The UWB time hopping impulse radio signal considered in this paper is a stream of narrow pulses, which are shifted in amplitude modulated (PAM). The same modulated pulse is repeated N f times (frames number) over a T s period (symbol time). During each duration frame T f , a data-modulated ultra-short pulse p(t), with duration , is transmitted [4]. The transmitted waveform from the uth user is (1) where represents the energy per pulse, are differentially encoded symbols and drawn equiprobably from finite alphabet. In our case, symbolize the binary PAM information symbols and indicates the transmitted symbol as (2) where is the chip duration and is the user-specific pseudo-random TH code during the ith frame.
The transmitted signal propagates through the multipath channel corresponding to each user.
The UWB channel is modelled as tapped-delay line with L u taps, where and is amplitude and delay of the L multipath elements, respectively. The channel is assumed quasi-static and among , τ 0 represents the propagation delay of the channel. Thus, the received waveform from all users is (3) where N u is the users number, is the propagation delay of the uth user's direct path and is the zero-mean additive Gaussian noise (AGN). The global received symbol-long waveform is therefore given by (4) Assuming that the nonzero support of waveform is upper bounded by the symbol time T s , the received waveform in (3) can be rewritten as (5) In the next section, we will develop a low-complexity timing acquisition approach using TDT synchronizer in order to find the desired timing offset for multi-user environments. The structure of our synchronization scheme is illustrated in Fig.1.

PROPOSED TIMING ACQUISITION APPROACH
There are many difficulties reaching from the signal and channel characteristics relied to UWB systems that show the importance of the timing acquisition problem and the necessity to resolve it effectively, in particular for multi-user environments. This signifies that there could be numerous steps in the research domain which may be judged satisfactory and may be developed to accelerate the timing acquisition processing.
As mentioned previously, the new acquisition timing scheme proposed in this paper for multiuser environments consists of two complementary stages or floors. The first one is based on a blind (or coarse) synchronization algorithm which id the well-known TDT. The system model structure's with first stage synchronization is shown in Fig.2. This approach is consisted on correlating adjacent symbol-long segments of the received waveform. The basic idea behind TDT is trying to find the maximum of square correlation between pairs of successive symbollong segments. These symbol-long segments are also called dirty templates and they are subject to the unknown offset . Then, we will analyze representing estimate offset of by deriving upper bounds on their mean square error (MSE) in both NDA and DA modes.
After development and calculation, we find the above equation as, where 's are zero-mean information symbols emitted by the th user, , , and corresponds to the superposition of three noise terms [10] and can be approximated as an additive white Gaussian noise (AWGN) with zero mean and power.
Practically, the mean square of x 2 (k;τ) is approximated from the average of different values x 2 (k;τ) for k ranging from 0 to M-1 acquired during an observation interval duration's MT s . In the multi-user case, for the two synchronization modes NDA and DA, the TDT algorithm is given as follows, u E {x 2 (k;τ)} As a second stage, we propose a new fine synchronization approach with low complexity in order to have a more accurate estimate of the exact time synchronization. In this stage, we analyze and develop a fine synchronization algorithm that will give a better estimate of the time delay. The second stage synchronization description's is given in  The idea which is based this floor is extremely simple. The proposition is to scan the time period through a step noted δ by making integration between the received signal and its replica shifted by T f on a window with a width T corr .
is the estimate delay found after the first synchronization stage. We denote the integration window output for the n th step nδ as follows (9) where , and K is the frames number considered for enhancing the decision taken at the first stage. The value of n which maximizes gives the exact moment of pulse beginning noted . Consequently, the fine synchronization is achieved. Finally, note that this proposed timing acquisition approach will be developed in both NDA and DA modes. In the next Section, we will deduce for multi-user environments in what mode this approach gives us better results compared to those given by the original approach TDT in terms of mean square error (MSE) and especially acquisition probability.

SIMULATION RESULTS AND COMPARISONS
In this section, we will evaluate the performance of our timing acquisition approach in multiuser environments with simulations. The UWB pulse is the second derivative of the Gaussian function with unit energy and duration . Simulations are achieved in the IEEE 802.15.3a channel model CM1 [15]. The sampling frequency chosen in the simulations is f c = 50 GHz. Each symbol contains N f = 32 frames each with duration T f = 35 ns. We used a random TH code uniformly distributed over , with N c = 35 and T c = 1.0 ns. The width integration window value's is 4 ns. The performance of our approach is tested for various values of M with the presence of two interfering users. The two interfering users are asynchronous relative to the desired user, and are sending information symbols with 5 and 10 dB less SNR than the desired one.
In Figs. 4-5, we compare the multi-user performances in terms of mean square error (MSE) of both original TDT and fine synchronization approaches for different values of M [4]. From the simulation results, we note that increasing the duration of the observation interval M leads to improved performance for both NDA and DA modes. In comparison with the original TDT approach, we show also that the new timing acquisition approach greatly outperforms the NDA mode and offers a slight improvement in DA mode. In Figs. 6-7, we compare the timing acquisition probability of the proposed synchronizer with the original TDT algorithm. From the simulation results, we deduce that our novel synchronizer can ameliorate the original NDA TDT algorithm and realize a slight improvement performance's to the DA TDT algorithm. This performance amelioration is enabled thanks to the contribution of fine synchronization approach introduced in second stage which can further improve the timing offset found in first stage (coarse synchronization approach: TDT). Unfortunately, this performance amelioration is permitted at the price of higher computation complexity and consequently time lost.

CONCLUSIONS
In this paper, we establish a new timing acquisition approach based on the timing with dirty templates (TDT) introduced in first stage of our synchronization algorithm for UWB radio system. With the fine synchronization approach introduced in second stage, we realize a fine estimation of the frame beginning. The simulation results show that even without training symbols, our novel synchronizer can enable a better performance (in terms of mean square error and acquisition probability) than the original TDT especially in NDA mode and offers a slight improvement in DA mode.