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.

Wireless sensor networks are being used in many disaster-related applications. Certain types of disasters are studied and modeled with different and dynamic risk estimations in different areas, hence requiring different levels of monitoring. Such nonuniform and dynamic coverage requirements pose a challenge to a sensor coverage problem. This work proposes the Mobile sensor Relocation using Delaunay triangulation And Shifting on Hill climbing (MR-DASH) approach, which calculates an appropriate location for each mobile sensor as an attempt to maximize coverage ratio. Based on a probabilistic sensing model, it constructs a Delaunay triangulation from static sensors' locations and vertices of interesting regions. The resulting triangles are then prioritized based on their sizes and corresponding levels of requirement so that mobile sensors can be relocated accordingly. The proposed method was both compared with an existing previous work and demonstrated with real-world disaster scenarios by simulation. The result showed that MR-DASH gives appropriate target locations that significantly improve the coverage ratio with relatively low total sensors' moving distance, while properly adapting to variations in coverage requirements.

Controlling synchrony as well as desynchrony in a network of neuronal oscillators has been one of the focus issues in nonlinear science and engineering. It has been well known that spike stimuli injected commonly to multiple neurons can synchronize them if the strength of the common spike stimuli is high enough. Our recent study showed that this common spike-induced synchrony could be suppressed by introducing heterogeneity to inhibitory connections, through which the common spikes are transmitted. The aim of the present study is apply this methodology to electronic neurons as a real physical hardware. Using an Axon-Hillock circuit that represents basic properties of the leaky integrate-and-fire (LIF) neuron, our experiment demonstrated that the method was quite effective for desynchronizing the neuron circuits. The experimental results are also in a good agreement with the linear response theory that describes the input-output relationship of LIF neurons. Our method of suppressing the neuronal synchrony should be of practical use for enhancement of neural information processing as well as for improvement of pathological state of the brain.

The purpose of this study was to identify the key variables that determine the quality of the auditory environment, for the purposes of workplace auditory design and assessment. To this end, we characterized changes in oscillatory neural activity in electroencephalographic (EEG) data recorded from subjects who performed an intellectual activity while exposed to fluctuating ambient noise. Seven healthy men participated in the study. Subjects performed a verbal and spatial task that used the 3-back task paradigm to study working memory. During the task, subjects were presented with auditory stimuli grouped by increasing high-frequency content: (1) a sound with frequencies similar to Brownian noise and no modulation; (2) an amplitude-modulated sound with frequencies similar to white noise; (3) amplitude-modulated pink noise; and (4) amplitude-modulated Brownian noise. Upon presentation, we observed a characteristic change in three EEG bands: theta (4-8Hz), alpha (8-13Hz), and beta (13-30Hz). In particular, a frequency-dependent enhancement and reduction of power was observed in the theta and beta bands, respectively.

A lot of encryption and watermarking schemes have been developed as countermeasures to protect copyrights of broadcast or multicast content from malicious subscribers (traitors) that make pirate receivers (PRs) to use the content illegally. However, solo use of these schemes does not necessarily work well. Traitor tracing encryption schemes are a type of broadcasting encryption and have been developed for broadcasting and multicast services. There are multiple distinct decryption keys for each encryption key, and each service subscriber is given a unique decryption key. Any subscriber that redistributes his or her decryption key to a third party or who uses it and maybe other keys to make a PR can be identified with using the tracing algorithm of the scheme that is used by the services. However, almost all previous schemes have the same weakness; that is, they are vulnerable to an attack (content comparison attack). This is a concrete example such that solo use of the scheme does not work well. The attack involves multiple distinct decryption keys and a content-data comparison mechanism. We have developed a method, called complementary traitor tracing method (CTT), that makes traitor tracing schemes secure against content comparison attacks. It makes it impossible for PRs to distinguish ordinary content data from test data and makes traitor tracing schemes effective against all PRs, even those with multiple distinct decryption keys. CTT is made with a simple combination of schemes that are absolutely necessary. It makes broadcasting or multicast services secure.

Sound source localization is an essential technique in many applications, e.g., speech enhancement, speech capturing and human-robot interaction. However, the performance of traditional methods degrades in noisy or reverberant environments, and it is sensitive to the spatial location of sound source. To solve these problems, we propose a sound source localization framework based on bi-direction interaural matching filter (IMF) and decision weighting fusion. Firstly, bi-directional IMF is put forward to describe the difference between binaural signals in forward and backward directions, respectively. Then, a hybrid interaural matching filter (HIMF), which is obtained by the bi-direction IMF through decision weighting fusion, is used to alleviate the affection of sound locations on sound source localization. Finally, the cosine similarity between the HIMFs computed from the binaural audio and transfer functions is employed to measure the probability of the source location. Constructing the similarity for all the spatial directions as a matrix, we can determine the source location by Maximum A Posteriori (MAP) estimation. Compared with several state-of-the-art methods, experimental results indicate that HIMF is more robust in noisy environments.

To efficiently utilize storage resources, the in-network caching system of Information-Centric Networking has to deal with the popularity of huge content chunks which could cause large memory consumption. This paper presents a Popularity Monitoring based Gain-aware caching scheme, called PMG, which is an integrated design of cache placement and popularity monitoring. In PMG, by taking into account both the chunk popularity and the consumption saving of single cache hit, the cache placement process is transformed into a weighted popularity comparison, while the chunks with high cache gain are placed on the node closer to the content consumer. A Bloom Filter based sliding window algorithm, which is self-adaptive to the dynamic request rate, is proposed to capture the chunks with higher caching gain by Inter-Reference Gap (IRG) detection. Analysis shows that PMG can drastically reduce the memory consumption of popularity monitoring, and the simulation results confirm that our scheme can achieve popularity based cache placement and get better performance in terms of bandwidth saving and cache hit ratio when content popularity changes dynamically.

An overview of the evolution of intelligent transport systems (ITS) supported by advances in information and communication technologies is presented. Focusing on a sensing platform as one of the ITS applications, this paper presents a survey on vehicular ad hoc network-based geographic routing. In addition to the minimum requirement of street-awareness based on street maps, traffic and packet-awareness are considered essential to achieve acceptable packet delivery performance. In particular, in addition to statistical information, real-time traffic and packet level information are indispensable for making routing protocols feasible and effective. Considering traffic conditions that are highly space- and time-dependent, static nodes can be used to assist with geographic routing, and a protocol workable under a partial deployment of static nodes is considered.

In this paper, we propose a single-channel speech enhancement method for a push-to-talk enabled wireless communication device. The proposed method is based on adaptive weighted β-order spectral amplitude estimation under speech presence uncertainty and enhanced instantaneous phase estimation in order to achieve flexible and effective noise reduction while limiting the speech distortion due to different noise conditions. Experimental results confirm that the proposed method delivers higher voice quality and intelligibility than the reference methods in various noise environments.

Two plasmonic band-bass filters are analyzed: one is a grating-type filter and the other is a slit-type filter. The former shows a band-pass characteristic with a high transmission for a two-dimensional structure, while the latter exhibits a high transmission even for a three-dimensional structure with a thin metal layer.

Mixed-signal integrated circuit design and simulation highly rely on behavioral models of circuit blocks. Such models are used for the validation of design specification, optimization of system topology, and behavioral synthesis using a description language, etc. However, automatic behavioral model generation is still in its early stages; in most scenarios designers are responsible for creating behavioral models manually, which is time-consuming and error prone. In this paper an automatic behavioral model generation method for switched-capacitor (SC) integrator is proposed. This technique is based on symbolic circuit modeling with approximation, by which parametric behavioral integrator model can be generated. Such parametric models can be used in circuit design subject to severe process variational. It is demonstrated that the automatically generated integrator models can accurately capture process variation effects on arbitrarily selected circuit elements; furthermore, they can be applied to behavioral simulation of SC Sigma-Delta modulators (SDMs) with acceptable accuracy and speedup. The generated models are compared to a recently proposed manually generated behavioral integrator model in several simulation settings.

An on-chip monitoring circuit using a sub-sampling scheme, which consists of a 6-bit flash analog-to-digital converter (ADC) and a 51-phase phase-locked loop (PLL)-based frequency synthesizer, is proposed to analyze the signal integrity of a single-ended 8-Gb/s octal data rate (ODR) chip-to-chip interface with a source synchronous clocking scheme.

Noise and area consumption has been a trade-off in circuit design. Especially for switched-capacitor filters (SCF), kT/C noise gives a limitation to the minimum value of unit capacitance. In case of SCFs with a large capacitance spread, this limitation will result in a large area consumption due to large capacitors. This paper introduces a technique to reduce capacitance spread using charge scaling. It will be shown that this technique can reduce total capacitance of SCFs without deteriorating their noise performances. A design method to reduce the output noise of SC low-pass filters (LPF) based on the combination of cut-set scaling, charge scaling and adaptive configuration is proposed. The proposed technique can reduce the output noise voltage by 30% for small input signals.

Liquid crystal displays (LCDs) are suitable as elements underlying wearable and ubiquitous computing thanks to their low power consumption. A technique that uses less power to drive 1-pixel LCDs is proposed. It harvests the charges on the LCD and stores them in an external capacitor for reuse when the polarity changes. A simulation shows that the charge reduction depends on the ratio of the capacitance of the external capacitor to that of the LCD and can reach 50%. An experiment on a prototype demonstrates an almost 30% reduction with large 1-pixel LCDs. With a small 10 × 10mm2 LCD, the overhead of the micro-controller matches the reduction so no improvement could be measured. Though the technique requires longer time for polarity reversal, we confirm that it does not significantly degrade visual quality.

We investigate a quantization error improvement technique using a dual rail configuration for optical quantization. Our proposed optical quantization uses intensity-to-wavelength conversion based on soliton self-frequency shift and spectral compression based on self-phase modulation. However, some unfavorable input peak power regions exist due to stagnations of wavelength shift or distortions of spectral compression. These phenomena could induce a serious quantization error and degrade the effective number of bit (ENOB). In this work, we propose a quantization error improvement technique which can make up for the unfavorable input peak power regions. We experimentally verify the quantization error improvement effect by the proposed technique in 6 bit optical quantization. The estimated ENOB is improved from 5.35 bit to 5.66 bit. In addition, we examine the XPM influence between counter-propagating pulses at high sampling rate. Experimental results and numerical simulation show that the XPM influence is negligible under ∼40 GS/s conditions.

This paper demonstrates the resonant power supply noise reduction effects of STO thin film decoupling capacitors, which are embedded in interposers. The on-interposer STO capacitor consists of SrTiO2 whose dielectric constant is about 20 and is sandwitched by Cu films in an interposer. The on-interposer STO capacitors are directly connected to the LSI PADs so that they provide large decoupling capacitance without package leadframe/bonding wire inductance, resulting in the reduction of the resonant power supply noise. The measured power supply waveforms show significant reduction of the power supply noise, and the Shmoo plots also show the contribution of the STO capacitors to the robust operations of LSIs.

A forward/reverse body bias generator (BBG) which operates under wide supply-range is proposed. Fine-grained body biasing (FGBB) is effective to reduce variability and increase energy efficiency on digital LSIs. Since FGBB requires a number of BBGs to be implemented, simple design is preferred. We propose a BBG with charge pumps for reverse body bias and the BBG operates under wide supply-range from 0.5,V to 1.2,V. Layout of the BBG was designed in a cell-based flow with an AES core and fabricated in a 65~nm CMOS process. Area of the AES core is 0.22 mm$^2$ and area overhead of the BBG is 2.3%. Demonstration of the AES core shows a successful operation with the supply voltage from 0.5,V to 1.2,V which enables the reduction of power dissipation, for example, of 17% at 400,MHz operation.

In recent years, hybrid typestate analysis has been proposed to eliminate unnecessary monitoring instrumentations for runtime monitors at compile-time. Nop-shadows Analysis (NSA) is one of these hybrid typestate analyses. Before generating residual monitors, NSA performs the data-flow analysis which is intra-procedural flow-sensitive and partially context-sensitive to improve runtime performance. Although NSA is precise, there are some cases on which it has little effects. In this paper, we propose three optimizations to further improve the precision of NSA. The first two optimizations try to filter interferential states of objects when determining whether a monitoring instrumentation is necessary. The third optimization refines the inter-procedural data-flow analysis induced by method invocations. We have integrated our optimizations into Clara and conducted extensive experiments on the DaCapo benchmark. The experimental results demonstrate that our first two optimizations can further remove unnecessary instrumentations after the original NSA in more than half of the cases, without a significant overhead. In addition, all the instrumentations can be removed for two cases, which implies the program satisfy the typestate property and is free of runtime monitoring. It comes as a surprise to us that the third optimization can only be effective on 8.7% cases. Finally, we analyze the experimental results and discuss the reasons why our optimizations fail to further eliminate unnecessary instrumentations in some special situations.

Cell voltage equalizers are necessary to ensure years of operation and maximize the chargeable/dischargeable energy of series-connected supercapacitors (SCs). A two-switch voltage equalizer using a series-resonant voltage multiplier operating in frequency-multiplied discontinuous conduction mode (DCM) is proposed for series-connected SCs in this paper. The frequency-multiplied mode virtually increases the operation frequency and hence mitigates the negative impact of the impedance mismatch of capacitors on equalization performance, allowing multi-layer ceramic capacitors (MLCCs) to be used instead of bulky and costly tantalum capacitors, the conventional approach when using voltage multipliers in equalizers. Furthermore, the DCM operation inherently provides the constant current characteristic, realizing the excessive current protection that is desirable for SCs, which experience 0V and equivalently become an equivalent short-circuit load. Experimental equalization tests were performed for eight SCs connected in series under two frequency conditions to verify the improved equalization performance at the increased virtual operation frequencies. The standard deviation of cell voltages under the higher-frequency condition was lower than that under the lower-frequency condition, demonstrating superior equalization performance at higher frequencies.

A number of network monitoring sensors such as honeypot and web crawler have been launched to observe increasingly-sophisticated cyber attacks. Based on these technologies, there have been several large scale network monitoring projects launched to fight against cyber threats on the Internet. Meanwhile, these projects are facing some problems such as Difficulty of collecting wide range darknet, Burden of honeypot operation and Blacklisting problem of honeypot address. In order to address these problems, this paper proposes a novel proactive cyber attack monitoring platform called GHOST sensor, which enables effective utilization of physical and logical resources such as hardware of sensors and monitoring IP addresses as well as improves the efficiency of attack information collection. The GHOST sensor dynamically allocates targeted IP addresses to appropriate sensors so that the sensors can flexibly monitor attacks according to profiles of each attacker. Through an evaluation in a experiment environment, this paper presents the efficiency of attack observation and resource utilization.