Search

While multi-discriminators have been recently exploited to enhance the discriminability and diversity of Generative Adversarial Networks (GANs), these independent discriminators may not collaborate harmoniously to learn diverse and complementary decision boundaries. This paper extends the original two-player adversarial game of GANs by introducing a new multi-player objective named Discriminator Discrepancy Loss (DDL) for diversifying the multi-discriminators. Besides the competition between the generator and each discriminator, there are also competitions between the discriminators: 1) When training multi-discriminators, we simultaneously minimize the original GAN loss and maximize DDL, seeking a good trade-off between the accuracy and diversity. This yields diversified multi-discriminators that fit the generated data distribution to the real data distribution from more comprehensive perspectives. 2) When training the generator, we minimize DDL to encourage the generator to confuse all discriminators. This enhances the diversity of the generated data distribution. Further, we propose a layer-sharing network architecture for the multi-discriminators, which allows them to learn from distinct perspectives about the shared low-level features through better collaboration. It also makes our model more lightweight than existing multi-discriminators approaches. Our DDL-GAN remarkably outperforms other GANs over five standard datasets for image generation tasks.

Precise pointer analysis is desired since many program analyses benefit from it both in precision and performance. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. The more dimensions a pointer analysis considers, the more accurate its results will be. However, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced. This paper presents a flow, context, field and quasi path sensitive pointer analysis algorithm for C programs. Our algorithm runs on a control flow automaton, a key structure for our analysis to be flow sensitive. During the analysis process, we use function summaries to get context information. Elements of aggregate structures are handled to improve precision. We collect path conditions to filter unreachable paths and make all points-to relations gated. For efficiency, we propose a multi-entry mechanism. The algorithm is implemented in TsmartGP, which is an extension of CPAchecker. Our algorithm is compared with some state-of-the-art algorithms and TsmartGP is compared with cppcheck and Clang Static Analyzer by detecting uninitialized pointer errors in 13 real-world applications. The experimental results show that our algorithm is more accurate and TsmartGP can find more errors than other tools.

With the fast-growing of fleet size and the railway mileage, the energy consumption of trains is becoming a serious concern globally. The nature of railway offers a unique opportunity to optimize the energy efficiency of engines by the aid of various landforms along railway lines. However, because of the feature of non-linearity, high-dimension, complicated-constraint and time-variant, it is difficult to get the optimal train-driving scheme that saves the most energy. This paper proposes a dexterously augmented CNN model called sequential CNN(S-CNN) to generate automatic train-driving schemes. Forward and backward features are defined to depict the context of the running train and they are processed separately in the input layer. Operations of experienced train drivers are used for the CNN model training. The S-CNN model takes both the time-series and space-series into consideration and pays attention to their ordinal attributes. The proposed techniques are validated in a Hardware-in-Loop platform using realistic data. Experimental results proved that the driving operations obtained by S-CNN model are very similar to experienced human drivers and it saves more than 10% energy when compared with the average performance of human drivers.

Precise pointer analysis is desired since it is a core technique to find memory defects. There are several dimensions of pointer analysis precision, flow sensitivity, context sensitivity, field sensitivity and path sensitivity. For static analysis tools utilizing pointer analysis, considering all dimensions is difficult because the trade-off between precision and efficiency should be balanced.This paper presents TsmartGP, a static analysis tool for finding memory defects in C programs with a precise and efficient pointer analysis. The pointer analysis algorithm is flow, context, field, and quasi path sensitive. Control flow automatons are the key structures for our analysis to be flow sensitive. Function summaries are applied to get context information and elements of aggregate structures are handled to improve precision. Path conditions are used to filter unreachable paths. For efficiency, a multi-entry mechanism is proposed. Utilizing the pointer analysis algorithm, we implement a checker in TsmartGP to find uninitialized pointer errors in 13 real-world applications. Cppcheck and Clang Static Analyzer are chosen for comparison. The experimental results show that TsmartGP can find more errors while its accuracy is also higher than Cppcheck and Clang Static Analyzer. The demo video is available at https://youtu.be/IQlshemk6OA.

With the rapid development of intelligent vehicles, more and more researchers are paying attention to their security issues. This paper considers a vehicle system with multiple sensors measuring the same physical variable. Some of these sensors may be maliciously attacked, resulting in the system being unable to work properly. This paper mainly addresses the detection and identification of malicious attacks on sensors in the presence of transient faults. Although there are some solutions at present, the existing methods can hardly capture attacks when a professional attacker manipulates the sensor output very slightly or infrequently. To address this problem, we design a resilient sensor attack detection algorithm. This algorithm adds an additional virtual sensor to the system and builds a fault model for each sensor, and using the pairwise inconsistencies between the sensors to detect the attack. To improve the detection rate in the presence of transient faults, we consider the system dynamics model and incorporates historical measurements into the detection algorithm. In addition, we propose a method to select transient fault model parameters to obtain a more accurate sensor fault model in a dynamic environment. Finally, this paper obtains real experimental data from the EV3 platform to verify the algorithm. Experimental results show that the proposed method is more robust and can detect and identify more attacks. Especially for stealth attacks which are extremely difficult to detect, the detection rate and recognition rate are increased by about 90%.

State-of-the-art fuzzers implement various optimizations to enhance their performance. As the optimizations reside in different stages such as input seed selection and mutation, it is tempting to combine the optimizations in different stages. However, our initial attempts demonstrate that naive combination actually worsens the performance, which explains that most optimizations are still isolated by stages and metrics. In this paper, we present InteFuzz, the first framework that synergically integrates multiple fuzzing optimizations. We analyze the root cause for performance degradation in naive combination, and discover optimizations conflict in coverage criteria and optimization granularity. To resolve the conflicts, we propose a novel priority-based scheduling mechanism. The dynamic integration considers both branch-based and block-based coverage feedbacks that are used by most fuzzing optimizations. In our evaluation, we extract four optimizations from popular fuzzers such as AFLFast and FairFuzz and compare InteFuzz against naive combinations. The evaluation results show that InteFuzz outperforms the naive combination by 29% and 26% in path-and branch-coverage. Additionally, InteFuzz triggers 222 more unique crashes, and discovers 33 zero-day vulnerabilities in real-world projects with 12 registered as CVEs.

Cryptographic hash functions have become the basis of modern network computing for identity authorization and secure computing; protocol consistency of cryptographic hash functions is one of the most important properties that affect the security and correctness of cryptographic implementations, and protocol consistency should be well proven before being applied in practice. Software verification has seen substantial application in safety-critical areas and has shown the ability to deliver better quality assurance for modern software; thus, applying software verification to a protocol consistency proof for cryptographic hash functions is a reasonable approach to prove their correctness. Verification of protocol consistency of cryptographic hash functions includes modeling of the cryptographic protocol and program analysis of the cryptographic implementation; these require a dedicated cryptographic implementation model that preserves the semantics of the code, efficient analysis of cryptographic operations on arrays and bits, and the ability to verify large-scale implementations. In this paper, we propose a fully automatic software verification framework, VeriHash, that brings software verification to protocol consistency proofs for cryptographic hash function implementations. It solves the above challenges by introducing a novel cryptographic model design for modeling the semantics of cryptographic hash function implementations, extended array theories for analysis of operations, and compositional verification for scalability. We evaluated our verification framework on two SHA-3 cryptographic hash function implementations: the winner of the NIST SHA-3 competition, Keccack; and an open-source hash program, RHash. We successfully verified the core parts of the two implementations and reproduced a bug in the published edition of RHash.

Cyber-physical systems (CPSs) are built from, and depend upon, the seamless integration of software and hardware components. The most important challenge in CPS design and verification is to design CPS to be reliable in a variety of uncertainties, i.e., unanticipated and rapidly evolving environments and disturbances. The costs, delays and reliability of the designed CPS are highly dependent on software-hardware partitioning in the design. The key challenges in partitioning CPSs is that it is difficult to formalize reliability characterization in the same way as the uncertain cost and time delay. In this paper, we propose a new CPS design paradigm for reliability assurance while coping with uncertainty. To be specific, we develop an uncertain programming model for partitioning based on the uncertainty theory, to support the assured reliability. The uncertainty effect of the cost and delay time of components to be implemented can be modeled by the uncertainty variables with uncertainty distributions, and the reliability characterization is recursively derived. We convert the uncertain programming model and customize an improved heuristic to solve the converted model. Experiment results on some benchmarks and random graphs show that the uncertain method produces the design with higher reliability. Besides, in order to demonstrate the effectiveness of our model for in coping with uncertainty in design stage, we apply this uncertain framework and existing deterministic models in the design process of a sub-system that is used in real world subway control. The system implemented based on the uncertain model works better than the result of deterministic models. The proposed design paradigm has the potential to be generalized to the design of CPSs for greater assurances of safety and security under a variety of uncertainties

The Ethereum ecosystem has introduced a pervasive blockchain platform with programmable transactions. Everyone is allowed to develop and deploy smart contracts. Such flexibility can lead to a large collection of similar contracts, i.e., clones, especially when Ethereum applications are highly domain-specific and may share similar functionalities within the same domain, e.g., token contracts often provide interfaces for money transfer and balance inquiry. While smart contract clones have a wide range of impact across different applications, e.g., security, they are relatively little studied. Although clone detection has been a long-standing research topic, blockchain smart contracts introduce new challenges, e.g., syntactic diversity due to trade-off between storage and execution, understanding high-level business logic etc.. In this paper, we highlighted the very first attempt to clone detection of Ethereum smart contracts. To overcome the new challenges, we introduce the concept of smart contract birthmark, i.e., a semantic-preserving and computable representation for smart contract bytecode. The birthmark captures high-level semantics by effectively sketching symbolic execution traces (e.g., data access dependencies, path conditions) and maintain syntactic regularities (e.g., type and number of instructions) as well. Then, the clone detection problem is reduced to a computation of statistical similarity between two contract birthmarks. We have implemented a clone detector called EClone and evaluated it on Ethereum. The empirical results demonstrated the potential of EClone in accurately identifying clones. We have also extended EClone for vulnerability search and managed to detect CVE-2018-10376 instances.

Libraries offer reusable functionality through application programming interfaces (APIs) with usage constraints such as call conditions and orders. Constraint violations, i.e., API misuses, commonly lead to bugs and even security issues. In this paper, we introduce IMChecker, a constraint-directed static analysis toolkit to vet API usages in C programs powered by a domain-specific language (DSL) to specify the API usages. First, we propose a DSL, which covers most API usage constraint types and enables straightforward but precise specification by studying real-world API-misuse bug patches. Then, we design and implement a static analysis engine to automatically parse specifications into checking targets, identify potential API misuses and prune the false positives with rich semantics. We have instantiated IMChecker for C programs with user-friendly graphic interfaces and evaluated the widely used benchmarks and real-world projects. The results show that IMChecker outperforms 4.78--36.25% in precision and 40.25--55.21% w.r.t. state-of-the-arts toolkits. We also found 75 previously unknown bugs in Linux kernel, OpenSSL and applications of Ubuntu, 61 of which have been confirmed by the corresponding development communities. Video: https://youtu.be/YGDxeyOEVIM Repository: https://github.com/tomgu1991/IMChecker

Static analysis is an effective way of checking memory safety issues in program. Usually, multiple analysis algorithms usually run together to achieve a precise analysis result. In this paper, a novel analysis frame work over access path is presented for incorporating analysis algorithms. A pointer analysis based on access path works as a base layer, alias and pointer information are automatically handled. An summary based checking algorithm is designed for checking real world project. Moreover, the framework is fully extensible and various analysis can be added as plugins. Experimental results show that our method has good precision on Juliet Test Suite and scales to large software.

Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. What's more, TSV with auto selection achieves a better balance of accuracy, time and memory consumption.

Integer errors in C/C++ are caused by arithmetic operations yielding results which are unrepresentable in certain type. They can lead to serious safety and security issues. Due to the complicated semantics of C/C++ integers, integer errors are widely harbored in real-world programs and it is error-prone to repair them even for experts. An automatic tool is desired to 1) automatically generate fixes which assist developers to correct the buggy code, and 2) provide sufficient hints to help developers review the generated fixes and better understand integer types in C/C++. In this paper, we present a tool IntPTI that implements the desired functionalities for C programs. IntPTI infers appropriate types for variables and expressions to eliminate representation issues, and then utilizes the derived types with fix patterns codified from the successful human-written patches. IntPTI provides a user-friendly web interface which allows users to review and manage the fixes. We evaluate IntPTI on 7 real-world projects and the results show its competitive repair accuracy and its scalability on large code bases. The demo video for IntPTI is available at: https://youtu.be/9Tgd4A_FgZM.

Building language models for source code enables a large set of improvements on traditional software engineering tasks. One promising application is automatic code completion. State-of-the-art techniques capture code regularities at token level with lexical information. Such language models are more suitable for predicting short token sequences, but become less effective with respect to long statement level predictions. In this paper, we have proposed PCC to optimize the token level based language modeling. Specifically, PCC introduced an intermediate representation (IR) for source code, which puts tokens into groups using lexeme and variable relative order. In this way, PCC is able to handle long token sequences, i.e., group sequences, to suggest a complete statement with the precise synthesizer. Further more, PCC employed a fuzzy matching technique which combined genetic and longest common sub-sequence algorithms to make the prediction more accurate. We have implemented a code completion plugin for Eclipse and evaluated it on open-source Java projects. The results have demonstrated the potential of PCC in generating precise long statement level predictions. In 30%-60% of the cases, it can correctly suggest the complete statement with only six candidates, and 40%-90% of the cases with ten candidates.

When analyzing programs using static program analysis, we need to determine the reachability of each possible execution path of the programs. Many static analysis tools collect constraints of each path and use SMT solvers to determine the satisfiability of these constraints. The accumulated computing time can be long if we use SMT solvers too many times. In this paper, we propose a constraint-pattern based method for reachability determination to address the limitation of current approaches. We define some constraint-patterns. For each pattern, a carefully designed constraints solving algorithm is presented. Our method contains two steps. Firstly, we collect some information about the constraints in the program to be analyzed. Then we choose the most suitable algorithm for reachability determination based on the information. Secondly, we apply the algorithm in analysis process to speed up satisfiability checking of path constraints. We implement our method based on CPAchecker, a famous software verification tool. The experimental results on some well-known benchmarks show that, with a moderate accuracy, our method is more efficient in comparison with some state-of-the-art SMT solvers.

Formal program verification is a powerful technique to ensure the correctness of programs. To perform this technique, one oftentimes needs to manually specify assertions, which is a time-consuming and error-prone task. Generating assertions automatically can significantly improve the usability of formal program verification. To decide where an assertion is needed heavily and which value range of the variable should be checked are the most challenging parts of assertion recommendation. This paper proposes the first assertion recommendation approach for program verification. With the help of machine learning techniques, the approach automatically decides whether a program function needs to add assertions. If an assertion is needed, the approach automatically recommends a variable that is most likely to occur in this assertion. Meanwhile, a value range of the variable is suggested. Our method of assertion recommendation has been integrated into Ceagle Online (a program verifier) and evaluated on the benchmarks of SV-COMP and CProver. Our best performance in assertion necessity classification can reach 92.1192% accuracy rate, 84.2281% precision rate and 86.8512% recall rate.

Program obfuscation is a common practice in software development to obscure source code or binary code, in order to prevent humans from understanding the purpose or logic of software. It protects intellectual property and deters malicious attacks. While tremendous efforts have been devoted to the development of various obfuscation techniques, we have relatively little knowledge on how to most effectively use them together. The biggest challenge lies in identifying the most effective combination of obfuscation techniques. This paper presents a unified framework to optimize program obfuscation. Given an input program P and a set T of obfuscation transformations, our technique can automatically identify a sequence seq = 〈t2, t2, ... , tn〉 (∀i e [1, n]. ti e T), such that applying ti in order on P yields the optimal obfuscation performance. We model the process of searching for seq as a mathematical optimization problem. The key technical contributions of this paper are: (1) an obscurity language model to assess obfuscation effectiveness/optimality, and (2) a guided stochastic algorithm based on Markov chain Monte Carlo methods to search for the optimal solution seq. We have realized the framework in a tool Closure* for JavaScript, and evaluated it on 25 most starred JavaScript projects on GitHub (19K lines of code). Our machinery study shows that Closure* outperforms the well-known Google Closure Compiler by defending 26% of the attacks initiated by JSNice. Our human study also reveals that Closure* is practical and can reduce the human attack success rate by 30%.

Integer errors in C program may lead to serious failures and vulnerabilities. They are harbored in a wide range of programs including mature software such as Linux kernel. Code reviewing is laborious and cannot guarantee reliable fixes for errors. Addressing potential errors in the development phase is error-prone even for experts and essentially hinders developing efficiency. In this paper we propose a novel approach to automate fix for C integer errors. Our approach directly replaces original C integers with dynamic-precision integers to fix potential errors without detecting them in advance. Many errors can be fixed by precision improvement without changing the design of application. We implement a tool CIntFix to automatically fix C integer errors. CIntFix succeeds in fixing all 5414 programs in NIST's Juliet test suite from 7 weakness categories. Meanwhile, on Juliet test suite and SPEC CINT2000 benchmarks, CIntFix processes C source code at the rate of 0.157s/KLOC and the fixed programs have 18.0% slowdown on average. The results show that CIntFix is capable to fix integer errors in real-world C programs.

PLC (Programmable Logic Controller) program in automatic control is vital to this kind of safety-critical applications. In this paper, we present a useful method of compositional model checking for verification of PLC programs. The method is based on the work pattern and the system model of PLC for modelling PLC program. Because the state space explosion problem limits the use of general model checking in real PLC programs, the paper firstly defines the framework and the mechanism of model combination based on the module of PLC program. Then the paper proposes a series of PLC domain specific strategies for compositional model checking between two modules. Through two modules' combination is verified at a time in a PLC program, cyclic stacking combination of the modules can be verified by the recursive operation of compositional checking for the whole program. The strategies can effectively reduce state space by means of hierarchical module model and recursion state transfer. The validity of our method is illustrated by an example.

The control sequence optimization problem is difficult to solve due to its high nonlinearity, various constraints and the possible changes in the sequence of comprising elements at any instant of time. The optimization of train trip running profile is a typical control sequence optimization problem, whose optimization object is to minimize the energy consumption as well as the time deviation under various constraints. Engineers always have to face the trade-off between the optimization performance and calculation time for an onboard control system for such problems. This paper mainly proposed a framework of an offline to onboard system solution for control sequence optimization problems, specifically using on the train trip profile optimization problems. The framework choose the parameter-decision tree solution for the onboard control system, and then a series of offline procedures including sequence mining, optimal computation, and machine learning is proposed for getting the parameter-decision tree. The framework inherits the good optimization performance of offline systems, as well as guaranteed the onboard calculation time for real-time control. Performance on using such a framework for solving train trip profile optimization problems is shown in the literature, which shows the potentials of using such frameworks on solving related control sequence optimization problems.

Fault localization is a critical procedure in software development process. Previous studies based their research on the precondition that test results are conveniently acquired and 100% correct, which does not happen in the real world. In this article, we propose the concept of gamma-reliable test-suite to demonstrate the potential unreliability of test results. By modeling this unreliability using Dempster-Shafer theory, we managed to pin down the faults under the new situation. Experiments were conducted on both 100%-reliable and partial-reliable Siemens Test Suite and compared against several known spectrum-based localization algorithms, namely Naish1, Naish2, Binary, Wong1 and RusselaRao. The results proved the prior performance of our approach. We conclude that fault localization problem is more precisely modeled by Dempster-Shafer theory than common statistical theory.

In real-time embedded applications, interrupt-driven systems are widely adopted due to strict timing requirements. However, development of interrupt-driven systems is time-consuming and error-prone. To conveniently ensure a trustworthy system design and implementation is a challenging problem, especially in complex applications. In this paper, we present a novel domain-specific language called iDola to model interrupt-driven systems declaratively and concisely. A major strength of iDola is the feasibility to capture complex interrupt handling mechanism in real-time operating systems and target platforms, such as delayed service and buffered processing. We also propose the formal operational semantics and code generation algorithm of iDola, so that iDola models can be transformed to timed automata for verification and loaded to generate platform-specific codes. We apply iDola on the modeling of an industrial interrupt-driven system, multifunction vehicle bus controller which runs in an embedded environment with eCos operating system. Based on iDola, the system is modeled with a dispatcher which embodies advanced interrupt handling in eCos, including buffered interrupt service routine and deferred service routine. Through transformation, the system design is verified and design bugs are detected. Code generation is also executed using the proposed algorithm. Generated codes display comparatively equal performance in the real system. We believe iDola can facilitate building a trustworthy interrupt-driven system.

Temporal induction is one of the most popular SAT-based model checking techniques. It consists of two parts, the base case and the induction step. With the search length increment, both parts generate a sequence of SAT problems. This paper focuses on learnt clause replication and reuse in incremental temporal induction. Firstly, with the aid of assumption literals, we present an alternative clause replication scheme, which is much easier to implement than existing works. Secondly, based on our clause replication scheme, we present several clause reuse schemes to maximally explore the learnt clauses and their replications in temporal induction. Based on above ideas, we propose two new incremental temporal induction algorithms. Experimental results on a large number of benchmarks show significant performance improvement of our technique.

The correctness verification of embedded control software has become an important research topic in embedded system field. The paper analyses the present situation on correctness verification of control software as well as the limitations of existing technologies. In order to the high reliability and high security requirements of control software, the paper proposes a hierarchical framework and architecture of control software (PLC program) verification. The framework combines the technologies of testing, model checking and theorem proving. The paper introduces the construction, flow and key elements of the architecture.

The correctness of PLC (Programmable Logic Controller) program in automatic control is vital to this kind of safety-critical applications. In this paper, we present a useful method of combinational testing for correctness of PLC programs. The method is based on the denotational semantics of PLC program and the semantic functions for basic instructions. It establishes the definition of denotational semantics for PLC program. The function of denotational semantics is defined by extended λ-calculus. It analyses adaptive problems of various tests for PLC embedded software and proposes a combinational testing framework based on simulation mechanism. The equivalent transforming module of PLC program is defined by means of test module composed with high-level language code segments, which have equivalent denotational semantics and partly include program diagnostic information. The framework can decompose a PLC program test into some small tests, and solve the test problem under the condition of boundary and utmost or no environment supporting. The validity of our method is shown by one example of experiments.

Visual domain adaptation, which learns an accurate classifier for a new domain using labeled images from an old domain, has shown promising value in computer vision yet still been a challenging problem. Most prior works have explored two learning strategies independently for domain adaptation: feature matching and instance reweighting. In this paper, we show that both strategies are important and inevitable when the domain difference is substantially large. We therefore put forward a novel Transfer Joint Matching (TJM) approach to model them in a unified optimization problem. Specifically, TJM aims to reduce the domain difference by jointly matching the features and reweighting the instances across domains in a principled dimensionality reduction procedure, and construct new feature representation that is invariant to both the distribution difference and the irrelevant instances. Comprehensive experimental results verify that TJM can significantly outperform competitive methods for cross-domain image recognition problems.

A large amount of heterogeneous event data are increasingly generated, e.g., in online systems for Web services or operational systems in enterprises. Owing to the difference between event data and traditional relational data, the matching of heterogeneous events is highly non-trivial. While event names are often opaque (e.g., merely with obscure IDs), the existing structure-based matching techniques for relational data also fail to perform owing to the poor discriminative power of dependency relationships between events. We note that interesting patterns exist in the occurrence of events, which may serve as discriminative features in event matching. In this paper, we formalize the problem of matching events with patterns. A generic pattern based matching framework is proposed, which is compatible with the existing structure based techniques. To improve the matching efficiency, we devise several bounds of matching scores for pruning. Since the exploration of patterns is costly and incrementally, our proposed techniques support matching in a pay-as-you-go style, i.e., incrementally update the matching results with the increase of available patterns. Finally, extensive experiments on both real and synthetic data demonstrate the effectiveness of our pattern based matching compared with approaches adapted from existing techniques, and the efficiency improved by the bounding/pruning methods.

Transfer learning is established as an effective technology in computer vision for leveraging rich labeled data in the source domain to build an accurate classifier for the target domain. However, most prior methods have not simultaneously reduced the difference in both the marginal distribution and conditional distribution between domains. In this paper, we put forward a novel transfer learning approach, referred to as Joint Distribution Adaptation (JDA). Specifically, JDA aims to jointly adapt both the marginal distribution and conditional distribution in a principled dimensionality reduction procedure, and construct new feature representation that is effective and robust for substantial distribution difference. Extensive experiments verify that JDA can significantly outperform several state-of-the-art methods on four types of cross-domain image classification problems.

The train control system is a safety-critical embedded system. In this system, all buses and devices share the real time communication protocol, which is described in the standard IEC 61375. Many systems that comply the standard have been implemented and used in the real world railway, however, their safety checking is highly nontrivial. In this paper, we focus on the formal verification and implementation of the protocol described in the standard. The protocol is modeled as a network of timed automata, which are synchronized to describe the procedure of connection establishment and data transmission among vehicles. The stochastic factors such as time delay and packet loss are modeled in the channel module. Afterwards, we abstract some safety critical properties that are important to guarantee the correctness of the protocol. These properties are verified with the model checker Uppaal. Two properties are violated in the verification, and two corresponding bugs in the standard are fixed and proposed to the IEC. In order to prove the bugs we find, we implement two versions of the standard. The first is for the original description of the standard, and the second is for our fixed description. Both versions are tested with the D113 (a widely used general Multifunction Vehicle Bus control system implemented by the Duagon company), and we find that the second version works well, while the first fails. The second version for the fixed protocol is now used in the real world subway.

Sparse coding learns a set of basis functions such that each input signal can be well approximated by a linear combination of just a few of the bases. It has attracted increasing interest due to its state-of-the-art performance in BoW based image representation. However, when labeled and unlabeled images are sampled from different distributions, they may be quantized into different visual words of the codebook and encoded with different representations, which may severely degrade classification performance. In this paper, we propose a Transfer Sparse Coding (TSC) approach to construct robust sparse representations for classifying cross-distribution images accurately. Specifically, we aim to minimize the distribution divergence between the labeled and unlabeled images, and incorporate this criterion into the objective function of sparse coding to make the new representations robust to the distribution difference. Experiments show that TSC can significantly outperform state-of-the-art methods on three types of computer vision datasets.

Embedded systems are becoming increasingly popular due to their widespread applications and the reliability of them is a crucial issue. The complexity of the reliability analysis arises in handling the sequential feedback that make the system output depends not only on the present input but also the internal state. In this paper, we propose a novel probabilistic model, named sequential dependency model (SDM), for the reliability analysis of embedded systems with sequential feedback. It is constructed based on the structure of the system components and the signals among them. We prove that the SDM model is s Dynamic Bayesian Network (DBN) that captures: the spatial dependencies between system components in a single time slice, the temporal dependencies between system components of different time slices, and the temporal dependencies due to the sequential feedback. We initiate the conditional probability distribution (CPD) table of the SDM node with the failure probability of the corresponding system component. Then, the SDM model handles the spatial-temporal correlations at internal components as well as the higher order temporal correlations due to the sequential feedback with the computational mechanism of DBN, experiment results demonstrate the accuracy of our model.

Embedded systems are becoming increasingly popular due to their widespread applications. Hardware/software partitioning is becoming one of the most crucial steps in the design of embedded systems. The costs and delays of the final results of a design will strongly depend on partitioning. In this paper, we propose an uncertain programming model for partitioning problems. The delay related constraints and the cost related objective are modeled by uncertain variables with uncertainty distributions. We convert the uncertain programming model to a deterministic model and solve the converted model by an efficient heuristic method. We propose a heuristic based on genetic algorithm and simulated annealing to solve the problem near-optimally, even for quite large systems. Experiment results show that the proposed model and algorithm produce quality partitions.

International audience; Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper shows the modeling and validation work of a typical PLC control system using the Behavior-Interaction-Priority(BIP) component framework. The gate control system based on PLC is a real industry application. We design general system architecture for this kind of device control system. The control software and hardware of environment are all modeled as BIP components. Their interactions are described by BIP connectors. System requirements are formalized as monitors. Simulation is applied on the system model. We found a couple of design errors in simulation, which help us to improve the dependability of the original systems.

In this work, we address the problem of distributed expert finding using chains of social referrals and profile matching with only local information in online social networks. By assuming that users are selfish, rational, and have privately known cost of participating in the referrals, we design a novel truthful efficient mechanism in which an expert-finding query will be relayed by intermediate users. When receiving a referral request, a participant will locally choose among her neighbors some user to relay the request. In our mechanism, several closely coupled methods are carefully designed to improve the performance of distributed search, including, profile matching, social acquaintance prediction, score function for locally choosing relay neighbors, and budget estimation. We conduct extensive experiments on several data sets of online social networks. The extensive study of our mechanism shows that the success rate of our mechanism is about 90 percent in finding closely matched experts using only local search and limited budget, which significantly improves the previously best rate 20 percent. The overall cost of finding an expert by our truthful mechanism is about 20 percent of the untruthful methods, e.g., the method that always selects high-degree neighbors. The median length of social referral chains is 6 using our localized search decision, which surprisingly matches the well-known small-world phenomenon of global social structures.

We present a fast collision detection method for deformable surfaces with parallel spatial hashing on GPU architecture. The efficient update and access of the uniform grid are exploited to accelerate the performance in our method. To deal with the inflexible memory system, which makes the building of stream data a challenging task on GPU, we propose to subdivide the whole workload into irregular segments and design an efficient evaluation algorithm, which employs parallel scan and stream compaction, to build the stream data in parallel. The load balancing is a key aspect that needs to be considered in the SIMD parallelism. We break the heavy and irregular collision computation down into lightweight part and heavyweight part, ensuring the later perfectly run in load balancing manner with each concurrent thread processes just a single collision. In practice, our approach can perform collision detection in tens of milliseconds on a PC with NVIDIAGTX 260 graphics card on benchmarks composed of millions of triangles. The results highlight our speedups over prior CPU-based and GPU-based algorithms.

A software cloud is ready-made for software delivery or Software as a Service (SaaS). As it becomes more and more popular, security problems of software running in the cloud also become an important issue. The threats, such as destroying system softwares and access violation, are frequently emerging in the field of software cloud. In this paper, we propose a watermark-aware trusted running environment to protect the softwares running in the cloud. We implement the scheme which mainly contains two parts: 1) embedding watermark into the Java programs running in the cloud; 2) generating customized JVMs for recognizing the watermarked programs. Experimental results within a real private software cloud to demonstrate that our approach can provide a large-scale protection with a small overhead.

N-sided hole filling plays an important role in vertex blending. Piegl and Tiller presented an algorithm to interpolate the given boundary and cross-boundary derivatives in B-spline form. To deal with the incompatible cases that their algorithm cannot handle, we propose an extension method to manipulate the transition between sharp and rounded features. The algorithm first patches n crescent-shaped extended surfaces to the boundary with G2 continuity to handle incompatibility problem in the corners. Then, we compute the inner curves and the corresponding cross-boundary derivatives fulfilling tangent and twist compatibilities. The generated B-spline Coons patches are G1-continuously connected exactly, and have epsilon-G1 continuity with the extended surfaces. Our method improves the continuity-quality of the shape and reduces the count of the inserted knots. It can be applied to all G0-continuous boundary conditions without any restrictions imposed on the boundary or cross-boundary derivatives. It generates better shapes than some popular industrial modeling systems on these incompatible occasions. Some examples underline its feasibility.

Sectional views are widely used in engineering practice due to their clear and concise expression. However, it is difficult for computers to understand because of the large numbers of omitted entities and their diversified representations. This paper aims at reconstructing 3D models from 2D sectional views by improving the traditional volume based method. First, we present a two-stage loop searching algorithm to extract desired loops from sectional views. Then, sub-objects are identified by the hint-based feature identification algorithm with an intuitive loop-matching criterion. After that, a model-directed algorithm is proposed to guide the generation of sub-objects which are assembled together to form the final objects. The algorithm can handle full sections, partial sections and offset sections, as well as orthographic views. Multiple sectional views are supported in our algorithm. Moreover, the domain of objects is extended to inclined quadric surfaces and intersecting quadric surfaces with higher order curves. Experiment results show its practicability.

According to testing embedded real-time software (ERTS) of programmable logic controller (PLC), the paper summarizes the present researches of PLC ERTSpsila test. It analyses concretely the technologies including static test or verification, testing in real environment and simulation environment, and testing by hardware checker or code instrumentation. An agent-oriented software testing model is presented for solving the existing problems of these methods in testing PLC ERTS. The architecture of the model is introduced from structure, frame and work pattern. Based on the model the automatic test of PLC ERTS can be realized in simulation environment.

This paper presents a new VQ encoding method using a dynamically constructed mixed pyramid for fast image compression. Our method enhances the speed of VQ encoding by allowing the "nearest" codeword of an input block to be identified without computing the Euclidean distances between the input block and all codewords. Our method is based on, and enhanced from, two recently proposed methods based on mixed pyramid data structure and dynamically constructed subvectors, respectively. Experimental results demonstrated that our method is more efficient than the previous two methods.

Remote user authentication is important to protect web-based services offered over the Internet. The use of smart cards was proposed to avoid the storage of password table in the server. Further protection of user information in the smart cards can be done by imposing a fingerprint verification mechanism. The Lee, Ryu and Yoo (LRY) scheme which provides both smart card based authentication and fingerprint verification is found to be vulnerable to various attacks. This paper proposed an improvement to the LRY scheme which is able to withstand the attacks of the LRY scheme.

The performance of a given cache architecture is largely determined by the behavior of the application using the cache. Reconfigurable cache is an effective low-power technique. Using the technique, microprocessor's cache can be configured dynamically to adapt itself to the requirement of running program, and minimize the energy consumption and performance loss. We introduce a phase-based self-tuning algorithm (PBSTA), which can automatically, transparently, and dynamically manage the reconfigurable cache on a per-phase basis. In contrast with previous works, the algorithm seeks not only to lower the cache's energy consumption effectively, but also reduce the performance loss due to unnecessary reconfigurations. By simulating numerous MiBench benchmarks, the results show that the PBSTA, when applied to reconfigurable cache, saves on average 40% of total memory access energy compared with a conventional cache and the associated performance loss is close to 1.8%.

A new rest generation method of fully scanned or combinational circuits is proposed for complete coverage of path delay faults based on single stuck-at tests. The proposed method adds the target path into the original circuit, where all off inputs of the path are connected with corresponding nodes in the original circuit. Test generation of the path delay fault is reduced to that of the single stuck-at fault at the fanout branch, where the additional path connects with its source node in the original circuit. A disjoint dynamic test compaction scheme is proposed to reduce the size of the test set in the process of test generation. A conjoint test compaction scheme is proposed based on fanout counts of the paths. The proposed method presents a very compact test set for complete coverage of robustly and non-robustly testable path delay faults.

Role-based access control (RBAC) models have been successfully implemented in various information systems in recent years. However, the traditional centralized authorization and administration mechanisms in RBAC have several drawbacks in collaborative environments. In this paper, we propose a distributed Domain Administration of RBAC Model, DARBAC, in which the authorization and administration privileges are distributed to multiple administrative domains. Each administrative role is assigned to an administrative domain and can only execute administrative operations within its domain. By introducing the concept of administrative domain and administrative role hierarchy, the DARBAC model can flexibly meet the access control requirements in collaborative environments. We also describe how to implement the model in the PLM product and how to apply the model in a distributed enterprise environment to support cooperative work.

This paper proposes an effective data mining technique for finding useful patterns in streaming sequences. At present, typical approaches to this problem are to search for patterns in a fixed-size window sliding through the stream of data being collected. The practical values of such approaches are limited in that, in typical application scenarios, the patterns are emerging and it is difficult, if not impossible, to determine a priori a suitable window size within which useful patterns may exist. It is therefore desirable to devise techniques that can identify useful patterns with arbitrary window sizes. Attempts to this problem are challenging, however, because it requires a highly efficient searching in a substantially bigger solution space. This paper presents a new method which includes firstly a pruning strategy to reduce the search space and secondly a mining strategy that adopts a dynamic index structure to allow efficient discovery of emerging patterns in a streaming sequence. Experimental results on real data and synthetic data show that the proposed method outperforms other existing schemes both in computational efficiency and effectiveness in finding useful patterns.

A few faulty nodes can make an n-dimensional mesh or torus network unsafe for fault-tolerant routing methods based on the block fault model, where the whole system (n-dimensional space) forms a fault block. A new concept, called extended local safety information in meshes or tori, is proposed to guide fault-tolerant routing, and classifies fault-free nodes inside 2-dimensional planes. Many nodes globally marked as unsafe become locally enabled inside 2-dimensional planes. A fault-tolerant routing algorithm based on extended local safety information is proposed for k-ary n-dimensional meshes/tori. Our method does not need to disable any fault-free nodes, unlike many previous methods, and this enhances the computational power of the system and improves performance of the routing algorithm greatly. All fault blocks are constructed inside 2-dimensional planes rather than in the whole system. Extensive simulation results are presented and compared with the previous methods.