Search

Workflow provides a promising solution for organizations to achieve their business goals by interactions and collaborations between users. Separation of duty (SoD) is a security principle to prevent fraud and errors in collaborative workflow environments. It is crucial to verify and ensure the correctness and consistence of workflow with SoD constraints during the design time. In this paper, we propose a method to model and analyze workflow with SoD constraints based on colored Petri nets (CPN). The control flow, authorization rules and SoD constraints in a workflow are all represented by CPN and combined into one integrated CPN model. Then the execution paths of this model can be derived by reachability tree analysis. By analyzing these execution paths, some latent deadlocks caused by the inconsistency between authorization rules and SoD constraints can be detected.

Model checking has been considered as a promising approach to establish the correctness of systems. Counterexample-guided abstraction refinement is a key strategy for model checking in verification of large-scale systems. State separation problem poses the main hurdle during the refinement. We present two fast heuristics to solve this problem. We prove the effectiveness of our heuristics by both theoretical analysis and experimental results. Experimental results show the promising performance of our approach.

This paper presents a satisfiability formulation for FPGA segmented channel routing with pin rearrangements. In our new routing model, the pins in each module have certain degree of freedom to be rearranged. With this flexibility, the wire routability can be improved in segmented channel routing. We present an efficient SAT-based approach to solve the problem. We use one of the best SAT-solvers, zChaff, to perform our experiments. Experimental results show the promising performance of the method.

A two-stage scan architecture is proposed to constrain transition propagation within a small part of scan flip-flops. Most scan flip-flops are deactivated during test application. The first stage includes multiple scan chains, where each scan chain is driven by a primary input. Each scan flip-flop in the multiple scan chains drives a group of scan flip-flops in the second stage. Scan flip-flops in different stages use separate clock signals. Test signals assigned to scan flip-flops in the multiple scan chains are applied to the scan flip-flops of the second stage in one clock cycle after the test vector has been applied to the multiple scan chains. There exists no transition at the scan flip-flops in the second stage when a test vector is applied to the multiple scan chains

A new scan architecture called reconfigured scan forest is proposed for cost-effective scan testing. Multiple scan flip-flops can be grouped based on structural analysis that avoids new untestable faults due to new reconvergent fanouts. The proposed new scan architecture allows only a few scan flip-flops to be connected to the XOR trees. The size of the XOR trees can be greatly reduced compared with the original scan forest; therefore, area overhead and routing complexity can be greatly reduced. It is shown that test application cost, test data volume, and test power with the proposed scan forest architecture can be greatly reduced compared with the conventional full scan design with a single scan chain and several recent scan testing methods

International audience; Polyline curves which are composed of line segments and arcs are widely used in engineering applications. In this paper, a novel offset algorithm for polyline curves is proposed. The offset algorithm comprises three steps. Firstly, the offsets of all the segments of polyline curves are calculated. Then all the offsets are trimmed or joined to build polyline curves that are called untrimmed offset curves. Finally, a clipping algorithm is applied to the untrimmed offset curves to yield the final results. The offset algorithm can deal with polyline curves that are self-intersection, overlapping or containing small arcs. The new algorithm has been implemented in a commercial system TiOpenCAD 8.0 and its reliability is verified by a great number of examples.

In recent years there has been a significant interest in peer-to-peer (P2P) environments in the community of data management. However, almost all work, so far, is focused on exact query processing in current P2P data systems. The autonomy of peers also is not considered enough. In addition, the system cost is very high because the information publishing method of shared data is based on each document instead of document set. In this paper, abstract indices (AbIx) are presented to implement content-based approximate queries in centralized, distributed and structured P2P data systems. It can be used to search as few peers as possible but get as many returns satisfying users' queries as possible on the guarantee of high autonomy of peers. Also, abstract indices have low system cost, can improve the query processing speed, and support very frequent updates and the set information publishing method. In order to verify the effectiveness of abstract indices, a simulator of 10,000 peers, over 3 million documents is made, and several metrics are proposed. The experimental results show that abstract indices work well in various P2P data systems.

Process mining aims at extracting information from event logs to capture the business process as it is being executed. Process mining is particularly useful in situations where events are recorded but there is no system enforcing people to work in a particular way. Consider for example a hospital where the diagnosis and treatment activities are recorded in the hospital information system, but where health-care professionals determine the "careflow." Many process mining approaches have been proposed in recent years. However, in spite of many researchers' persistent efforts, there are still several challenging problems to be solved. In this paper, we focus on mining non-free-choice constructs, i.e., situations where there is a mixture of choice and synchronization. Although most real-life processes exhibit non-free-choice behavior, existing algorithms are unable to adequately deal with such constructs. Using a Petri-net-based representation, we will show that there are two kinds of causal dependencies between tasks, i.e., explicit and implicit ones. We propose an algorithm that is able to deal with both kinds of dependencies. The algorithm has been implemented in the ProM framework and experimental results shows that the algorithm indeed significantly improves existing process mining techniques.

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.

A new model of event and message driven Petri network(EMDPN) based on the characteristic of class interaction for messages passing between two objects was extended. Using EMDPN interaction graph, a class hierarchical test-case generation algorithm with cooperated paths (copaths) was proposed, which can be used to solve the problems resulting from the class inheritance mechanism encountered in object-oriented software testing such as oracle, message transfer errors, and unreachable statement. Finally, the testing sufficiency was analyzed with the ordered sequence testing criterion(OSC). The results indicate that the test cases stemmed from newly proposed automatic algorithm of copaths generation satisfies synchronization message sequences testing criteria, therefore the proposed new algorithm of copaths generation has a good coverage rate.

International audience; N-sided hole filling plays an important role in vertex blending. To deal with the case that the corner is surrounded by rational surfaces (i.e. NURBS surfaces), an algorithm to fill n-sided holes with ɛ-G1 continuous NURBS patches that interpolate the given boundary curves and approximate the given cross-boundary derivatives is presented based on Piegl's method. The NURBS surfaces joining along inner or boundary curves have normal vectors that do not deviate more than the user-specified angular tolerance ɛ. The boundaries as well as cross-boundary derivatives can all be NURBS curves. No restrictions are imposed on the number of boundary curves, and the cross-boundary derivatives can be specified independently.

Field programmable gate arrays (FPGAs) are an enabling technology in circuit designs. We consider the board-level multi-terminal net assignment in the FPGA-based logic emulation. A novel probabilistic optimization method is devised for solving the net assignment problem. The approach incorporates randomized rounding, genetic algorithm, and solution-improvement strategies. Experimental results demonstrate promising performance.

The reconstruction of 3D objects from 2D orthographic views is very important for the maintenance and continued development of existing product designs. An efficient method for generating 3D curvilinear wire-frames from three orthographic views is presented, which is the pivotal stage of solid reconstruction by wire-frame-oriented approaches. By unifying the recovery of spatial conics without restrictions on their positions, our method can improve the efficiency and reliability of curvilinear wire-frame reconstruction. A projection matching algorithm is proposed to efficiently reveal all match projections according to the projective properties of spatial edges. Furthermore, a four-point method, which is based on the rational Bezier form of conics, is proposed to uniformly generate various types of conics in arbitrary positions. Several examples are provided.

Congestion estimation plays an important role in the physical layout of VLSI design. This paper presents a new probabilistic estimation model that improves the previous estimators by relaxing the constraint on detours in a route. The model is more general and realistic for it gives the flexibility for the wires to have wider usage area to bypass the congestion regions and blockages. Given a routing grid and a set of nets to be routed, the model predicts the routing density on each edge of the grid. The routing density provides direct congestion estimation. We compare our estimation results to the actual routing results. Experimental results show the effectiveness of our estimator.

A finite difference method (FDM) for multi-dimensional nonlinear coupled system of parabolic and hyperbolic equations is studied. Nonlinear coupled property is fully considered. Variant techniques of discrete functional analysis such as summation by parts and deductive reasoning are used to make prior estimates. The FD scheme is uniquely solvable and unconditionally stable. With the approximation property of the scheme, the convergence is obtained with a rate of O(h2+Δt2) order.

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.

By Bezout's theorem, three quadric surfaces have at most eight isolated intersections although they may have infinitely many intersections. In this paper, we present an efficient and robust algorithm, to obtain the isolated and the connected components of, or to determine the number of isolated real intersections of, three quadric surfaces by reducing the problem to computing the real intersections of two planar curves obtained by Levin's method.

Test effectiveness of a test-per-scan built-in self-test (BIST) scheme is highly dependent on the length and number of scan chains. Fewer cycles are used to capture test responses when the length of the scan chains increases and the total number of clock cycles is fixed. Another important feature of the test-per-scan BIST scheme is that test responses of the circuit at the inputs of the scan flip-flops are not observable during the shift cycles. A new scan architecture is proposed to make a scan-based circuit more observable. The scan chain is partitioned into multiple segments. Multiple capture cycles are inserted to receive test responses during the shift cycles compared to the test-per-scan test scheme. Unlike other BIST schemes using multiple capture cycles after the shift cycles, our method inserts multiple capture cycles inside the shift cycles, but not after the shift cycles. Unlike the previous method that drives multiple scan segments by a single scan-in signal, the proposed method uses a new architecture to control all scan segments by different signals. Sufficient experimental results are presented to demonstrate the effectiveness of the method.

This paper proposes a new codebook generation algorithm for image data compression using a combined scheme of principal component analysis (PCA) and genetic algorithm (GA). The combined scheme makes full use of the near global optimal searching ability of GA and the computation complexity reduction of PCA to compute the codebook. The experimental results show that our algorithm outperforms the popular LBG algorithm in terms of computational efficiency and image compression performance.

We address the problem of board-level multiterminal net assignment in FPGA-based logic emulation. We present a novel mathematical model for this problem. A powerful metaheuristic approach, called scatter search, is adopted. Effective heuristics are incorporated for accelerating the optimization search process. Experimental results demonstrate the promising performance of our approach.

Reversible logic plays an important role in quantum computing. This article presents some novel results on synthesis of 3 × 3 reversible Boolean gates. We derive the relationship between reversible 3 × 3 gates and corresponding symmetric groups. By introducing a set of universal libraries, we show how to use group theory to synthesize any 3 × 3 reversible gate.

Cell assignment is an important task in the design of personal communication services networks. We present a stochastic approach for solving the problem. The method consists of an expected value programming and a chance-constrained programming. We show that the expected value programming model is equivalent to the existing deterministic models. However, the chance-constrained programming model is more precise and flexible. A hybrid intelligent algorithm is proposed for the CCP model. Experimental results show the effectiveness of the method.

In this paper, region features and relevance feedback are used to improve the performance of CBIR. Unlike existing region-based approaches where either individual regions are used or only simple spatial layout is modeled, the proposed approach simultaneously models both region properties and their spatial relationships in a probabilistic framework. Furthermore, the retrieval performance is improved by an adaptive filter based relevance feedback. To illustrate the performance of the proposed approach, extensive experiments have been carried out on a large heterogeneous image collection with 17,000 images, which render promising results on a wide variety of queries.

This paper describes a lightweight security mechanism for protecting electronic transactions conducted over the mobile platform. In a typical mobile computing environment, one or more of the transacting parties are based on some wireless handheld devices. Electronic transactions conducted over the mobile platform are gaining popularity and it is widely accepted that mobile computing is a natural extension of the wired Internet computing world. However, security over the mobile platform is more critical due to the open nature of wireless networks. Furthermore, security is more difficult to implement on the mobile platform because of the resource limitation of mobile handheld devices. Therefore, security mechanisms for protecting traditional computer communications need to be revisited so as to ensure that electronic transactions involving mobile devices can be secured and implemented in an effective manner. This research is part of our effort in designing security infrastructure for electronic commerce systems, which extend from the wired to the wireless Internet. A lightweight mechanism was designed to meet the security needs in face of the resource constraints. The proposed mechanism is proven to be practical in real deployment environment.

The definition and maintenance of workflow processes have become important tasks for enterprises as workflow management systems (WFMS) are systematically applied to critical business processes. In order to simplify the management and usage of workflow processes and to integrate with other applications, a good modeling method is essential. The WFCP-net (workflow-net based on colored Petri net) is an extension of the workflow-net (WF-net) which can be used to model family of workflow processes with similar process routes and logic rules. An expanding suite of tools, which currently includes, can support its application: a process structure graph editor, a WF script (workflow script language for writing business rules) editor and translator (translate WF script into Java classes) and a dynamically loadable workflow engine.

The key challenges of the model-driven approach to designing multi-clocked embedded systems are three-fold: (1) how to model local synchronous components and asynchronous communication between components in a single framework, (2) how to ensure the correctness of the model, and (3) how to maintain the consistency between the model and the implementation of the system. In this paper, we present Tsmart, a self-contained toolkit to address these three challenges. Tsmart seamlessly integrates (1) a graphical editor to facilitate the modeling of the complex behaviors and structures in an embedded system, (2) a simulator for interactive graphical simulation to understand and debug the system model, (3) a verication engine to verify the correctness of the system design, and (4) a synthesis engine to automatically generate ecient executable VHDL code from the model. The toolkit has been successfully applied to designing the main control system of a train communication controller, and the system has already been deployed and in operation. The evaluation of Tsmart on this real industrial application demonstrates the eectiveness and the potential of the toolkit.

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.

Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant COQ. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.

International audience; Polar NURBS surface is a kind of periodic NURBS surface, one boundary of which shrinks to a degenerate polarpoint. The specific topology of its control-point mesh offers the ability to represent a cap-like surface, which iscommon in geometric modeling. However, there is a critical and challenging problem that hinders its application:curvature continuity at the extraordinary singular pole. We first propose a sufficient and necessary condition ofcurvature continuity at the pole. Then, we present constructive methods for the two key problems respectively:how to construct a polar NURBS surface with curvature continuity and how to reform an ordinary polar NURBSsurface to curvature continuous. The algorithms only depend on the symbolic representation and operations ofNURBS, and they introduce no restrictions on the degree or the knot vectors. Examples and comparisons demonstratethe applications of the curvature-continuous polar NURBS surface in hole-filling and free-shape modeling.

Programmable logic controller (PLC) system, a typical member in the embedded family, is now widely applied in industry. For safety critical PLC systems, reliability is of top significance. However, due to subcomponents’ temporal correlations caused by the run-time execution of embedded ladder programs, the complexity of reliability analysis is greatly increased. In this paper, we propose a novel probabilistic model to analyze reliability of PLC systems, called run-time reliability model (RRM). RRM is automatically constructed based on the structure and run-time execution of the embedded ladder program. Moreover, it is also a dynamic bayesian network (DBN) capturing full dependencies in a PLC system. Then, according to execution semantics of RRM nodes, we present customized conditional probability distribution (CPD) tables to calculate final reliability of the system, with failure probability of every referenced component as refinement. The strength of this model is that not only does it explicitly specify the correlations between run-time execution of embedded software and system components, but also it serves as a computational mechanism for probabilistic inference. Besides, the proposed approach is superior to previous works in both accuracy and efficiency. Compared to monte carlo based simulation, the average error rate of reliability values inferred from RRM model is small.

Today’s system-on-chip and distributed systems are commonly equipped with multiple clocks. The key challenge in designing such systems is that heterogenous control-oriented and data-oriented behaviors within one clock domain, and asynchronous communications between two clock domains have to be captured and evaluated in a single framework. In this paper, we propose to use timed automata and synchronous dataflow to capture the dynamic behaviors of multi-clock embedded systems. A timed automata and synchronous dataflow based modeling and analyzing framework is constructed to evaluate and optimize the performance of multiclock embedded systems. Data-oriented behaviors are captured by synchronous dataflow, while synchronous control-oriented behaviors are captured by timed automata, and inter clock-domain asynchronous communication can be modeled in an interface timed automaton or a synchronous dataflow module with the CSP mechanism. The behaviors of synchronous dataflow are interpreted by some equivalent timed automata to maintain the semantic consistency of the mixed model. Then, various functional properties can be simulated and verified within the framework. We apply this framework in the design process of a sub-system that is used in real world subway communication control system

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.

International audience; Particle systems are important building block for simulating vivid and detail-rich effects in virtual world. One of the most difficult aspects of particle systems has been detecting collisions between particlesand mesh surface. Due to the huge computation, a variety of proxy-based approaches have been proposed recently to perform visually correct simulation. However, all either limit the complexity of the scene, fail toguarantee non-penetration, or are too slow for real-time use with many particles. In this paper, we propose anew octree-based proxy for colliding particles with meshes on the GPU. Our approach works by subdividingthe scene mesh with an octree in which each leaf node associates with a representative normal correspondingto the normals of the triangles that intersect the node. We present a view-visible method, which is suitable forboth closed and non-closed models, to label the empty leaf nodes adjacent to nonempty ones with appropriateback/front property, allowing particles to collide with both sides of the scene mesh. We show how collisionscan be performed robustly on this proxy structure in place of the original mesh, and describe an extension thatallows for fast traversal of the octree structure on the GPU. The experiments show that the proposed methodis fast enough for real-time performance with millions of particles interacting with complex scenes.

When IBM's John Backus first developed the Fortran programming language, back in 1957, he certainly never dreamt that it would become a world-wide success and still be going strong many years later. Given the oft-repeated predictions of its imminent demise, starting around 1968, it is a surprise, even to some of its most devoted users, that this much-maligned language is not only still with us, but is being further developed for the demanding applications of the future. What has made this programming language succeed where most slip into oblivion? One reason is certainly that the language has been regularly standardized. In this paper we will trace the evolution of the language from its first version and though six cycles of formal revision, and speculate on how this might continue. Now, modern Fortran is a procedural, imperative, compiled language with a syntax well suited to a direct representation of mathematical formulas. Individual procedures may be compiled separately or grouped into modules, either way allowing the convenient construction of very large programs and procedure libraries. Procedures communicate via global data areas or by argument association. The language now contains features for array processing, abstract data types, dynamic data structures, objectoriented programming and parallel processing.

We develop an efficient approach to fabricate nitrogen-doped graphene with tunable pyridinic nitrogen levels (from 1.1 to 1.8 at.%), abundant in-plane holes and high surface areas (623 m(2) g(-1)) via a hydrothermal treatment of graphene oxide with hydrogen peroxide and subsequent annealing under ammonia gas. It is found that the chemical etching is beneficial to the formation of pyridinic nitrogen in graphene during the nitrogen-doping process, which is crucial to enhancing the electrocatalytic properties of graphene for oxygen reduction reaction (ORR). Hence, the optimized NG exhibits good electrocatalytic activity, more positive onset potential than Pt-C (-0.08 V versus -0.09 V), good durability, and high selectivity when it is employed as a metal-free catalyst for ORR. This approach may uncover a mechanism in escalation of pyridinic N atoms doped on the graphene basal edge and provide an efficient platform for the synthesis of a series of heteroatom-doped graphene with tunable heteroatom content for broad applications.

In this paper, we propose a novel image auto-annotation model using tag-related random search over range-constrained visual neighbors of the to-be-annotated image. The proposed model, termed as TagSearcher, observes that the annotating performances of many previous visual-neighbor-based models are generally sensitive to the quantity setting of visual neighbors, and the probabilities for visual neighbors to be selected is better to be tag-dependent, meaning that each candidate tag can have its own trustworthy part of visual neighbors for score prediction. And thus TagSearcher uses a constrained range rather than an identical and fixed number of visual neighbors for auto-annotation. By performing a novel tag-related random search process over the graphical model made up of range-constrained visual neighbors, TagSearcher can find the trustworthy part for each candidate tag, and further utilize both visual similarities and tag correlations for score prediction. With the range constraint for visual neighbors and the tag-related random search process, TagSearcher can not only achieve satisfactory annotating performances, but also reduce the performance sensitivity. Experiments conducted on benchmark Corel5k well demonstrate its rationality and effectiveness.

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.

This paper presents a new approach for constructing normal maps that capture high-frequency geometric detail from dense models of arbitrary topology and are applied to the simplified version of the same models generated by any simplification method to mimic the same level of detail. A variant of loose octree scheme is used to optimally calculate the mesh normals. A B-spline surface fitting based method is employed to solve the issue of thin plate. A memory saving Breadth-First Search (BFS) order construction is designed. Furthermore, a speedup scheme that exploits access coherence is used to accelerate filtering operation. The proposed method can synthesize good quality images of models with extremely high number of polygons while using much less memory and render at much higher frame rate.