Abstract:

Abstract:This paper designs a domain-specific language P3 for reconfigurable protocol-independent packet parsers. Due to the requirement to facilitate the implementation of a high-security network, the language is designed from the perspective of high trustworthiness, including the formal definition of type system and operational semantics of the language and its trusted compiler architecture. Based on the full understanding of the basic requirements of the reconfigurable hardware, from the view of hardware-software codesign, the core characteristics of P3 language and its trusted compiler architecture named P3C are finally defined. As the reconfigurable packet parser is an important part of SDN and programmable data plane, implementing the trusted compiler architecture of P3C will be of great significance to the security of SDN. It is expected that the development of P3C project will promote the further research in the field of network and formal method.

Abstract:As the application software's architecture style changes and its scale enlarges, the running environment of the application software turned out to be more complex than before. This prompts the verification of the application system architecture as early as in design phase to evaluate the deployment plan objectively and to contribute to the active maintenance of the system, while the existing methods of modelling and verification of the application system architecture needs the support of kinds of tools. In this paper, under the background of MDSE (model driven software engineering), a higher-order typed verifiable application system architecture modelling language (V_ASAML) and verifiable application system architecture modelling method (V_ASAMM) are proposed. In the V_ASAML language, the syntax and semantics of types and terms are defined to describe the structure of the system compositions' types and objects, the typing rules and its type checking algorithms are defined to process the judgement of Γ|-t:T and Γ|-R(T₁,T₂). In the V_ASAMM method, the system architecture modelling process is presented, which are the modelling of M_bd (basic data type), M_bti (basic interface type), M_dev (device type), and M_frwk (framework type). In each layer, modelling of the types and the relations of the types are needed, while the typing rules corresponding to the type relations are automatically generated. Furthermore, the device service invocation graph (G_DSI) is defined to describe the deployment requirements and the type sequences and its correctness are defined to describe the properties of user requirements, with the related verification algorithms. The prototype of the verifiable application system architecture modelling system (V_ASAMS) as a modelling and verifying tool is developed, to which support to the design process by modelling and the automatic verification of the design regarding to the requirements. Finally, the method is applied to a real case of large scale by the design of an application system architecture and it is well verified.

Abstract:PaxosStore is a highly available distributed storage system developed by Tencent Inc. to support the comprehensive business of WeChat. PaxosStore employs a variant of Paxos which is a classic protocol for solving distributed consensus. It is called as TPaxos in this study. The originality of TPaxos lies in its “uniformity”: it maintains a unified state type for each participant and adopts a universal message format for communication. However, this design choice brings various differences between TPaxos and Paxos, rendering TPaxos hard to understand. Moreover, although the core code (including both pseudocode and source code in C++) for TPaxos is publicly available, there still lacks a formal specification of TPaxos. Finally, as far as literature demonstrates, TPaxos has not yet been manually proven or formally checked. To address these issues, three main contributions are expounded in this paper. First, it is demonstrated that how to derive TPaxos from classic Paxos step by step. Based on this derivation, TPaxos can be regarded as a natural variant of Paxos and is much easier to understand. Second, TPaxos in TLA+, a formal specification language, is described. In the course of developing the TLA+ specification for TPaxos, a crucial but subtle detail is uncovered in TPaxos which is not fully clarified. That is, upon messages, do the participants (as acceptors) make promise that no proposals with smaller proposal numbers will be accepted before accepting proposals or vice versa? This leads to two different interpretations of TPaxos and motivates authors to propose a variant of TPaxos, called TPaxosAP. In TPaxosAP, the participants accept proposals first, and then make promise. Third, the correctness of both TPaxos and TPaxosAP is verified by refinement. Particularly, since the known voting mechanism called Voting cannot capture all the behaviors of TPaxosAP, EagerVoting for TPaxosAP is first proposed and then the refinement mappings are established from TPaxosAP to EagerVoting and from EagerVoting to consensus. They are also verified using the TLC model checker.

Abstract:Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.

Abstract:In order to ensure the reliability of task management design in the operating system on the satellite, the theorem proving tool Coq is used to requirements layer modeling and formal verification of the operating system task management module. From the user point of view for the basic mechanism of on-board operating system task management, this study proposes verification method based on task state list collection. The mechanism process is formalized and implemented in Coq. Six properties are consistent with the task management of the real-world operating system for the established requirements layer model. This article gives a verification process of one of the properties in Coq. The result shows that the model satisfies the properties of the article.

Abstract:Basic parallel process (BPP) is a model for describing and analyzing concurrent programs, which is an important subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPP is undecidable. This study proposes an algorithm for the problem of bounded model checking EG over BPP. First, a bounded semantics of EG over BPP is proposed. Then, according to the constraint-based approach, a reduction from the problem of bounded model checking EG over BPP to the satisfiability problem of linear integer arithmetic formulas is given. Finally, the linear integer arithmetic formulas are solved by SMT solvers.

Abstract:Software self-adaptation (SSA) provides a way of dealing with dynamic environment and uncertain requirement. There are existing works that transform the dynamic and uncertainty concerned by SSA into regression, classification, cluster, or decision problems; and apply machine learning algorithms, including reinforcement learning, neural network/deep learning, Bayesian decision theory and probabilistic graphical model, rule learning, to problem formulation and solving. These kinds of work are called as “machine learning enabled SSA” in this study. The survey is conducted on the state-of-the-art research about machine learning enabled SSA by firstly explaining the related concepts of SSA and machine learning; and then proposing a taxonomy based on current work from SSA perspective and machine learning perspective respectively; analyzing the machine learning algorithms, software external interaction, software internal control, adaptation process, the relationship between SSA task and learning ability under this taxonomy; as well as identifying finally deficiency of current work and highlighting future research trends.

Abstract:Bug localization is one of the most active domains in software engineering. Most of the bugs are submitted to bug tracker systems, e.g., Bugzilla and Jira. Because of the large number of the submitted bug reports, it is difficult for developers to resolve these defects in time. Therefore, an automatic tool to help developers to identify bug related files is needed. Many bug localization technologies have been proposed by researchers. Taking advantages of the text nature of bug report, information retrieval technologies are adopted to solve bug localization problems. Due to the low computing cost and the applicability to various programming languages, information retrieval-based bug localization (IRBL) technologies become hot spots in bug localization and acquire a series of achievements. However, challenges still exist in data preprocessing, similarity calculation, and engineering application. Therefore, current IRBL technologies are summarized. The contributions of this study are: (1) the data preprocess methods and general information retrieval algorithms are summarized; (2) the feature categories are concluded and classified; (3) the performance measures are concluded; (4) the current problems in IRBL technologies are highlighted; and (5) the trends of IRBL technologies are outlooked.

Abstract:As an important cryptographic criterion of Boolean function, algebraic degree is widely used in the design and analysis of ciphers. This work mainly studies the algorithm for estimating algebraic degree of Boolean function and its applications to SIMON-like ciphers. Firstly, by analyzing the algorithm of using truth table to solve algebraic normal form, a parallel solution architecture based on CUDA is constructed. The model uses the CPU and GPU computing resources collaboratively, which greatly reduces the time for solving algebraic degree. As applications, the algebraic degree of full round function is solved for SIMON32 and SIMECK32 in a short time. Secondly, based on the Cube attack theory, a probabilistic algorithm for estimating algebraic degree is presented according to the relationship between algebraic degree and superpoly. The algorithm is applied to estimate algebraic degree of general SIMON-like ciphers. Finally, from the algebraic degree point of view, the differences of SIMON-like ciphers selecting different cyclic shift parameters are given, and then some design choices for cyclic shift parameters are proposed. The experiment shows that SIMON has shortest number of required rounds to reach maximum algebraic degree under original parameters, thus means that the original parameters have higher security.

Abstract:Emotion recognition is an interdisciplinary research field which relates to cognitive science, psychology, signal processing, pattern recognition, artificial intelligence, and so on, aiming at helping computer understand human emotion state to realize natural human-computer interaction. In this survey, the psychological theory of emotion is firstly introduced as the theoretical basis for the emotion model used in emotion recognition, including appraisal theory, dimensional models of emotion, brain mechanisms, and computing models. Then, the advanced technologies of dimensional emotion recognition from the artificial intelligence perspective, such as the speech emotion corpora, feature extraction, classification, are presented in detail. Finally, the challenges of dimensional emotion recognition are discussed and the workable solutions and future research directions are proposed.

Abstract:Sentiment analysis aims to judge the emotional tendency of the text, while the review quality prediction aims at judging the quality of the review. Sentiment analysis and review quality detection are two key tasks in sentiment analysis, these two tasks are closely related by many factors, the reviews on the same product have similar opinion polarity, and the quality of reviews from the same user tend to be similar. Therefore, this study proposes a joint neural model to learn sentiment analysis and quality prediction in order to better study the correlation between sentiment classification and review quality prediction tasks and the impact of user information and product information on sentiment classification and review quality prediction respectively. First of all, this study employs a deep representation learning approach to learn textual information of reviews, serving as the basis to connect two tasks, and then uses the user reviews and product reviews as the representation of the user and the representation of the product, on the basis, a user attention is adopted to encode user information in user representation, and a product attention is used to encode product information in product representation, and finally both user and product representations are jointly integrated for sentiment analysis and quality prediction with attention mechanism. The experimental results on the Yelp2013 and Yelp2015 datasets show that the proposed model can effectively improve the performance of sentiment analysis and online review quality prediction compared with the existing neural network models.

Abstract:It is well known that the fragmentation of Android ecosystem has caused severe compatibility issues. Therefore, for Android apps, cross-platform testing (the apps must be tested on a multitude of devices and operating system versions) is particularly important to assure their quality. Although lots of cross-platform testing techniques have been proposed, there are still some limitations: 1) It is time-consuming and error-prone to encode platform-agnostic tests manually; 2) Test scripts generated by existing record/replay techniques are brittle and will crash when replayed on different platforms; 3) Developers, and even test vendors have not equipped with some special Android devices; 4) Due to the lack of specific domain knowledge, the existing test methods cannot generate effective user inputs, resulting in low testing coverage. As a result, apps that have not been fully tested, will lead to many compatibility issues after releasing. To address these limitations, this study proposes AppCheck, a crowdsourced testing service for Android apps. To generate tests that will explore different behavior of the app automatically, AppCheck crowdsources event trace collection over the Internet, and various touch events will be captured when real users interact with the app. The collected event traces are then transformed into device-independent test scripts, and directly replayed on the devices of real users. During the replay, various data (e.g., screenshots and layout information) will be extracted to identify compatibility issues. The empirical evaluation shows that the proposed AppCheck is effective and improves limitations of the state-of-the-art.

Abstract:Modeling visual data onto the SPD (symmetric positive definite) manifold using the SPD matrices has been proven to yield high discriminatory power for many visual classification tasks in the domain of pattern recognition and machine learning. Among them, generalising the sparse representation classification algorithm to the SPD manifold-based visual classification tasks has attracted extensive attention. This study first comprehensively reviews the characteristics of the sparse representation classification algorithm and the Riemannian geometrical structure of the SPD manifold. Then, embedding the SPD manifold into the Reproducing Kernel Hilbert Space (RKHS) via a kernel function. Afterwards, the latent sparse representation model and latent classification model in RKHS has been suggested, respectively. However, the original visual data in RKHS is implicitly described, which is impossible to perform the subsequent dictionary learning. To handle this issue, the Nyström method is utilized to obtain the approximate representations of the training samples in RKHS for the sake of updating the latent dictionary and latent matrix. Finally, the classification results obtained on five benchmarking datasets show the effectiveness of the proposed approach.

Abstract:Visitors tend to choose personalized travel routes. Planning such a route requires a comprehensive consideration of the length and cost of the route, and the points of interest covered by the route. Keyword-aware optimal route query (KOR) is a typical query for this purpose. Processing a KOR consists of preprocessing and route expansion. With the scale of maps of road networks continues to expand, the overhead for preprocessing and the search space for route expansion increase rapidly. The scalability and the real-time responsiveness are hard to guarantee. To alleviate these pain points, an algorithm called keyword-aware optimal route query algorithm on large-scale road networks or KORL is proposed. In the preprocessing stage, KORL reduces memory requirements by partitioning the road network into subgraphs and stores only information about the routes inside and between subgraphs. In the route expansion stage, KORL combines four strategies, namely minimum cost pruning, approximately dominance pruning, global priority expansion, and keyword vertex expansion to efficiently search the approximate optimal solution. The road networks of various regions in the United States are used as experimental datasets and the experiments are run by the computer with 16 G memory. The limitation that existing algorithms can only handle the road network with the number of vertexes less than 25K is broken. Experiments show that KORL has sound scalability.

Abstract:This study proposes a two-layer collaborative approach for privacy protection in consortium blockchain. The proposed approach consists of two layers. 1. Inter-chain privacy protection: such protection approach aims to protect the privacy between different businesses. This approach is realized by separating and storing the data of different businesses. 2. Intra-chain privacy protection: such protection approach is realized by embedding collection field into transaction body to specify the participants of privacy protection. Then, this approach regards the receiving blockchain node as a relay node to synchronize private data. At the same time, the relay node is also responsible to construct a public transaction by replacing the private payload with its hash after which the public transaction will be synchronized to all participants through consensus. Finally, private participant nodes update their private ledgers to achieve intra-chain privacy. To verify the validity of the proposed approach, some experiments are designed to measure the throughput of inter-chain privacy protection and the delay of intra-chain privacy protection. The experimental results show that the privacy protection approach which is combined with coarse-grained inter-chain protection and fine-grained intra-chain protection ensures the considerable performance and satisfies the privacy requirements at the same time. Thus, the proposed approach has made a potential contribution to the privacy and security of blockchain platform.

Abstract:With the increasing scale of the Internet, network management and operations become extremely complex. Intent-based networking (IBN) emerges when network autonomy becomes a major trend of future network. First of all, this paper gives the definition of IBN, and describes the IBN category and architecture in academia and industry. The implementation closed-loop of IBN is also summarized, including intent acquisition, intent translation, policy verification, intent distribution and execution, real-time feedback and optimization. Then, key technologies of IBN implementation are elaborated in detail according to the IBN closed-loop. In addition, examples are given to illustrate the IBN-based applications from the aspects of network measurement and network service orchestration. Finally, the future research work is prospected and the whole paper is concluded.

Abstract:Medical image segmentation is a key technology in computer aided diagnosis. As a widespread eye disease, glaucoma may cause permanent loss in vision and its screening and diagnosis requires accurate segmentation of optic cup and disc from fundus images. Most traditional computer vision methods segment optic cup and disc with artificial features lead to limited generalization ability. While the end-to-end learning models based on convolutional neural networks focus on optic disc and cup segmentation using automatically detected features, but fail to tackle the lack of labeled samples, thus the segmentation performance is still barely satisfactory. This study proposes an effective two-stage optic disc and cup segmentation method based on semi-supervised conditional generative adversarial nets, namely CDR- GANs. Each stage builds upon three players—A segmentation net, a generator, and a discriminator, where the segmentation net and generator concentrate on learning the conditional distributions between fundus images and their corresponding segmentation maps, and the discriminator distinguishes whether the image-label pairs come from the empirical joint distribution. The extensive experiments show that the proposed method achieves state-of-the-art optic cup and disc segmentation results on ORIGA dataset.

Abstract:With the development of heterogeneous computing technology, heterogeneous fusion processors, such as CPU-GPU integrated processors, have been fully developed in recent years, and arouse attention from both academia and industry. The fusion of different devices has several advantages. For example, all devices share the same memory and can have fine-grained cooperation. However, many system programming challenges and optimization challenges have emerged. To take full advantage of the capacity of heterogeneous fusion processors, it is needed to utilize features of heterogeneous fusion processors such as shared memory, and to perform architecture optimizations to different devices according to different applications. The research work related to heterogeneous fusion processors is first analyzed and summarized. Second, the related work about performance analysis is introduced. Third, the optimizations on heterogeneous fusion processors are summarized. A summarization for the applications that utilize heterogeneous fusion processors is also provided. At last, the future directions are provided on heterogeneous fusion processors and conclusion is given.