For embedded systems, verifying both real-time properties and logical validity are important. The embedded system is not only required to the accurate operation but also required to strictly real-time properties. To verify real-time properties is a key problem in model checking. In order to verify real-time properties of assembly program, we develop the simulator to propose the model checking method for verifying assembly programs. Simultaneously, we propose a timed Kripke structure and implement the simulator of the robot's processor to be verified. We propose the timed Kripke structure including the execution time which extends Kripke structure. For the input assembly program, the simulator generates timed Kripke structure by dynamic program analysis. Also, we implement model checker after generating timed Kripke structure in order to verify whether timed Kripke structure satisfies RTCTL formulas. Finally, to evaluate a proposed method, we conduct experiments with the implementation of the verification system. To solve the real problem, we have experimented with real microcontroller software.
Yoshiki TAKAI Mamoru FUKUCHI Chihiro MATSUI Reika KINOSHITA Ken TAKEUCHI
This paper analyzes the optimal SSD configuration including emerging non-volatile memories such as quadruple-level cell (QLC) NAND flash memory [1] and storage class memories (SCMs). First, SSD performance and SSD endurance lifetime of hybrid SSD are evaluated in four configurations: 1) single-level cell (SLC)/QLC NAND flash, 2) SCM/QLC NAND flash, 3) SCM/triple-level cell (TLC)/QLC NAND flash and 4) SCM/TLC NAND flash. Furthermore, these four configurations are compared in limited cost. In case of cold workloads or high total SSD cost assumption, SCM/TLC NAND flash hybrid configuration is recommended in both SSD performance and endurance lifetime. For hot workloads with low total SSD cost assumption, however, SLC/QLC NAND flash hybrid configuration is recommended with emphasis on SSD endurance lifetime. Under the same conditions as above, SCM/TLC/QLC NAND flash tri-hybrid is the best configuration in SSD performance considering cost. In particular, for prxy_0 (write-hot workload), SCM/TLC/QLC NAND flash tri-hybrid achieves 67% higher IOPS/cost than SCM/TLC NAND flash hybrid. Moreover, the configurations with the highest IOPS/cost in each workload and cost limit are picked up and analyzed with various types of SCMs. For all cases except for the case of prxy_1 with high total SSD cost assumption, middle-end SCM (write latency: 1us, read latency: 1us) is recommended in performance considering cost. However, for prxy_1 (read-hot workload) with high total SSD cost assumption, high-end SCM (write latency: 100ns, read latency: 100ns) achieves the best performance.
Han-Ying LIN Chien-Chieh HUANG Wen-Whei CHANG Jen-Tzung CHIEN
This study presents a new method to exploit both accent and grouping structures of music in meter estimation. The system starts by extracting autocorrelation-based features that characterize accent periodicities. Based on the local boundary detection model, we construct grouping features that serve as additional cues for inferring meter. After the feature extraction, a multi-layer cascaded classifier based on neural network is incorporated to derive the most likely meter of input melody. Experiments on 7351 folk melodies in MIDI files indicate that the proposed system achieves an accuracy of 95.76% for classification into nine categories of meters.
Takuya SAKAMOTO Koji NISHIMURA
An analytic expression of the Capon spectrum is derived for two uncorrelated incident signals. On the basis of this theoretical formulation, we discuss the effect of a factor arising from the inner product of mode vectors with respect to the incident angles, which compromises the resolution. We show numerical examples to demonstrate the effect that the inner product of mode vectors has on the shape of the Capon spectrum.
Yifan WEI Wanchun LI Yuning GUO Hongshu LIAO
This paper presents a three-dimensional (3D) spatial localization algorithm by using multiple one-dimensional uniform linear arrays (ULA). We first discuss geometric features of the angle-of-arrival (AOA) measurements of the array and present the corresponding principle of spatial cone angle intersection positioning with an angular measurement model. Then, we propose a new positioning method with an analytic study on the geometric dilution of precision (GDOP) of target location in different cases. The results of simulation show that the estimation accuracy of this method can attain the Cramér-Rao Bound (CRB) under low measurement noise.
Taeyoung JUNG Hyuk-Ju KWON Joonku HAHN Sung-Hak LEE
We propose image synthesizing using luminance adapted range compression and detail-preserved blending. Range compression is performed using the correlated visual gamma then image blending is performed by local adaptive mixing and selecting method. Simulations prove that the proposed method reproduces natural images without any increase in noise or color desaturation.
Dongyeong KIM Dawoon KWON Junghwan SONG
The boomerang connectivity table (BCT) was introduced by C. Cid et al. Using the BCT, for SPN block cipher, the dependency between sub-ciphers in boomerang structure can be computed more precisely. However, the existing method to generate BCT is difficult to be applied to the ARX-based cipher, because of the huge domain size. In this paper, we show a method to compute the dependency between sub-ciphers in boomerang structure for modular addition. Using bit relation in modular addition, we compute the dependency sequentially in bitwise. And using this method, we find boomerang characteristics and amplified boomerang characteristics for the ARX-based ciphers LEA and SPECK. For LEA-128, we find a reduced 15-round boomerang characteristic and reduced 16-round amplified boomerang characteristic which is two rounds longer than previous boomerang characteristic. Also for SPECK64/128, we find a reduced 13-round amplified boomerang characteristic which is one round longer than previous rectangle characteristic.
Kouji HIRATA Hiroshi YAMAMOTO Shohei KAMAMURA Toshiyuki OKA Yoshihiko UEMATSU Hideki MAEDA Miki YAMAMOTO
This paper proposes a traveling maintenance method based on the resource pool concept, as a new network maintenance model. For failure recovery, the proposed method utilizes permissible time that is ensured by shared resource pools. In the proposed method, even if a failure occurs in a communication facility, maintenance staff wait for occurrence of successive failures in other communication facilities during the permissible time instead of immediately tackling the failure. Then, the maintenance staff successively visit the communication facilities that have faulty devices and collectively repair them. Therefore, the proposed method can reduce the amount of time that the maintenance staff take for fault recovery. Furthermore, this paper provides a system design that optimizes the proposed traveling maintenance according to system requirements determined by the design philosophy of telecommunication networks. Through simulation experiments, we show the effectiveness of the proposed method.
Mobile edge computing (MEC) is a new computing paradigm, which provides computing support for resource-constrained user equipments (UEs). In this letter, we design an effective incentive framework to encourage MEC operators to provide computing service for UEs. The problem of jointly allocating communication and computing resources to maximize the revenue of MEC operators is studied. Based on auction theory, we design a multi-round iterative auction (MRIA) algorithm to solve the problem. Extensive simulations have been conducted to evaluate the performance of the proposed algorithm and it is shown that the proposed algorithm can significantly improve the overall revenue of MEC operators.
Qingbo WANG Gaoqi DOU Ran DENG Jun GAO
The current orthogonal cooperative system (OCS) achieves diversity through the use of relays and the consumption of an additional time slot (TS). To guarantee the orthogonality of the received signal and avoid the mutual interference at the destination, the source has to be mute in the second TS. Consequently, the spectral efficiency (SE) is halved. In this paper, linear constellation precoded orthogonal frequency division multiplexing with index modulation (LCP-OFDM-IM) based OCS is proposed, where the source activates the complementary subcarriers to convey the symbols over two TSs. Hence the source can consecutively transmit information to the destination without the mutual interference. Compared with the current OFDM based OCS, the LCP-OFDM-IM based OCS can achieve a higher SE, since the subcarrier activation patterns (SAPs) can be exploited to convey additional information. Furthermore, the optimal precoder, in the sense of maximizing the minimum Euclidean distance of the symbols conveyed on each subcarrier over two TSs, is provided. Simulation results show the superiority of the LCP-OFDM-IM based OCS over the current OFDM based OCS.
Yuji MIZUTANI Hiroto KURIKI Yosuke KODAMA Keiichi MIZUTANI Takeshi MATSUMURA Hiroshi HARADA
The conventional universal filtered-DFT-spread-OFDM (UF-DFTs-OFDM) can drastically improve the out-of-band emission (OOBE) caused by the discontinuity between symbols in the conventional cyclic prefix-based DFTs-OFDM (CP-DFTs-OFDM). However, the UF-DFTs-OFDM degrades the communication quality in a long-delay multipath fading environment due to the frequency-domain ripple derived from the long transition time of the low pass filter (LPF) corresponding to the guard interval (GI). In this paper, we propose an enhanced UF-DFTs-OFDM (eUF-DFTs-OFDM) that achieves significantly low OOBE and high communication quality even in a long-delay multipath fading environment. The eUF-DFTs-OFDM applies an LPF with quite short length in combination with the zero padding (ZP) or the CP process. Then, the characteristics of the OOBE, peak-to-average power ratio (PAPR), and block error rate (BLER) are evaluated by computer simulation with the LTE uplink parameters. The result confirms that the eUF-DFTs-OFDM can improve the OOBE by 22.5dB at the channel-edge compared to the CP-DFTs-OFDM, and also improve the ES/N0 to achieve BLER =10-3 by about 2.5dB for QPSK and 16QAM compared to the UF-DFTs-OFDM. For 64QAM, the proposed eUF-DFTs-ODFDM can eliminate the error floor of the UF-DFTs-OFDM. These results indicate that the proposed eUF-DFTs-OFDM can significantly reduce the OOBE while maintaining the same level of communication quality as the CP-DFTs-OFDM even in long-delay multipath environment.
Ye PENG Wentao ZHAO Wei CAI Jinshu SU Biao HAN Qiang LIU
Due to the superior performance, deep learning has been widely applied to various applications, including image classification, bioinformatics, and cybersecurity. Nevertheless, the research investigations on deep learning in the adversarial environment are still on their preliminary stage. The emerging adversarial learning methods, e.g., generative adversarial networks, have introduced two vital questions: to what degree the security of deep learning with the presence of adversarial examples is; how to evaluate the performance of deep learning models in adversarial environment, thus, to raise security advice such that the selected application system based on deep learning is resistant to adversarial examples. To see the answers, we leverage image classification as an example application scenario to propose a framework of Evaluating Deep Learning for Image Classification (EDLIC) to conduct comprehensively quantitative analysis. Moreover, we introduce a set of evaluating metrics to measure the performance of different attacking and defensive techniques. After that, we conduct extensive experiments towards the performance of deep learning for image classification under different adversarial environments to validate the scalability of EDLIC. Finally, we give some advice about the selection of deep learning models for image classification based on these comparative results.
This paper presents a Siamese architecture model with two identical Convolutional Neural Networks (CNNs) to identify code clones; two code fragments are represented as Abstract Syntax Trees (ASTs), CNN-based subnetworks extract feature vectors from the ASTs of pairwise code fragments, and the output layer produces how similar or dissimilar they are. Experimental results demonstrate that CNN-based feature extraction is effective in detecting code clones at source code or bytecode levels.
Picross 3D is a popular single-player puzzle video game for the Nintendo DS. It presents a rectangular parallelepiped (i.e., rectangular box) made of unit cubes, some of which must be removed to construct an object in three dimensions. Each row or column has at most one integer on it, and the integer indicates how many cubes in the corresponding 1D slice remain when the object is complete. Kusano et al. showed that Picross 3D is NP-complete and Kimura et al. showed that the counting version, the another solution problem, and the fewest clues problem of Picross 3D are #P-complete, NP-complete, and Σ2P-complete, respectively, where those results are shown for the restricted input that the rectangular parallelepiped is of height four. On the other hand, Igarashi showed that Picross 3D is NP-complete even if the height of the input rectangular parallelepiped is one. Extending the result by Igarashi, we in this paper show that the counting version, the another solution problem, and the fewest clues problem of Picross 3D are #P-complete, NP-complete, and Σ2P-complete, respectively, even if the height of the input rectangular parallelepiped is one. Since the height of the rectangular parallelepiped of any instance of Picross 3D is at least one, our hardness results are best in terms of height.
Mamoru FUKUCHI Chihiro MATSUI Ken TAKEUCHI
This paper analyzes the system-level performance of Storage Class Memory (SCM)/NAND flash hybrid solid-state drives (SSDs) and SCM/NAND flash/NAND flash tri-hybrid SSDs in difference types of NAND flash memory. There are several types of NAND flash memory, i.e. 2-dimensional (2D) or 3-dimensional (3D), charge-trap type (CT) and floating-gate type (FG) and multi-level cell (MLC) or triple-level cell (TLC). In this paper, the following four types of NAND flash memory are analyzed: 1) 3D CT TLC, 2) 3D FG TLC, 3) 2D FG TLC, and 4) 2D FG MLC NAND flash. Regardless of read- and write-intensive workloads, SCM/NAND flash hybrid SSD with low cost 3D CT TLC NAND flash achieves the best performance that is 20% higher than that with higher cost 2D FG MLC NAND flash. The performance improvement of 3D CT TLC NAND flash can be obtained by the short write latency. On the other hand, in case of tri-hybrid SSD, SCM/3D CT TLC/3D CT TLC NAND flash tri-hybrid SSD improves the performance 102% compared to SCM/2D FG MLC/3D CT TLC NAND flash tri-hybrid SSD. In addition, SCM/2D FG MLC/2D FG MLC NAND flash tri-hybrid SSD shows 49% lower performance than SCM/2D FG MLC/3D CT TLC NAND flash tri-hybrid SSD. Tri-hybrid SSD flash with 3D CT TLC NAND flash is the best performance in tri-hybrid SSD thanks to larger block size and word-line (WL) write. Therefore, in 3D CT TLC NAND flash based SSDs, higher cost MLC NAND flash is not necessary for hybrid SSD and tri-hybrid SSD for data center applications.
Shota SHIRATORI Yuichiro FUJIMOTO Kinya FUJITA
In order not to disrupt a team member concentrating on his/her own task, the interrupter needs to wait for a proper time. In this research, we examined the feasibility of predicting prospective interruptible times of office workers who use PCs. An analysis of actual working data collected from 13 participants revealed the relationship between uninterruptible durations and four features, i.e. type of application software, rate of PC operation activity, activity ratio between keystrokes and mouse clicks, and switching frequency of application software. On the basis of these results, we developed a probabilistic work continuance model whose probability changes according to the four features. The leave-one-out cross-validation indicated positive correlations between the actual and the predicted durations. The medians of the actual and the predicted durations were 539 s and 519 s. The main contribution of this study is the demonstration of the feasibility to predict uninterruptible durations in an actual working scenario.
Toshinori SUZUKI Masahiro KAMINAGA
To increase the number of wireless devices such as mobile or IoT terminals, cryptosystems are essential for secure communications. In this regard, random number generation is crucial because the appropriate function of cryptosystems relies on it to work properly. This paper proposes a true random number generator (TRNG) method capable of working in wireless communication systems. By embedding a TRNG in such systems, no additional analog circuits are required and working conditions can be limited as long as wireless communication systems are functioning properly, making TRNG method cost-effective. We also present some theoretical background and considerations. We next conduct experimental verification, which strongly supports the viability of the proposed method.
Takashi MATSUI Kyozo TSUJIKAWA Takehisa OKUDA Nobutomo HANZAWA Yuto SAGAE Kazuhide NAKAJIMA Yasuyuki FUJIYA Kazuyuki SHIRAKI
We investigate the potential of photonic crystal fiber (PCF) to realize high quality and high-power transmission. We utilize the PCF with a quasi-uniform air-hole structure, and numerically clarify that the quasi-uniform PCF can realize the effective area (Aeff) of about 500µm2 with bending loss comparable with that of a conventional single-mode fiber for telecom use by considering the quasi single-mode transmission. We then apply the quasi-uniform PCF to kW-class high-power beam delivery for the single-mode laser processing. The cross-sectional design of the PCF with the high-power delivery potential of more than 300kW·m is numerically and experimentally revealed. A 10kW single-mode beam at 1070nm is successfully delivered over a 30m-long optical fiber cable containing a fabricated PCF with single-mode class beam quality of M2 =1.7 for the first time.
Atsushi TANIGUCHI Takeru INOUE Kohei MIZUNO Takashi KURIMOTO Atsuko TAKEFUSA Shigeo URUSHIDANI
Communication networks are now an essential infrastructure of society. Many services are constructed across multiple network domains. Therefore, the reliability of multi-domain networks should be evaluated to assess the sustainability of our society, but there is no known method for evaluating it. One reason is the high computation complexity; i.e., network reliability evaluation is known to be #P-complete, which has prevented the reliability evaluation of multi-domain networks. The other reason is intra-domain privacy; i.e., network providers never disclose the internal data required for reliability evaluation. This paper proposes a novel method that computes the lower and upper bounds of reliability in a distributed manner without requiring privacy disclosure. Our method is solidly based on graph theory, and is supported by a simple protocol that secures intra-domain privacy. Experiments on real datasets show that our method can successfully compute the reliability for 14-domain networks in one second. The reliability is bounded with reasonable errors; e.g., bound gaps are less than 0.1% for reliable networks.
In this study, product of two independent and non-identically distributed (i.n.i.d.) random variables (RVs) for κ-µ fading distribution and α-µ fading distribution is considered. The statistics of the product of RVs has been broadly applied in a large number of communications fields, such as cascaded fading channels, multiple input multiple output (MIMO) systems, radar communications and cognitive radios (CR). Exact close-form expressions of probability density function (PDF) and cumulative distribution function (CDF) with exact series formulas for the product of two i.n.i.d. fading distributions κ-µ and α-µ are deduced more accurately to represent the provided product expressions and generalized composite multipath shadowing models. Furthermore, ergodic channel capacity (ECC) is obtained to measure maximum fading channel capacity. At last, interestingly unlike κ-µ, η-µ, α-µ in [9], [17], [18], these analytical results are validated with Monte Carlo simulations and it shows that for provided κ-µ/α-µ model, non-linear parameter has more important influence than multipath component in PDF and CDF, and when the ratio between the total power of the dominant components and the total power of the scattered waves is same, higher α can significantly improve channel capacity over composite fading channels.