Search

One of the main challenges for researchers to build routing protocols is how to use energy efficiently to extend the lifespan of the whole wireless sensor networks (WSN) because sensor nodes have limited battery power resources. In this work, we propose a Sector Tree-Based clustering routing protocol (STB-EE) for Energy Efficiency to cope with this problem, where the entire network area is partitioned into dynamic sectors (clusters), which balance the number of alive nodes. The nodes in each sector only communicate with their nearest neighbour by constructing a minimum tree based on the Kruskal algorithm and using mixed distance from candidate node to base station (BS) and remaining energy of candidate nodes to determine which node will become the cluster head (CH) in each cluster? By calculating the duration of time in each round for suitability, STB-EE increases the number of data packets sent to the BS. Our simulation results show that the network lifespan using STB-EE can be improved by about 16% and 10% in comparison to power-efficient gathering in sensor information system (PEGASIS) and energy-efficient PEGASIS-based protocol (IEEPB), respectively.

This paper improves the breadth-first search strategy in directed automated random testing (DART) to generate a fewer number of test data while gaining higher branch coverage, namely Static DART or SDART for short. In addition, the paper extends the test data compilation mechanism in DART, which currently only supports the projects written in C, to generate test data for C++ projects. The main idea of SDART is when it is less likely to increase code coverage with the current path selection strategies, the static test data generation will be applied with the expectation that more branches are covered earlier. Furthermore, in order to extend the test data compilation of DART for C++ context, the paper suggests a general test driver technique for C++ which supports various types of parameters including basic types, arrays, pointers, and derived types. Currently, an experimental tool has been implemented based on the proposal in order to demonstrate its efficacy in practice. The results have shown that SDART achieves higher branch coverage with a fewer number of test data in comparison with that of DART in practice.

This paper presents two test data automatic generation methods which are based on weighted control flow graph (named WCFT) and boundary values of input parameters (named BVTG). Firstly, WCFT method generates a CFG from a given unit function, updates weight for it, then generates test data from the greatest weight test paths. In the meantime, WCFT can And dead code that can be used for automatic source code errors fix. Secondly, BVTG method generates test data from boundary values of input parameters of the given unit function. The combination of the two generated test data sets from these two methods will improve the error detection ability while maintaining a high code coverage. An implemented tool (named WCFT4Cpp) and experimental results are also presented to show the effectiveness of the two proposed methods in both time required to generate test data and error detection ability.

Global variables may have a significant impact on preventing programs from automatic parallelism. This paper introduces a practical approach to measure the effect of global variables on program parallelism. First, we conduct static data dependence analysis among program variables and represent such dependencies by a Variable Dependence Graph. Then, we analyze this graph for measuring and identifying which global variables have a significant impact on program parallelism. To evaluate this approach, we conduct experiments on 20 benchmark programs and an industrial application. The experimental results show that half of the studied programs contain large impact variables which may be the cause of preventing programs from parallel execution.

The two-phase assume-guarantee verification method for timed systems using TL algorithm implemented in the learner has been known as a potential method to solve the problem of state space explosion in model checking thanks to its divide and conquer strategy. This paper presents three improvements to the verification method. First, we remove the untimed verification phase from the verification process. This removal reduces the time complexity of the verification process because of the great time complexity of this phase. Second, we introduce a maxbound to the equivalence queries answering algorithm implemented in the teacher which acts as a method for the teacher to return "don't know" results to the learner to prevent the verification process from many endless scenarios. Finally, we introduce a technique to analyze the counterexample received from the teacher and another one implemented in the equivalence queries answering algorithm which helps the teacher not return a counterexample that has been returned to the learner. This technique keeps the verification process from running forever in several circumstances. We give primitive experimental results for both two-phase assumption generation method and the improved one with some discussions in the paper.

Assume-guarantee reasoning, a well-known approach in component-based software (CBS) verification, is infact a language containment problem whose computational cost depends on the sizes of languages of the softwarecomponents under checking and the assumption to be generated. Therefore, the smaller language assumptions,the more computational cost we can reduce in software verification. Moreover, strong assumptions are moreimportant in CBS verification in the context of software evolution because they can be reused many times in theverification process. For this reason, this paper presents a method for generating locally strongest assumptions withlocally smallest languages during CBS verification. The key idea of this method is to create a variant techniquefor answering membership queries of the Teacher when responding to the Learner in the L–based assumptionlearning process. This variant technique is then integrated into an algorithm in order to generate locally strongestassumptions. These assumptions will effectively reduce the computational cost when verifying CBS, especiallyfor large–scale and evolving ones. The correctness proof, experimental results, and some discussions about theproposed method are also presented.Keywords: Assume-guarantee reasoning, Model checking, Component-based software verification, Locallystrongest assumptions, Locally smallest language assumptions.

The dialect identification was studied for many languages over the world nevertheless the research on signal processing for Vietnamese dialects is still limited and there were not many published works. There are many different dialects for Vietnamese. The influence of dialectal features on speech recognition systems is important. If the information about dialects is known during speech recognition process, the performance of recognition systems will be better because the corpus of these systems is normally organized according to different dialects. This paper will present the combination of MFCC coefficients and fundamental frequency features of Vietnamese for dialectal identification based on GMM. The experiment result for the dialect corpus of Vietnamese shows that the performance of dialectal identification is increased from 59% for the case using only MFCC coefficients to 71% for the case using MFCC coefficients and the information of fundamental frequency.

This paper presents a framework for verifying evolving component-based software using assume-guarantee logic. The goal is to improve CDNF-based assumption generation method by having local weakest assumptions that can be used more effectively when verifying component-based software in the context of software evolution. For this purpose, we improve the technique for responding to membership queries when generating candidate assumptions. This technique is then integrated into a proposed backtracking algorithm to generate local weakest assumptions. These assumptions are effectively used in rechecking the evolving software by reducing time required for assumption regeneration within the proposed framework. The proposed framework can be applied to verify software that is continually evolving. An implemented tool and experimental results are presented to demonstrate the effectiveness and usefulness of the framework.

The Assume-guarantee verification using $TL^{*}$ algorithm implemented in Learner is an important method to alleviate the state space explosion problem in model checking of timed systems, thanks to its divide and conquer strategy. This paper presents an improvement for $TL^{*}$ learning algorithm of Learner by removing the first phase from the verification process and starting learning assumption from $\lambda $. This improvement reduces the time complexity and covers a number of cases where assumptions exist while the original $TL^{*}$ algorithm cannot. Besides, this paper adds a kind of bound to the candidate query answering algorithm of Teacher for it to return “don’t know” result and prevent Learner from running endlessly. We give some discussions related to both of original algorithms and the improved ones in the paper.

This paper proposes a method for automated user interface testing of Windows-based applications to increase the accuracy in identifying the target widgets or executing several interactions. The key idea of this method is to generate new test scenarios from widgets and test specification where widgets are extracted during the execution of the application and test specification is generated by combining the interactions of widgets. Furthermore, the paper contributes some techniques to detect hidden widgets which considering as one of the most challenging problems in user interface testing. Currently, a supporting tool has been implemented and tested with several industrial projects. The details of the experimental results will be presented and discussed.

This paper presents a novel tool for change impact analysis of Java EE applications named JCIA. Analyzing the source code of the Java EE applications is a big challenge because of the complexity and large scale of the applications. Moreover, components in Java EE applications are not only in Java language but also in different languages such as XHTML, XML, JSP. This tool analyzes source code of Java EE applications for building the dependency graphs (called JDG). The main idea for generating JDG is based on developing the source code analyzers for the typical technologies of Java EE such as JavaServer Faces, Context and Dependency Injection, Web services. Based on the obtained JDG and the given change sets, JCIA calculates the corresponding impact sets by applying the change impact analysis (CIA) based on change types and Wave-CIA method. The calculated impact sets help managers in planning and estimating changes, developers in implementing changes, and testers with regression testing.

This research proposes an automated test data generation method for C/C++ projects to generate the lower number of test data while gaining higher code coverage in comparison with KLEE, CAUT, PathCrawler, and CREST. In order to do that, the proposed method contributes an algorithm named loop depth first search by combining both static testing and concolic testing together. Besides, the paper also provides an improvement symbolic execution for avoiding the initial test data problem in the concolic testing. Currently, a tool supporting the proposed method has been developed and applied to test on different C/C++ projects in several software companies. The experimental results show the higher coverage with the lower number of test data compared with the existing methods. The experimental results display the effectiveness and practical usefulness of the proposed method for automated test data generation in practice.

This manuscript describes a method to program everyday manipulation tasks for the robots from human demonstration by using a movement generating model and primitive skills. The hand movement in the demonstrated task is recorded by using a hand motion tracker with a Kinect camera and a color-marker glove. The recorded movement is segmented to sub-actions and then mapped to primitive skills which can be built independently with the task. To adapt with the change of the goal position, Dynamic Movement Primitives model was applied to generate movement trajectory which follows the demonstrated trajectory. In experiment, we considered the task “dispensing water” from a water thermos pot performed by a robot arm. We implemented DMPs model for the sub-movement such as ‘approaching object’ to confirm the adaptation to new goal of movement trajectory. We proposed a list of necessary common skills to use for accomplishing the demonstrated task and can be reused in other everyday manipulation tasks.

This manuscript presents a method to program everyday manipulation tasks for a robot by human demonstration using primitive skills. The hand movement in the demonstrated task is recorded then segmented into sub-actions. Each sub-action is mapped to primitives skills of the robot. We proposed a list of necessary skills for a manipulator which are common to use in many everyday tasks. In order to adapt with the change of object's location, we applied Dynamic Movement Primitives model for regenerating movement which follows the demonstrated trajectory. In experiment, we considered the task “dispensing water” from a water thermos pot performed by a robot arm to verify the proposed method.

The assume-guarantee verification has been recognized as a promising method for solving the state space explosion in modular model checking of component-based software. However, the counterexample analysis technique used in this method has huge complexity and the computational cost for generating assumptions is very high. As a result, the method is difficult to be applied in practice. Therefore, this paper presents two improvements of the assume-guarantee verification method in order to solve the above problems. The first one is a counterexample analysis method that is simple to implement but effective enough to prevent the verification process from infinite loops when considering the last action of counterexample as suffix in implementation. This is done by finding a suffix that can make the observation table not closed when being added to the suffix set of the table and use that suffix for the learning process. The second one is a reduction of the number of membership queries to be asked to teacher when learning assumptions. This results in a significantly faster speed in generating assumption than that of the original algorithm. An implemented tool and experimental results are also described to show the effectiveness of the improvements.

This paper proposes an automated test cases generation method from sequence diagrams and class diagrams with string constraints. The method supports UML 2.0 sequence diagrams including twelve combined fragments. An algorithm for generating test scenarios are developed to avoid test paths explosion without having data sharing points of threads in parallel fragments or weak sequencing fragments. Test data are also generated with solving constraints of string variables. We standardize string constraints and equations at the boundary of variables that are input formula of Z3-str solver. Comparing with the current approach of the solver, some preprocessing rules are extended for other operations such as charAt, lastindexOf, trim, startsWith and endsWith. If a result of the Z3-str is SAT, test data of each test scenario are generated to satisfy the constraints with boundary coverage. A tool is implemented to support the proposed method, and some experiments are also presented to illustrate the effectiveness of the tool.

This research proposes an automated test case generation method for C functions. In this method, the source code is transformed into a control flow graph corresponding to the given coverage criterion. After that, a list of feasible test paths are discovered by traversing the control flow graph using backtracking algorithm, symbolic execution, and Z3 solver. We also generate test cases for functions containing one loop or two-nested loop. A tool supporting the proposed method has been developed and applied to test on some C functions. The experimental results show the high coverage with the minimum number of test cases, the ability to improve the total time of the test case generation with a specified coverage criterion, and the increasing precision of checking the feasibility of test paths if comparing with the random technique. The experimental results display the potential usefulness of this tool for automated test case generation in practice.

This paper proposes an automated test data generation method from the information embedded in model elements such as Unified Modeling Language (UML) sequence diagrams, class diagrams, and Object Constraint Language (OCL). The method supports UML 2.0 sequence diagrams including eight kinds of combined fragments describing control flow of systems. Comparing with some approaches by using depth first search (DFS) or breadth first search (BFS) algorithms, the proposed method generates all possible test scenarios with the higher error uncover capability. Test data for testing loop fragment is also generated. Therefore, it helps to detect errors in testing loops and the concurrency errors such as safety and liveness property of the systems.

Composing existing services to create new services has been considered as an important activity of developing service-oriented architecture systems. The increment of services that provide the same functionality but different qualities leads to the complexity in finding the best solution for a composite service. In a heterogeneous and dynamic environment, QoS negotiation provides a flexible means for choosing suitable atomic services for service compositions. However, most proposed negotiation approaches assume that services are independent of others in terms of quality. Consequently, these negotiation approaches are not able to handle the correlation factors among services. This paper presents a flexible correlation-aware negotiation approach for service compositions. In our approach, the service correlations are considered as factors affecting the choice of concrete services. The effectiveness of the approach is demonstrated via experiments.

This paper proposes an efficient method for automated generating models of component-based software. This method accepts regular expressions that describe behaviors of software components. The proposed method uses the CNNFA algorithm to parse the regular expressions in order to generate corresponding models. This method can generate minimal accurate models of the software components. A tool is implemented and applied for some typical systems to show the efficiency of this method. The obtained experimental results show that this method is faster than existing methods. The generated models play an important role in making such model-based approaches as model checking and model-based testing more feasible in practice.

This paper presents a method for automated control flow testing of unit programs. The key idea of this method is to combine the black-box and white-box techniques in order to minimize the complexity of white-box testing. Instead of performing black-box and white-box separately, the proposed method uses the test inputs that are generated by black-box to reduce searching space of white-box testing. The method then continually eliminates arcs in remaining space to find non-duplicated test paths. Therefore, the proposed method is able to operate white-box testing with less effort than the current method.

This paper proposes a method and a tool support for automated data flow testing of Java programs. The key purpose of this method is to detect improper uses of data values due to coding errors. Given source code of a Java program, the proposed method analyzes and visualizes the program as a data flow graph. All test paths for covering all definition-use pairs of all variables are then generated. A test case corresponding to each generated test path is produced by identifying values to the input parameters so that the test path is executable. The expected outputs of these test cases are identified automatically. An implemented tool supporting the improved method and experimental results are also presented. This tool is promising to be applied in practice.

This paper introduces an assume-guarantee model checker, named AGMC, for verifying correctness of designs of component-based systems. Given UML 2.0 sequence diagrams that describe behaviors of the system components and a required property, AGMC generates accurate models of the components represented by labeled transition systems (LTSs) automatically. AGMC then model checks that whether the system satisfies the property by using the assume-guarantee verification method. AGMC has been implemented and tested by applying some typical component-based systems. The implemented AGMC is not only useful to verify component-based systems in practice but also has a potential to solve the state space explosion problem in model checking.

The model-based approaches are difficult to be applied in practice due to the lack of formal models describing behaviors of systems. This paper proposes a method for generating accurate models of components in order to solve this issue in the context of the component-based systems. The key idea of this method is to generate minimal deterministic finite automata as the accurate models of the corresponding components. For this purpose, the proposed method first computes a set of traces as a regular language of a given component by executing all possible experiments over the alphabet of the component. This method then constructs a regular expression to represent this set. After that, a minimal deterministic finite automaton as an accurate model of the component is generated by applying the Thompson algorithm and some optimized activities. The generated models are useful for the existing model-based approaches, e.g., model checking and model-based testing in improving quality of component-based software. An implemented tool supporting the method and experimental results are also presented.

This paper proposes an effective framework for the assume-guarantee verification of component-based software in the context of component evolution at system design level. In this framework, when a component is evolved after adapting some refinements, we do not recheck all components in the evolved system, but only the evolved component. For this purpose, if the design model of the evolved component satisfies the current assumption of the system before evolving, the evolved system still satisfies the required property. Otherwise, if the assumption is too strong to be satisfied by the model, a new assumption must be generated again. We propose two methods for regenerating the new assumption called assumption regeneration and minimized assumption regeneration. The methods reuse the assumption to reduce a large number of required membership queries and candidate assumptions which are needed to generate again the new assumption. An implementation and experimental results are presented.

An assume-guarantee verification method has been recognized as a promising approach to verify component-based software with model checking. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. This method allows us to decompose a verification target into components so that we can model check each of them separately. In this method, assumptions which are environments of the components are generated. The number of states of the assumptions should be minimized because the computational cost of model checking is influenced by that number. Thus, we propose a method for generating minimal assumptions for the assume-guarantee verification of component-based software. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. These assumptions are seen as the environments needed for the components to satisfy a property and for the rest of the system to be satisfied. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. We have implemented a tool for generating the minimal assumptions. Experimental results are also presented and discussed.

This paper proposes a framework for verifying component-based software in the context of component evolution. This framework includes two stages: modular conformance testing for updating inaccurate model of the evolved component and modular verification for evolving component-based software. When a component is evolved after adapting some refinements, the proposed framework only focuses on this component and its model in order to update the model and recheck the whole evolved system. The framework also reuses the previous verification results and the previous models of the evolved component to reduce several steps of the model update and verification processes.

Automated user interaction testing of Web applications has been received great attentions from the research community and industry. Currently, several available tools are proposed to partly deal withthe problem. However, how to perform the automated user interaction testing of whole Web applications effectively is still an open problem. This research proposes a method and develops a tool supporting automated user interaction testing of whole Web applications. In this method, the model of each Web page of the Web application under testing which describes the user interaction (UI) is represented by a finite state automaton. The whole model that describes the behaviors of the whole Web application then is constructed by composing the models of all Web pages. After that, test paths are generated automatically based on the compositional model of the Web application so that these test paths cover all possible user interactions of the application. A tool supporting the proposed method has been developed and applied to test on some simple Web applications. The experimental results show the potential application of this tool for automated user interaction testing of Webapplications in practice