Simulation-based verification of hardware designs, in particular, register-transfer-level (RTL) designs, has been widely used, and has been one of the major bottlenecks in design processes. One of the approaches is coverage-driven verification, of its target is improvement of some metric called coverage. In a prior work of ours, we have proposed a coverage-driven verification using both randomly generated simulation patterns and patterns generated by a SAT (satisfiability) solver, and have shown its effectiveness. In this paper, we extend this approach with an SMT (satisfiability modulo theory) solver, which can handle arithmetic relations among integer, floating-point or bit-vector variables. Experimental results show that the more arithmetic modules are included, the more an SMT-based method gets superior to the method using only a SAT solver.

This paper enhances the QoE of audio and video multicast transmission over a wireless LAN by means of reliable groupcast schemes. We use GCR (GroupCast with Retries) Unsolicited Retry and GCR Block ACK as reliable groupcast schemes; they are standardized by IEEE 802.11aa. We assume that a wireless access point transmits audio and video streams to several terminals connected to the access point by groupcast. We compare three schemes: Groupcast with EDCA (Enhanced Distributed Channel Access), GCR Unsolicited Retry and GCR Block ACK. We perform computer simulations under various network conditions to assess application-level QoS and evaluate QoE by a subjective experiment. As a result, we find that the most effective scheme depends on network conditions.

Utilizing software architecture patterns is important for reducing maintenance costs. However, maintaining code according to the constraints defined by the architecture patterns is time-consuming work. As described herein, we propose a technique to detect code fragments that are incompliant to the architecture as fine-grained architectural violations. For this technique, the dependence graph among code fragments extracted from the source code and the inference rules according to the architecture are the inputs. A set of candidate components to which a code fragment can be affiliated is attached to each node of the graph and is updated step-by-step. The inference rules express the components' responsibilities and dependency constraints. They remove candidate components of each node that do not satisfy the constraints from the current estimated state of the surrounding code fragment. If the inferred role of a code fragment does not include the component that the code fragment currently belongs to, then it is detected as a violation. We have implemented our technique for the Model-View-Controller for Web Application architecture pattern. By applying the technique to web applications implemented using Play Framework, we obtained accurate detection results. We also investigated how much does each inference rule contribute to the detection of violations.

MathML is a standard markup language for describing math expressions. MathML consists of two sets of elements: Presentation Markup and Content Markup. The former is widely used to display math expressions in Web pages, while the latter is more suited to the calculation of math expressions. In this letter, we focus on the former and consider classifying Presentation MathML expressions. Identifying the classes of given Presentation MathML expressions is helpful for several applications, e.g., Presentation to Content MathML conversion, text-to-speech, and so on. We propose a method for classifying Presentation MathML expressions by using multilayer perceptron. Experimental results show that our method classifies MathML expressions with high accuracy.

Rehabilitation training with pedaling wheelchair in combination with functional electrical stimulation (FES) can be effective for decreasing the risk of falling significantly. Automatic adjustment of cycling speed and making a turn without standstill has been desired for practical applications of the training with mobile FES cycling. This study aimed at developing closed-loop control system of cycling speed with the pedaling wheelchair. Considering clinical practical use with no requirement of extensive modifications of the wheelchair, measurement method of cycling speed with inertial motion measurement units (IMUs) was introduced, and fuzzy controller for adjusting stimulation intensity to regulate cycling speed was designed. The developed prototype of closed-loop FES control system achieved appropriately cycling speed for the different target speeds in most of control trials with neurologically intact subjects. In addition, all the control trials of low speed cycling including U-turn achieved maintaining the target speed without standstill. Cycling distance and cycling time increased with the closed-loop control of low cycling speed compensating decreasing of cycling speed caused by muscle fatigue. From these results, the developed closed-loop fuzzy FES control system was suggested to work reliably in mobile FES cycling.

An important step for improving software analyzability is applying refactorings during the maintenance phase to remove bad smells, especially the long method bad smell. Long method bad smell occurs most frequently and is a root cause of other bad smells. However, no research has proposed an approach to repeating refactoring identification, suggestion, and application until all long method bad smells have been removed completely without reducing software analyzability. This paper proposes an effective approach to identifying refactoring opportunities and suggesting an effective refactoring set for complete removal of long method bad smell without reducing code analyzability. This approach, called the long method remover or LMR, uses refactoring enabling conditions based on program analysis and code metrics to identify four refactoring techniques and uses a technique embedded in JDeodorant to identify extract method. For effective refactoring set suggestion, LMR uses two criteria: code analyzability level and the number of statements impacted by the refactorings. LMR also uses side effect analysis to ensure behavior preservation. To evaluate LMR, we apply it to the core package of a real world java application. Our evaluation criteria are 1) the preservation of code functionality, 2) the removal rate of long method characteristics, and 3) the improvement on analyzability. The result showed that the methods that apply suggested refactoring sets can completely remove long method bad smell, still have behavior preservation, and have not decreased analyzability. It is concluded that LMR meets the objectives in almost all classes. We also discussed the issues we found during evaluation as lesson learned.

This study proposes a mathematical model of a gesture-based pointing interface system for simulating pointing behaviors in various situations. We assume an interaction between a pointing interface and a user as a human-in-the-loop system and describe it using feedback control theory. The model is formulated as a hybrid of a target value follow-up component and a disturbance compensation one. These are induced from the same feedback loop but with different parameter sets to describe human pointing characteristics well. The two optimal parameter sets were determined individually to represent actual pointing behaviors accurately for step input signals and random walk disturbance sequences, respectively. The calibrated model is used to simulate pointing behaviors for arbitrary input signals expected in practical situations. Through experimental evaluations, we quantitatively analyzed the performance of the proposed hybrid model regarding how accurately it can simulate actual pointing behaviors and also discuss the advantage regarding the basic non-hybrid model. Model refinements for further accuracy are also suggested based on the evaluation results.

A lot of vision systems have been embedded in devices around us, like mobile phones, vehicles and UAVs. Many of them still need interactive operations of human users. However, specifying accurate object information could be a challenging task due to video jitters caused by camera shakes and target motions. In this paper, we first collect practical hand drawn bounding boxes on real-life videos which are captured by hand-held cameras and UAV-based cameras. We give a deep look into human-computer interactive operations on unstable images. The collected data shows that human input suffers heavy deviations which are harmful to interaction accuracy. To achieve robust interactions on unstable platforms, we propose a target-focused video stabilization method which utilizes a proposal-based object detector and a tracking-based motion estimation component. This method starts with a single manual click and outputs stabilized video stream in which the specified target stays almost stationary. Our method removes not only camera jitters but also target motions simultaneously, therefore offering an comfortable environment for users to do further interactive operations. The experiments demonstrate that the proposed method effectively eliminates image vibrations and significantly increases human input accuracy.

In this paper, we establish a novel bimodal emotion database from physiological signals and facial expression, which is named as PSFE. The physiological signals and facial expression of the PSFE database are respectively recorded by the equipment of the BIOPAC MP 150 and the Kinect for Windows in the meantime. The PSFE database altogether records 32 subjects which include 11 women and 21 man, and their age distribution is from 20 to 25. Moreover, the PSFE database records three basic emotion classes containing calmness, happiness and sadness, which respectively correspond to the neutral, positive and negative emotion state. The general sample number of the PSFE database is 288 and each emotion class contains 96 samples.

In this paper, the problem on secure communication based on chaos synchronization is investigated. The dual channel information transmitting technology is proposed to increase the security of secure communication system. Based on chaos synchronization, a new digital secure communication scheme is presented for a class of master-slave systems. Finally some numerical simulation examples are given to demonstrate the effectiveness of the given results.

This paper investigates an adaptive movable access point (AMAP) system and explores its feasibility in a static indoor classroom environment with an applied wireless local area network (WLAN) system. In the AMAP system, the positions of multiple access points (APs) are adaptively moved in accordance with clustered user groups, which ensures effective coverage for non-uniform user distributions over the target area. This enhances the signal to interference and noise power ratio (SINR) performance. In order to derive the appropriate AP positions, we utilize the k-means method in the AMAP system. To accurately estimate the position of each user within the target area for user clustering, we use the general methods of received signal strength indicator (RSSI) or time of arrival (ToA), measured by the WLAN systems. To clarify the basic effectiveness of the AMAP system, we first evaluate the SINR performance of the AMAP system and a conventional fixed-position AP system with equal intervals using computer simulations. Moreover, we demonstrate the quantitative improvement of the SINR performance by analyzing the ToA and RSSI data measured in an indoor classroom environment in order to clarify the feasibility of the AMAP system.

Various applications have been realized on mobile computers such as smart phones and tablet computers. Because mobile computers have smaller monitors than conventional computers, strategies to develop user interfaces differ from conventional computer applications. For example, contents in a window are reduced or divided into multiple windows on mobile computers. To realize usable applications in this situation, usability evaluations are important. Although various usability evaluation methods for mobile computers have been proposed, few evaluate applications and identify problems automatically. Herein we propose a systematic usability evaluation method. In our method, operation histories by users are recorded and analyzed to identify steps with usability problems. Our method automatically analyzes usability problems, allowing usability evaluations in software development to be implemented easily and economically. As a case study, the operation histories were recorded and analyzed when 20 subjects operated an application on a tablet computer. Our method automatically identified many usability problems, confirming its effectiveness.

Extracting 3D information from a single image is an interesting but ill-posed problem. Especially for those artificial objects with less texture such as smooth metal devices, the decrease of object detail makes the problem more challenging. Aiming at the texture-less object with symmetric structure, this paper proposes a novel method for 3D pose estimation from a single image by introducing implicit structural symmetry and context constraint as priori-knowledge. Firstly, by parameterized representation, the texture-less object is decomposed into a series of sub-objects with regular geometric primitives. Accordingly, the problem of 3D pose estimation is converted to a parameter estimation problem, which is implemented by primitive fitting algorithm. Then, the context prior among sub-objects is introduced for parameter refinement via the augmentedLagrange optimization. The effectiveness of the proposed method is verified by the experiments based on simulated and measured data.

This paper proposes MRO-PUF, a new architecture for ring-oscillator-based physically unclonable functions (PUFs) with enhanced resistance against machine learning attacks. In the proposed PUF, an instantaneous output value of a ring oscillator is used as a response, whereas the most existing PUFs directly use propagation delays to determine the response. Since the response of the MRO-PUF is non-linear and discontinuous as the delay of the ring oscillator increases, the prediction of the response by machine learning attacks is difficult. Through the performance evaluation of the MRO-PUF with simulations, it achieves 15 times stronger resistance against machine learning attacks using a support vector machine compared to the existing ones such as an arbiter PUF and a bistable ring PUF. The MRO-PUF also achieves a sufficient level of the basic performance of PUFs in terms of uniqueness and robustness.

A penta-band antenna based on the mu-negative transmission line is presented for radio frequency (RF) energy harvesting application. The antenna utilizes five radiation modes; two quarter wavelength resonances, three quarter wavelength resonance, zeroth order resonance, and first order resonance. The parasitic radiating strip antenna generates quarter wavelength resonance radiation. The dual band antenna based on two unit cell mu-negative (MNG) transmission line gives birth to the zeroth order resonance (ZOR) mode and the first order resonance (FOR) mode. The parasitic radiating strip and dual band antenna based on two unit mu-negative (MNG) transmission line are magnetically coupled by a feed monopole with gap. This feed monopole, simultaneously, radiates at quarter and three quarter wavelength resonance frequency to cover the other bands. The multi-mode coupling mechanism of this penta-band antenna is well modeled by our derived equivalent circuit. The measured radiation efficiencies are more than 87% over the entire penta-band.

A vertex subset F ⊆ V(G) is called a cyclic vertex-cut set of a connected graph G if G-F is disconnected such that at least two components in G-F contain cycles. The cyclic vertex connectivity is the cardinality of a minimum cyclic vertex-cut set. In this paper, we show that the cyclic vertex connectivity of the trivalent Cayley graphs TGn is equal to eight for n ≥ 4.