The software development process is front-loaded when formal specification is deployed and as a consequence more problems are identified and solved at an earlier point of time. This places extra importance on the quality and efficiency of the different formal specification tasks. We use the term “exploratory modeling” to denote the modeling that is conducted during the early stages of software development before the requirements are clearly understood. We believe tools that support not only rigorous but also flexible construction of the specification at the same time are helpful in such exploratory modeling phases. This paper presents a web-based IDE named VDMPad to demonstrate the concept of exploratory modeling. VDMPad has been evaluated by experienced professional VDM engineers from industry. The positive evaluation resulting from such industrial users are presented. It is believed that flexible and rigorous tools for exploratory modeling will help to improve the productivity of the industrial software developments by making the formal specification phase more efficient.

Spatial modulation (SM) is introduced into layered space-time coding (L-STC) used in image sensor (IS)-based visible light communication (VLC) systems. STC was basically investigated for extending the communication range of the IS-based VLC link [10], although it is out of the range when IS receivers are at the long distance from the LED array of the transmitter where the number of pixels capturing the transmitter on the image plane is less than the number of LEDs of the array. Furthermore, L-STC was done in [11] for increasing the reception rate with improving the pixel resolution while the receiver was approaching the transmitter. In this paper, SM is combined into L-STC by mapping additional information bits on the location of the pair of STC bit matrices of each layer. Experimental results show that additional SM bits are extracted with no error, without deteriorating the reception quality of and shrinking the transmission range of the original L-STC.

We investigate a finite-sized self-complementary bow-tie antenna (SC-BTA) integrated with a semiconductor mesa with respect to radiation characteristics such as the peak radiation frequency and bandwidth around the fundamental radiation mode. For this investigation, we utilize an equivalent circuit model of the SC-BTA derived in our previous work and a finite element method solver. Moreover, we derive design guidelines for the radiation characteristics in the form of size scaling-rules with respect to the antenna outer size for a terahertz transmitter.

Image sensor communication (ISC), a type of visible light communication, is an emerging wireless communication technology that uses LEDs to transmit a signal and uses an image sensor in a camera to receive the signal. This paper discusses the present status of and future trends in ISC by describing the essential characteristics and features of ISC. Moreover, we overview the products and expected future applications of ISC.

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.

Subspace representation model is an important subset of visual tracking algorithms. Compared with models performed on the original data space, subspace representation model can effectively reduce the computational complexity, and filter out high dimensional noises. However, for some complicated situations, e.g., dramatic illumination changing, large area of occlusion and abrupt object drifting, traditional subspace representation models may fail to handle the visual tracking task. In this paper, we propose a novel subspace representation algorithm for robust visual tracking by using low-rank representation with graph constraints (LRGC). Low-rank representation has been well-known for its superiority of handling corrupted samples, and graph constraint is flexible to characterize sample relationship. In this paper, we aim to exploit benefits from both low-rank representation and graph constraint, and deploy it to handle challenging visual tracking problems. Specifically, we first propose a novel graph structure to characterize the relationship of target object in different observation states. Then we learn a subspace by jointly optimizing low-rank representation and graph embedding in a unified framework. Finally, the learned subspace is embedded into a Bayesian inference framework by using the dynamical model and the observation model. Experiments on several video benchmarks demonstrate that our algorithm performs better than traditional ones, especially in dynamically changing and drifting situations.

This paper presents a high resolution mixed-domain Delta-Sigma (ΔΣ) time-to-digital converter (TDC) which utilizes a charge pump as time-to-voltage converter, a low resolution SAR ADC as quantizer, and a pair of delay-line digital-to-time converters to form a negative feedback. By never resetting the sampling capacitor of the charge-pump, an integrator is realized and first order noise shaping can be achieved. However, since the integrating capacitor is never cleared, this circuit is prone to charge-sharing issue during input sampling which can degrade TDC's performance. To deal with this issue, a compensation circuit consists of another pair of sampling capacitors and charge-pumps with doubled current is proposed. This TDC is designed and simulated in 65 nm CMOS technology and can operate at 200 MHz sampling frequency. For 2.5 MHz bandwidth, simulation shows that this TDC achieves 66.4 dB SNDR and 295 fsrms integrated noise for ±1 ns input range. The proposed TDC consumes 1.78 mW power that translates to FoM of 208 fJ/conv.

This paper presents the formal analysis of the feature negotiation and connection management procedures of the Datagram Congestion Control Protocol (DCCP). Using state space analysis we discover an error in the DCCP specification, that result in both ends of the connection having different agreed feature values. The error occurs when the client ignores an unexpected Response packet in the OPEN state that carries a valid Confirm option. This provides an evidence that the connection management procedure and feature negotiation procedures interact. We also propose solutions to rectify the problem.

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 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.

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 paper presents a novel framework called error case frames for correcting preposition errors. They are case frames specially designed for describing and correcting preposition errors. Their most distinct advantage is that they can correct errors with feedback messages explaining why the preposition is erroneous. This paper proposes a method for automatically generating them by comparing learner and native corpora. Experiments show (i) automatically generated error case frames achieve a performance comparable to previous methods; (ii) error case frames are intuitively interpretable and manually modifiable to improve them; (iii) feedback messages provided by error case frames are effective in language learning assistance. Considering these advantages and the fact that it has been difficult to provide feedback messages using automatically generated rules, error case frames will likely be one of the major approaches for preposition error correction.

This paper studies the supervisory control of partially observed quantitative discrete event systems (DESs) under the fixed-initial-credit energy objective. A quantitative DES is modeled by a weighted automaton whose event set is partitioned into a controllable event set and an uncontrollable event set. Partial observation is modeled by a mapping from each event and state of the DES to the corresponding masked event and masked state that are observed by a supervisor. The supervisor controls the DES by disabling or enabling any controllable event for the current state of the DES, based on the observed sequences of masked states and masked events. We model the control process as a two-player game played between the supervisor and the DES. The DES aims to execute the events so that its energy level drops below zero, while the supervisor aims to maintain the energy level above zero. We show that the proposed problem is reducible to finding a winning strategy in a turn-based reachability game.

This study mainly involved examining a high-directivity radiation system with spherical dielectric resonator as pseudo multipole source. The method of spherical wave expansion is focused on wherein the plane wave that is infinitely spread can be radiated from or absorbed by multipoles at the origin. It is not possible to explain this phenomenon by Huygens' principle, which is a basic principle of aperture antenna theory. Thus, in the study, a high-directivity beam design is proposed by synthesizing spherical waves. The directivity of the synthesized spherical wave corresponds with the angular momentum and angle, which is an uncertainty relation different from that of the aperture source. The estimation of the effective aperture of the synthesized spherical wave indicates that the wave intrinsic source is assumed to exist at the surface of the cutoff region. Finally, the results reveal that a radiation system without a singular point can be composed using a spherical dielectric resonator. The study discusses the potential of a high-directivity radiation system constructed by a multi-mode degenerate spherical dielectric resonator as a pseudo multipole source.

A flexible orthogonal frequency-division multiplexing optical network enables the bandwidth to be flexibly changed by changing the number of sub-carriers. We assume that users request to dynamically change the number of sub-carriers. Dynamic bandwidth changes allow the network resources to be used more efficiently but each change takes a significant amount of time to complete. Service centric resource allocation must be considered in terms of the waiting time needed to change the number of sub-carriers. If the user demands drastically increase such as just after a disaster, the waiting time due to a chain-change of bandwidth becomes excessive because disaster priority telephone services are time-critical. This paper proposes a Grouped-elastic spectrum allocation scheme to satisfy the tolerable waiting time of the service in an optical fiber link. Spectra are grouped to restrict a waiting time in the proposed scheme. In addition, the proposed scheme determines a bandwidth margin between neighbor spectra to spectra to prevent frequent reallocation by estimating real traffic behavior in each group. Numerical results show that the bandwidth requirements can be minimized while satisfying the waiting time constraints. Additionally measurement granularity and channel alignment are discussed.

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.

In this paper, a new effective C/N0 theoretical model for global navigation satellite system (GNSS) receiver is proposed, in the presence of continuous wave interference (CWI). The proposed model is derived based on an interesting finding, correlator may output direct current (DC) in the presence of CWI. The DC introduced by CWI eventually leads to increase of carrier power estimation. It is totally different from current assumption that interference just causes noise power increase after correlation. The proposed model is verified by simulation.

In heterogenous networks (HetNets), the deployment of small cells with the reuse of limited frequency resources to improve the spectral efficiency results in cross- and co-tier interference. In addition, the excessive power usage in such networks is also a critical problem. In this paper, we propose precoding and postcoding schemes to tackle interference and energy efficiency (EE) challenges in the two-tier downlink multiple-input-multiple-output (MIMO) HetNets. We propose transmission strategies based on hierarchical partial coordination (HPC) of the macro cell and small cells to reduce channel state information (CSI) exchange and guarantee the quality of service (QoS) in the upper tier with any change of network deployment in the lower tier. We employ the interference alignment (IA) scheme to cancel cross- and co-tier interference. Additionally, to maximize the EE, power allocation schemes in each tier are proposed based on a combination of Dinkelbach's method and the bisection searching approach. To investigate insights on the optimization problem, a theoretical analysis on the relationship between the maximum achievable EE and the transmit power is derived. Simulation results prove the superior EE performance of the proposed EE maximization scheme over the sum rate maximization approach and confirm the validity of our theoretical findings.

Second-order sampling of 2-D frequency distributions is examined in this paper. When a figure in the frequency space can fill up the entire frequency space by tiling, we call this figure a tiling cluster. We also introduce the concept of pair regions. The results obtained for the second-order sampling of 1-D and 2-D frequency distributions are arranged using these two concepts. The sampling functions and sampling positions of second-order sampling of a 2-D rectangular-complement highpass frequency distribution, which have not been solved until now, are explicitly presented by using these two concepts.

We propose a microphone array speech enhancement method that integrates spatial-cue-based source power spectral density (PSD) estimation and statistical speech model-based PSD estimation. The goal of this research was to clearly pick up target speech even in noisy environments such as crowded places, factories, and cars running at high speed. Beamforming with post-Wiener filtering is commonly used in many conventional studies on microphone-array noise reduction. For calculating a Wiener filter, speech/noise PSDs are essential, and they are estimated using spatial cues obtained from microphone observations. Assuming that the sound sources are sparse in the temporal-spatial domain, speech/noise PSDs may be estimated accurately. However, PSD estimation errors increase under circumstances beyond this assumption. In this study, we integrated speech models and PSD-estimation-in-beamspace method to correct speech/noise PSD estimation errors. The roughly estimated noise PSD was obtained frame-by-frame by analyzing spatial cues from array observations. By combining noise PSD with the statistical model of clean-speech, the relationships between the PSD of the observed signal and that of the target speech, hereafter called the observation model, could be described without pre-training. By exploiting Bayes' theorem, a Wiener filter is statistically generated from observation models. Experiments conducted to evaluate the proposed method showed that the signal-to-noise ratio and naturalness of the output speech signal were significantly better than that with conventional methods.