This paper proposes a formal approach of verifying ubiquitous computing application scenarios. Ubiquitous computing application scenarios assume that there are a lot of devices and physical things with computation and communication capabilities, which are called smart objects, and these are interacted with each other. Each of these interactions among smart objects is called “federation”, and these federations form a ubiquitous computing application scenario. Previously, Yuzuru Tanaka proposed “a proximity-based federation model among smart objects”, which is intended for liberating ubiquitous computing from stereotyped application scenarios. However, there are still challenges to establish the verification method of this model. This paper proposes a verification method of this model through model checking. Model checking is one of the most popular formal verification approach and it is often used in various fields of industry. Model checking is conducted using a Kripke structure which is a formal state transition model. We introduce a context catalytic reaction network (CCRN) to handle this federation model as a formal state transition model. We also give an algorithm to transform a CCRN into a Kripke structure and we conduct a case study of ubiquitous computing scenario verification, using this algorithm and the model checking. Finally, we discuss the advantages of our formal approach by showing the difficulties of our target problem experimentally.

Recently, a high dimensional classification framework has been proposed to introduce spatial structure information in classical single kernel support vector machine optimization scheme for brain image analysis. However, during the construction of spatial kernel in this framework, a huge adjacency matrix is adopted to determine the adjacency relation between each pair of voxels and thus it leads to very high computational complexity in the spatial kernel calculation. The method is improved in this manuscript by a new construction of tensorial kernel wherein a 3-order tensor is adopted to preserve the adjacency relation so that calculation of the above huge matrix is avoided, and hence the computational complexity is significantly reduced. The improvement is verified by experimental results on classification of Alzheimer patients and cognitively normal controls.

Regression testing is essential for assuring the quality of a software product. Because rerunning all test cases in regression testing may be impractical under limited resources, test case prioritization is a feasible solution to optimize regression testing by reordering test cases for the current testing version. In this paper, we propose a novel test case prioritization approach that combines the clustering algorithm and the scheduling algorithm for improving the effectiveness of regression testing. By using the clustering algorithm, test cases with same or similar properties are merged into a cluster, and the scheduling algorithm helps allocate an execution priority for each test case by incorporating fault detection rates with the waiting time of test cases in candidate set. We have conducted several experiments on 12 C programs to validate the effectiveness of our proposed approach. Experimental results show that our approach is more effective than some well studied test case prioritization techniques in terms of average percentage of fault detected (APFD) values.

A new class of visible light communication (VLC) systems, namely image sensor (IS) based VLC systems, has emerged. An IS consists of a two-dimensional (2D) array of photodetectors (PDs), and then VLC systems with an IS receiver are capable of exploiting the spatial dimensions invoked for transmitting information. This paper aims for providing a brief survey of topics related to the IS-based VLC, and then provides a matrix representation of how to map a series of one dimensional (1D) symbols onto a set of 2D symbols for efficiently exploit the associate grade of freedom offered by 2D VLC systems. As an example, the matrix representation is applied to the symbol mapping of layered space-time coding (L-STC), which is presented to enlarge the coverage of IS-based VLC that is limited by pixel resolution of ISs.

Effective indoor localization is the essential part of VR (Virtual Reality) and AR (Augmented Reality) technologies. Tracking the RGB-D camera becomes more popular since it can capture the relatively accurate color and depth information at the same time. With the recovered colorful point cloud, the traditional ICP (Iterative Closest Point) algorithm can be used to estimate the camera poses and reconstruct the scene. However, many works focus on improving ICP for processing the general scene and ignore the practical significance of effective initialization under the specific conditions, such as the indoor scene for VR or AR. In this work, a novel indoor prior based initialization method has been proposed to estimate the initial motion for ICP algorithm. We introduce the generation process of colorful point cloud at first, and then introduce the camera rotation initialization method for ICP in detail. A fast region growing based method is used to detect planes in an indoor frame. After we merge those small planes and pick up the two biggest unparallel ones in each frame, a novel rotation estimation method can be employed for the adjacent frames. We evaluate the effectiveness of our method by means of qualitative observation of reconstruction result because of the lack of the ground truth. Experimental results show that our method can not only fix the failure cases, but also can reduce the ICP iteration steps significantly.

It inevitably comes out information overload problem with the increasing available data on e-commence websites. Most existing approaches have been proposed to recommend the users personal significant and interesting items on e-commence websites, by estimating unknown rating which the user may rate the unrated item, i.e., rating prediction. However, the existing approaches are unable to perform user prediction and item prediction, since they just treat the ratings as real numbers and learn nothing about the ratings' embeddings in the training process. In this paper, motivated by relation prediction in multi-relational graph, we propose a novel embedding model, namely RPEM, to solve the problem including the tasks of rating prediction, user prediction and item prediction simultaneously for recommendation systems, by learning the latent semantic representation of the users, items and ratings. In addition, we apply the proposed model to cross-domain recommendation, which is able to realize recommendation generation in multiple domains. Empirical comparison on several real datasets validates the effectiveness of the proposed model. The data is available at https://github.com/yuzhaour/da.

Artificial lighting is responsible for a large portion of total energy consumption and has great potential for energy saving. This paper designs an LED light control algorithm based on users' localization using multiple battery-less binary human detection sensors. The proposed lighting control system focuses on reducing office lighting energy consumption and satisfying users' illumination requirement. Most current lighting control systems use infrared human detection sensors, but the poor detection probability, especially for a static user, makes it difficult to realize comfortable and effective lighting control. To improve the detection probability of each sensor, we proposed to locate sensors as close to each user as possible by using a battery-less wireless sensor network, in which all sensors can be placed freely in the space with high energy stability. We also proposed to use a multi-sensor-based user localization algorithm to capture user's position more accurately and realize fine lighting control which works even with static users. The system is actually implemented in an indoor office environment in a pilot project. A verification experiment is conducted by measuring the practical illumination and power consumption. The performance agrees with design expectations. It shows that the proposed LED lighting control system reduces the energy consumption significantly, 57% compared to the batch control scheme, and satisfies user's illumination requirement with 100% probability.

This letter introduces a new model for backscatter assisted wireless powered communication networks (BAWPCNs) that include a hybrid access point (HAP) and multiple backscatter communication (BackCom) and traditional wireless powered communication network (WPCN) users. To make full use of time to transmit information, both backscatter and harvest-then-transmit (HTT) modes are employed. In the proposed model, during the first time slot dedicated for energy transfer in traditional WPCNs, the traditional WPCN users harvest energy radiated by the HAP, and simultaneously the BackCom users reflect modulated signals to the HAP. The traditional WPCN users are scheduled during the remaining time slots via time division multiple access (TMDA). The optimal time allocation policies for the half-duplex (HD) and full-duplex (FD) BAWPCNs are obtained to maximize the system throughput. The tradeoff between backscatter and HTT modes is analyzed. Simulation results demonstrate the superiority of the proposed model.

We evaluated a technique for protecting the copyright of digital data for 3-D printing. To embed copyright information, the inside of a 3-D printed object is constructed from fine domains that have different physical characteristics from those of the object's main body surrounding them, and to read out the embedded information, these fine domains inside the objects are detected using nondestructive inspections such as X-ray photography or thermography. In the evaluation, copyright information embedded inside the 3-D printed object was expressed using the depth of fine cavities inside the object, and X-ray photography were used for reading them out from the object. The test sample was a cuboid 46mm wide, 42mm long, and 20mm deep. The cavities were 2mm wide and 2mm long. The difference in the depths of the cavities appeared as a difference in the luminance in the X-ray photographs, and 21 levels of depth could be detected on the basis of the difference in luminance. These results indicate that under the conditions of the experiment, each cavity expressed 4 to 5bits of information with its depth. We demonstrated that the proposed technique had the possibility of embedding a sufficient volume of information for expressing copyright information by using the depths of cavities.

The 1-bit band-pass delta-sigma modulator (BP-DSM) achieves high resolution by using the oversampling technique. This method allows direct RF signal transmission from a digitally modulated signal, using a 1-bit digital pulse train. However, it has been previously reported that the adjacent channel leakage ratio (ACLR) in a target frequency band degrades due to the pulse transition mismatch between rising and falling waveforms in the time domain. This paper clarifies that the spurious distortion in BP-DSM is caused by the asymmetricity of the waveform about the center of an eye pattern in the time axis, and proposes a 1-bit BP-DSM with the compensator consisting of a fractional delay filter and a binary data differentiator to cancel out the asymmetry in the target frequency band. This can accurately provide a wideband cancellation signal with more than 100MHz bandwidth, including the adjacent channel, within 50dB power dynamic range. Using long term evolution (LTE) signals with 5MHz bandwidth at 0.8GHz, we simulated the spurious distortion, performing various combinations of rising and falling times in the eye pattern, and the proposed 1-bit BP-DSM always achieved high ACLR, up to 60dB, in 140MHz bandwidth, under all conditions.

In accordance with Moore's law, recent design issues include shortening of time-to-market and detection of delay faults. Several studies with respect to formal techniques have examined the first issue. Using the equivalence checking, it is possible to identify whether large circuits are equivalent or not in a practical time frame. With respect to the latter issue, it is difficult to achieve 100% fault efficiency even for transition faults in full scan designs. This study involved proposing a redundant transition fault identification method using equivalence checking. The main concept of the proposed algorithm involved combining the following two known techniques, 1. modeling of a transition fault as a stuck-at fault with temporal expansion and 2. detection of a stuck-at fault by using equivalence checking tools. The experimental results indicated that the proposed redundant identification method using a formal approach achieved 100% fault efficiency for all benchmark circuits in a practical time even if a commercial ATPG tool was unable to achieve 100% fault efficiency for several circuits.

In multi-view social networks field, a flexible Nonnegative Matrix Factorization (NMF) based framework is proposed which integrates multi-view relation data and feature data for community discovery. Benefit with a relaxed pairwise regularization and a novel orthogonal regularization, it outperforms the-state-of-art algorithms on five real-world datasets in terms of accuracy and NMI.

A novel real-valued ESPRIT (RV-ESPRIT) algorithm is proposed to estimate the direction of arrival (DOA) and direction of departure (DOD) for noncircular signals in bistatic MIMO radar. By exploiting the property of signal noncircularity and Euler's formula, a new virtual array data of bistatic MIMO radar, which is twice that of the MIMO virtual array data, is established with real-valued sine and cosine data. Then the receiving/transmitting selective matrices are constructed to obtain the receiving/transmitting rotationally invariant factors. Compared to the existing angle estimation methods, the proposed algorithm has lower computational load. Simulation results confirm the effectiveness of the RV-ESPRIT.

Multiple image group cosegmentation (MGC) aims at segmenting common object from multiple group of images, which is a new cosegmentation research topic. The existing MGC methods formulate MGC as label assignment problem (Markov Random Field framework), which is observed to be sensitive to parameter setting. Meanwhile, it is also observed that large object variations and complicated backgrounds dramatically decrease the existing MGC performance. To this end, we propose a new object proposal based MGC model, with the aim of avoiding tedious parameter setting, and improving MGC performance. Our main idea is to formulate MGC as new region proposal selection task. A new energy function in term of proposal is proposed. Two aspects such as the foreground consistency within each single image group, and the group consistency among image groups are considered. The energy minimization method is designed in EM framework. Two steps such as the loop belief propagation and foreground propagation are iteratively implemented for the minimization. We verify our method on ICoseg dataset. Six existing cosegmentation methods are used for the comparison. The experimental results demonstrate that the proposed method can not only improve MGC performance in terms of larger IOU values, but is also robust to the parameter setting.

Numerous methods have been developed to handle lighting variations in the preprocessing step of face recognition. However, most of them only use the high-frequency information (edges, lines, corner, etc.) for recognition, as pixels lied in these areas have higher local variance values, and thus insensitive to illumination variations. In this case, information of low-frequency may be discarded and some of the features which are helpful for recognition may be ignored. In this paper, we present a new and efficient method for illumination normalization using an energy minimization framework. The proposed method aims to remove the illumination field of the observed face images while simultaneously preserving the intrinsic facial features. The normalized face image and illumination field could be achieved by a reciprocal iteration scheme. Experiments on CMU-PIE and the Extended Yale B databases show that the proposed method can preserve a very good visual quality even on the images illuminated with deep shadow and high brightness regions, and obtain promising illumination normalization results for better face recognition performance.

For a multiuser multi-input multi-output (MU-MIMO) multicell network, the Han-Kobayashi strategy aims to improve the achievable rate region by splitting the data information intended to a serviced user (UE) into a common message and a private message. The common message is decodable by this UE and another UE from an adjacent cell so that the corresponding intercell interference is cancelled off. This work aims to design optimal precoders for both common and private messages to maximize the network sum-rate, which is a highly nonlinear and nonsmooth function in the precoder matrix variables. Existing approaches are unable to address this difficult problem. In this paper, we develop a successive convex quadratic programming algorithm that generates a sequence of improved points. We prove that the proposed algorithm converges to at least a local optimum of the considered problem. Numerical results confirm the advantages of our proposed algorithm over conventional coordinated precoding approaches where the intercell interference is treated as noise.

In the field of action recognition, Spatio-Temporal Interest Points (STIPs)-based features have shown high efficiency and robustness. However, most of state-of-the-art work to describe STIPs, they typically focus on 2-dimensions (2D) images, which ignore information in 3D spatio-temporal space. Besides, the compact representation of descriptors should be considered due to the costs of storage and computational time. In this paper, a novel local descriptor named 3D Gradient LBP is proposed, which extends the traditional descriptor Local Binary Patterns (LBP) into 3D spatio-temporal space. The proposed descriptor takes advantage of the neighbourhood information of cuboids in three dimensions, which accounts for its excellent descriptive power for the distribution of grey-level space. Experiments on three challenging datasets (KTH, Weizmann and UT Interaction) validate the effectiveness of our approach in the recognition of human actions.

This contribution presents and analyzes the statistical regularity related to the noise power spectrum series and the speech spectrum series. It also undertakes a thorough inquiry of the quasi-Gaussian distributed power spectrum series obtained using the radical root transformation. Consequently, a noise-estimation algorithm is proposed for speech enhancement. This method is effective for separating the noise power spectrum from the noisy speech power spectrum. In contrast to standard noise-estimation algorithms, the proposed method requires no speech activity detector. It was confirmed to be conceptually simple and well suited to real-time implementations. Practical experiment tests indicated that our method is preferred over previous methods.

This paper addresses power saving for STAs (Wireless Stations) in WLANs (Wireless LANs). Mobile devices are increasingly used in situations in which they access WLANs. However, mobile devices consume large amounts of power when they communicate through a WLAN, and this shortens their battery lifetime. IEEE 802.11 specifies PSM (Power-Saving Mode) as the power-saving method for standard WLANs. However, the sleep conditions specified by PSM for STAs are not optimal in terms of power saving, except when the number of STAs is small, and this increases packet transfer delay. In this paper, we propose a power-saving method in which STAs reduce power consumption by sleeping for a period specified by the NAV (Network Allocation Vector) duration, which is set by an RTS/CTS handshake, and the duration of the NAV is extended by bidirectional burst transmission. To suppress the transfer delay caused by the bidirectional burst transmission, an AP (Access Point) manages the transmission deadline of each downlink packet on the basis of its acceptable value of delay and adapts the number of packets transferred in the bidirectional burst transmission. Although another existing method also uses the NAV duration to manage STA sleeping, the bidirectional burst transmission can only be initiated by the STAs themselves and the NAV is of an extremely limited duration. On the other hand, the proposed method specifies generalized bidirectional burst transmission without the limitations of the transmission initiator and the burst length within acceptable packet transfer delay. Moreover, we investigate the combination of the proposed method with PSM in order to improve the performance in situations in which the number of STAs is small by taking advantage of the combined properties of PSM and the proposed method. The evaluation results demonstrate that these proposed methods can reduce the power consumption of wireless stations and suppress packet transfer delay.

A novel spur cancelled clock generator (SCCG) capable of recovering RX sensitivity degradations caused by digital clocks in wireless SoCs is presented. Clock spurs that degrade RX sensitivities are canceled by applying the SCCG to digital circuits or ADCs. The SCCG is integrated into a Bluetooth Low Energy (BLE) SoC fabricated in a 65 nm CMOS process. A measured clock spur reduction of 34 dB and an RX sensitivity recovery of 5 dB are achieved by the proposed SCCG. The power consumption and occupied area of the SCCG is only 18 µW and 40 μm × 120 μm, respectively.