Abstract:Termination of linear programs over closed and bounded domains is analyzed in this paper. The termination of this class of loops can be reduced to that of another class of loops by means of Jordan canonical forms. It has been shown that under some condition, this kind of loops do not terminate over the domains if and only if there exist fixed points or periodic orbits in the domains.

Abstract:Existing work on the verification of information flow in threads mainly focuses on timing channels. However, this paper shows that system calls, such as‘fork’ or ‘join’ with side effects, can also be used to create covert channels intentionally or accidentally. The study results in a dependency logic for verifying information flow in multi-threaded programs where improper calls over thread controlling primitives with side effects could incur illegal information flow. The logic can express the data flow, control flow and the side effects of thread-controlling system calls, and can reason about the dependency relationship among variables and thread identities, to determine whether secret variables interfere with public ones in multi-threaded programs.

Abstract:To obtain as much performance improvement as possible for sequential applications, it is important to exploit parallelism lurking in DOACROSS loops and find good schemes for their parallel execution. Pipelining is such a parallelizing method which can work well for regular DOACROSS loops. However, it is so hard to maintain high performance pipeline parallel codes automatically that parallel compilers always treat DOACROSS loops conservatively. Compilers usually serialize DOACROSS loops, which loses the inherent parallelism of DOACROSS loops and affects the performance of generated parallel programs. To solve this problem, automatic generation of pipeline parallel code for regular DOACROSS loops is implemented for multicore platform based on OpenMP. Firstly, a heuristic is proposed to choose the partition loop and the tiling loop of regular DOACROSS loops. Secondly, a formula based on pipelining cost model is given to compute the optimal tiling size. Lastly, the synchronization between threads is implemented with counter semaphores. Measuring against the wavefront loops of finite difference relaxation, the representative loops of finite difference time domain, and Poisson, LU and Jacobi procedures, the pipeline parallel loops automatically generated by the proposed method increase execution efficiency on multicore platform with the average speedup up to 89% of the optimal speedup obtained manually.

Abstract:In software systems, bug localization is a key step in the bug fix process. By automatically narrowing down potential bug locations, the difficulty of bug fix is greatly reduced. In this paper, a bug localization method based on Gaussian processes, called Gaussian processes bug localization (GPBL) is proposed. This method can facilitate fixing bugs for the developers, by recommending source files that may contain bugs. In order to evaluate GPBL, the open-source software Eclipse and Argouml are employed as data sources. Experimental results show that GPBL can achieve 87.16% recall and 78.90% precision on average. In addition, GPBL can locate relevant buggy files more accurately compared with LDA-based bug localization methods.

Abstract:A massive personalized functional requirement oriented service composition method is presented to support service mass customization. In the realm of real-world service domains, there are usually massive customers who concurrently raise their personalized requirements. For such kind of scenarios, traditional approaches have to deal with each requirement one by one, consequentially leading to high cost. The proposed method considers massive requirements together. First, massive requirements are sorted based on the potential benefit. Then an iterative enhancement strategy is adopted to gradually enhance an existing composition solution based on the similarities between requirements. And finally, a service solution (called service network) with high customization degree is formed. Requirement consolidation is adopted to reduce the algorithm complexity. Comparisons made between the new method and two traditional composition approaches by experiments show the superiority of the new method. The method uses service network as a persistent infrastructure being a combination of personalization and standardization of services, and its objective is to select the minimal amount of candidate services to meet maximal amount of functional requirements, so as to achieve the best cost-effectiveness and high degree of customer satisfaction. The method can be applied to various modern service industries.

Abstract:There are many challenges associated with service selection in a multi-user, dynamic environment. One of these challenges is the frequently changing workload. Traditional approaches to service selection, however, don't adapt to the frequently changing workload in the open and multi-user environment and can't deal with the varied workload in real time. This study is to address the problem, First, a load level based multidimensional QoS model (LLBMQoS) for services is presented; Next, a load aware dynamic service selection model (LADSSM) is proposed based on LLBMQoS to optimize service selection in dynamic environments. The model adopts a two-phase service selection framework, which generates candidate queues in design time and dynamically selects the services in terms of the current workload in execution time. Finally, simulation experiment results are provided to show the proposed model can adapt to the varied workload in a multi-user environment and provide an optimal service selection scheme while meeting the end-to-end QoS constraints.

Abstract:Tabular expressions are a formal notation using Tabular form to organize functions or relationships, and they have been widely used in documenting and analyzing software systems. To avoid misunderstanding and to support user with trustworthy tools, the meaning of these expressions must be fully defined. This paper presents the formal grammar and denotational semantics of the Tabular expressions in general model. By defining semantics assigned equation of each syntax unit of the Tabular expressions' formal grammar, denotational semantics of the Tabular expressions is specified. In addition, the meaning of some classical Tabular expression types and new table types are described based on this semantics. Comparisons made with other semantics description methods show that the denotational semantics method defines Tabular expressions' meaning precisely without subjecting to the restrictions of models and types of Tabular expressions. The proposed method breaks the existing methods' limitations and is an effective method.

Abstract:Argumentation is a kind of interaction between agents for resolving differences in speech. Due to the limitation of knowledge, arguments and its inner statements are usually uncertain, and therefore it is necessary to consider uncertain information processing when modeling the process of argumentation. This paper proposes an argumentation model based on the theory of certainty-factor, in which an argument is expressed as a defeasible rule with several premises but only one conclusion, and the process of argumentation is described as a dialogue tree. In order to do uncertain reasoning, the uncertainty of argument's premise and the strength of the attack that one argument makes against another are assigned with certainty-factors. Next, the algorithms of argument evaluation are provided to compute the credibility of statements. Using the algorithms the set of acceptable arguments can be determined by the credibility threshold and the result of argumentation can be obtained. Finally, an example is given to illustrate the validity of the method. The algorithms are based on numerical computation where the set of acceptable arguments is unique under a given credibility threshold, and can overcome the shortage of extension semantics of Dung's abstract argumentation framework.

Abstract:There exist several problems in existing graph-based semi-supervised learning (GSSL) methods such as model parameters sensitiveness and insufficient discriminative information in data space, etc. To address those issues, this paper proposes a sparse approximated nearest feature space embedding label propagation (SANFSP) algorithm, which is inspired by both ideas of nearest feature space embedding and that of sparse representation. SANFSP first sparsely reconstructs data from original space using its feature space embedding projection images, and then measures the similarity between original data and its sparse approximated nearest feature space embedding projection points, thus proposing a sparse approximated nearest feature space embedding regularizer. At last, SANFSP complets label propagation procedure by using classical label propagation algorithm. The study also derives an easy way to extend SANFSP to out-of-sample data. Promising experimental results are obtained on several toy and real-world classification tasks such as face recognition, visual object recognition and digit classification.

Abstract:Negative information plays an important role in fuzzy knowledge representation and reasoning. This paper distinguishes between contradictory negative relation and opposite negative relation in fuzzy concept, and discovers a characteristic of fuzzy concept that if a pair of opposite concepts are fuzzy concepts, then there must exists a "medium" fuzzy concept between them; conversely, if there is a medium fuzzy concept between the two opposite concepts, then opposite concepts must be fuzzy concepts. Thus, negation of fuzzy concept is considered to include contradictory negation, opposite negation and medium negation. In order to provide a base of logic for the three kinds of negations, this paper proposes a fuzzy propositional logic, FLCOM, with contradictory negation, opposite negation and medium negation, discusses operations and interesting properties as well as characteristics of FLCOM, presents a semantic interpretation of FLCOM, and proves reliability theorem. In order to show that FLCOM is applicable for dealing with fuzzy proposition and its different negations in practical problem, the paper studies applications of FLCOM to fuzzy decision making in an example. Based on FLCOM, the study discusses formal representation of fuzzy proposition and different negations in decision rules, presents an approach to measure truth value of fuzzy proposition and threshold of truth value, and describes reasoning and realization of fuzzy decision making in the example based on fuzzy production rules.

Abstract:Remote attestation, whether binary-based or property-based, mostly undertakes the static environment of the trusted terminal where only part of software configurations in the trusted terminal are demonstrated, leaving trustworthiness of the dynamic running environment unproved. To resolve the problem, a new property-based remote attestation project for the dynamic running environment of the trusted terminal is presented. The project focuses not only on trusted chain and software configuration for the static environment of the trusted terminal, but also on the behaviors of the trusted terminal for the dynamic environment. Moreover, the decidability and algorithm for the trustworthiness of each property by each specific trusted policy is analyzed, and the comprehensive decision strategy is put forward. After that, attestation agent and verification agent which are critical entities in the project, are designed and implemented on Windows, and the communication protocol between them are designed too. Finally, an application case of the project on Windows is introduced, the performance of attestation agent in this application is studied, and the feasibility of the project is demonstrated.

Abstract:Delivery delay is an important performance metric in opportunistic networks. With given buffer size and copy numbers, how to select appropriate nodes to replicate message is the key to minimizing delivery delay. To solve this problem, this paper proposes an optimal stopping decision method for routing opportunistic networks (OSDR). With OSDR, the average meeting time between a node and the destination is regarded as the forwarding utility of the node. A node carrying a message observes the random forwarding utilities of the nodes it meets, and replicates messages according to the optimal stopping rule, which turns out to be threshold-based. By making tradeoffs between the forwarding utility and waiting cost, OSDR achieves the minimum delivery delay expectation. This paper introduces the OSDR network model and existence proof and calculation of optimal stopping rule in detail. Simulation results show that OSDR outperforms other protocols in delivery delay and delivery rate.

Abstract:Network measurement is the foundation for the in-depth research on P2P network. It's a prerequisite for the P2P protocol design, shared content searching, situational awareness as well as research on the security of P2P network. In structured P2P network with decentralized peer to peer relationship, high dynamics and unpredictable instantaneous disturbance, achieving highly accurate and near-complete information retrieval is much more difficult. This paper formalizes the search (or crawl) process of structured P2P network, studies the relationship between the node's route spreadness in the whole network and the query response rate in the midst of crawling, derives some improved search strategies from the knowledge of historic measurements and characteristics of specific P2P network, and proposes a improved search method with much lower bandwidth consumption, fast crawling speed as well as relatively high coverage of nodes in structured peer-to-peer network. KAD network is among the few of structured P2P networks that are extensively deployed. This research mainly concentrates on KAD network and develops a search tool called KadCrawler, upon which large amounts of measurements and analysis are conducted. The result shows that the proposed method is both feasible and effective. Lastly, an analysis on the topology and phenomenon of ID repetition reveals that KAD network has changed significantly over the years.

Abstract:Hidden node problem is an important factor in performance degradation of IEEE 802.15.4 protocol. This paper presents a resolution strategy of hidden collision based on collision indication and grouping. The new strategy, named Hidden Node Collision Detection and Avoidance Strategy (HNCDAS), uses grouping method to divide the CFP of IEEE 802.15.4 protocol into several equal slot cycles and extract the hidden node address information from some damaged frame caused by the hidden conflict. The strategy dynamically adjusts nodes to different competition groups based on currently obtained hidden relationship. The nodes within competitive groups still competitively send messages in accordance with the binary back method in the same period, while different competitive groups send messages in different time slots. As a result, the strategy completely solves the hidden conflict problem. Compared with other hidden node collision resolution strategies, HNCDAS has certain advantages such as less overhead and dynamic adjustment capability. The convergence of the strategy and the maximum time of resolution strategies are also demonstrated in theory. Experimental results show that HNCDAS can significantly improve data transmission rate, throughput and energy efficiency.

Abstract:Reconfigurable Fundamental Information Communication Network achieves optimum transmission quality for special services by establishing Omnibus Circuits. Due to the support of network virtualization in this architecture, optimum efficiency of Omnibus Circuits can be promoted by mapping services of the same type to one group of substrate devices. For this requirement, this paper designs a virtual network mapping algorithm for service aggregation. Because this algorithm has a comprehensive consideration of surplus resources and situation of mapped services, the services tend to be mapped on the substrate devices which host numerous services of the same type. Furthermore, a node selection strategy with hop constraint is proposed for reducing the running time of the algorithm. Simulation experiments show that this algorithm not only has a better performance in the acceptance ratio and the resource occupancy rate, but also substantially increases the degree of service aggregation.

Abstract:While server-centric data center networking schemes partly resolve the performance bottleneck and extensibility problems in existing tree-based networking schemes, designing a high extensible data center networking scheme with high performance is still a challenging problem. This paper proposes a high extensible and high performance data center networking scheme, called XDCent, where servers have fixed number of network interface card (NIC) ports. In the case that each server has the fixed number of NICs, XDCent can not only result in a high performance for data centers but also extend data centers continually without affecting the running applications.

Abstract:Low duty cycle is proposed to reduce the energy consumption of WSNs (wireless sensor networks), thereby extending the lifecycle of WSNs. However, low duty cycle makes neighbor discovery extremely difficult. Especially considering the mobility of nodes, effective neighbor discovery is more challenging. In this work, a new neighbor discovery algorithm based on Continuous Torus Quorum is proposed to solve the neighbor discovery problem in asynchronous symmetric and asymmetric low duty cycle WSNs. A neighbor discovery probability is also provided to estimate efficiency of neighbor discovery algorithms in mobile scene. Furthermore, a simulation platform is developed to measure performance of neighbor discovery algorithms. Both theoretical analysis and simulation results reveal that Continuous-Torus-Quorum-based algorithm can achieve significant performance improvement over several classical heterogeneous neighbor discovery algorithms, such as Disco and U-Connect, in terms of energy efficiency, discovery delay and discovery probability in the symmetric and asymmetric scenes.