In IoT systems, data acquired by many sensors are required. However, since sensor operation depends on the actual environment, it is important to ensure sensor redundancy to improve system reliability in IoT systems. To evaluate the safety of the system, it is important to estimate the achievement probability of the function based on the sensing probability. In this research, we proposed a method to automatically generate a PRISM model from the sensor configuration of the target system and calculate and verify the function achievement probability in the assumed environment. By designing and evaluating iteratively until the target achievement probability is reached, the reliability of the system can be estimated at the initial design phase. This method reduces the possibility that the lack of reliability will be found after implementation and the redesign accompanying it will occur.

In automotive control systems, the potential risks of software defects have been increasing due to growing software complexity driven by advances in electric-electronic control. Some kind of defects such as race conditions can rarely be detected by testing or simulations because these defects manifest themselves only in some rare executions. Model checking, which employs an exhaustive state-space exploration, is effective for detecting such defects. This paper reports our approach to applying model checking techniques to real-world automotive control programs. It is impossible to directly model check such programs because of their large size and high complexity; thus, it is necessary to derive, from the program under verification, a model that is amenable to model checking. Our approach uses the SPIN model checker as well as in-house tools that facilitate this process. One of the key features implemented in these tools is boundary-adjustable program slicing, which allows the user to specify and extract part of the source code that is relevant to the verification problem of interest. The conversion from extracted code into Promela, SPIN's input language, is performed using one of the tools in a semi-automatic manner. This approach has been used for several years in practice and found to be useful even when the code size of the software exceeds 400 KLOC.

5G network will serve billions of people worldwide in the near future and protecting human privacy from being violated is one of its most important goals. In this paper, we carefully studied the 5G authentication protocols (namely 5G AKA and EAP-AKA') and a location sniffing attack exploiting 5G authentication protocols vulnerability is found. The attack can be implemented by an attacker through inexpensive devices. To cover this vulnerability, a fix scheme based on the existing PKI mechanism of 5G is proposed to enhance the authentication protocols. The proposed scheme is successfully verified with formal methods and automatic verification tool TAMARIN. Finally, the communication overhead, computational cost and storage overhead of the scheme are analyzed. The results show that the security of the fixed authentication protocol is greatly improved by just adding a little calculation and communication overhead.

The choreography realization problem is a design challenge for systems based on service-oriented architecture. In our previous studies, we studied the problem on a case where choreography was given by one or two scenarios and was expressed by an acyclic relation of events; we introduced the notion of re-constructibility as a property of acyclic relations to be satisfied. However, when choreography is defined by multiple scenarios, the resulting behavior cannot be expressed by an acyclic relation. An event structure is composed of an acyclic relation and a conflict relation. Because event structures are a generalization of acyclic relations, a wider class of systems can be expressed by event structures. In this paper, we propose the use of event structures to express choreography, introduce the re-constructibility of event structures, and show a necessary condition for an event structure to be re-constructible.

Blockchain is a distributed ledger system composed of a P2P network and is used for a wide range of applications, such as international remittance, inter-individual transactions, and asset conservation. In Blockchain systems, tamper resistance is enhanced by the property of transaction that cannot be changed or deleted by everyone including the creator of the transaction. However, this property also becomes a problem that unintended transaction created by miss operation or secret key theft cannot be corrected later. Due to this problem, once an illegal transaction such as theft occurs, the damage will expand. To suppress the damage, we need countermeasures, such as detecting illegal transaction at high speed and correcting the transaction before approval. However, anomaly detection in the Blockchain at high speed is computationally heavy, because we need to repeat the detection process using various feature quantities and the feature extractions become overhead. In this paper, to accelerate anomaly detection, we propose to cache transaction information necessary for extracting feature in GPU device memory and perform both feature extraction and anomaly detection in the GPU. We also propose a conditional feature extraction method to reduce computation cost of anomaly detection. We employ anomaly detection using K-means algorithm based on the conditional features. When the number of users is one million and the number of transactions is 100 millions, our proposed method achieves 8.6 times faster than CPU processing method and 2.6 times faster than GPU processing method that does not perform feature extraction on the GPU. In addition, the conditional feature extraction method achieves 1.7 times faster than the unconditional method when the number of users satisfying a given condition is 200 thousands out of one million.

Social media channels, such as Facebook, Twitter, and Instagram, have altered our world forever. People are now increasingly connected than ever and reveal a sort of digital persona. Although social media certainly has several remarkable features, the demerits are undeniable as well. Recent studies have indicated a correlation between high usage of social media sites and increased depression. The present study aims to exploit machine learning techniques for detecting a probable depressed Twitter user based on both, his/her network behavior and tweets. For this purpose, we trained and tested classifiers to distinguish whether a user is depressed or not using features extracted from his/her activities in the network and tweets. The results showed that the more features are used, the higher are the accuracy and F-measure scores in detecting depressed users. This method is a data-driven, predictive approach for early detection of depression or other mental illnesses. This study's main contribution is the exploration part of the features and its impact on detecting the depression level.

Link prediction, the computational problem of determining whether there is a link between two objects, is important in machine learning and data mining. Feature-based link prediction, in which the feature vectors of the two objects are given, is of particular interest because it can also be used for various identification-related problems. Although the factorization machine and the higher-order factorization machine (HOFM) are widely used for feature-based link prediction, they use feature combinations not only across the two objects but also from the same object. Feature combinations from the same object are irrelevant to major link prediction problems such as predicting identity because using them increases computational cost and degrades accuracy. In this paper, we present novel models that use higher-order feature combinations only across the two objects. Since there were no algorithms for efficiently computing higher-order feature combinations only across two objects, we derive one by leveraging reported and newly obtained results of calculating the ANOVA kernel. We present an efficient coordinate descent algorithm for proposed models. We also improve the effectiveness of the existing one for the HOFM. Furthermore, we extend proposed models to a deep neural network. Experimental results demonstrated the effectiveness of our proposed models.

While existing inference engines solved real world problems using probabilistic knowledge representation, one challenging task is to efficiently utilize the representation under a situation of uncertainty during conflict resolution. This paper presents a new approach to straightforwardly combine a rule-based system (RB) with a probabilistic graphical inference framework, i.e., naïve Bayesian network (BN), towards probabilistic argumentation via a so-called probabilistic assumption-based argumentation (PABA) framework. A rule-based system (RB) formalizes its rules into defeasible logic under the assumption-based argumentation (ABA) framework while the Bayesian network (BN) provides probabilistic reasoning. By knowledge integration, while the former provides a solid testbed for inference, the latter helps the former to solve persistent conflicts by setting an acceptance threshold. By experiments, effectiveness of this approach on conflict resolution is shown via an example of liver disorder diagnosis.

In this paper, we propose an interactive system for controlling the pressure while cutting paper with a knife. The purpose is to improve the cutting skill of novices learning the art of paper-cutting. Our system supports skill improvement for novices by measuring and evaluating their cutting pressure in real-time. In this study, we use a knife with a blade attached to a stylus with a pressure sensor, which can measure the pressure, coordinates, and cutting time. We have developed a similar support system using a stylus and a tablet device. This system allows the user to experience the pressure of experts through tracing. Paper-cutting is created by cutting paper with a knife. The practice system in this paper provides practice in an environment more akin to the production of paper cutting. In the first experiment, we observed differences in cutting ability by comparing cutting pressures between novices and experts. As a result, we confirmed that novices cut paper at a higher pressure than experts. We developed a practice system that guides the novices on controlling the pressure by providing information on the cutting pressure values of experts. This system shows the difference in pressure between novices and experts using a synchronous display of color and sound. Using these functions, novices learn to adjust their cutting pressure according to that of experts. Determining the right cutting pressure is a critical skill in the art of paper-cutting, and we aim to improve the same with our system. In the second experiment, we tested the effect of the practice system on the knife device. We compared the changes in cutting pressure with and without our system, the practice methods used in the workshop, and the previously developed stylus-based support system. As a result, we confirmed that practicing with the knife device had a better effect on the novice's skill in controlling cutting pressure than other practice methods.

This study focuses on computer based foreign language vocabulary learning systems. Our objective is to automatically build vocabulary decks with desired levels of relative difficulty relations. To realize this goal, we exploit the fact that word frequency is a good indicator of vocabulary difficulty. Subsequently, for composing the decks, we pose two requirements as uniformity and diversity. Namely, the difficulty level of the cards in the same deck needs to be uniform enough so that they can be grouped together and difficulty levels of the cards in different decks need to be diverse enough so that they can be grouped in different decks. To assess uniformity and diversity, we use rank-biserial correlation and propose an iterative algorithm, which helps in attaining desired levels of uniformity and diversity based on word frequency in daily use of language. In experiments, we employed a spaced repetition flashcard software and presented users various decks built with the proposed algorithm, which contain cards from different content types. From users' activity logs, we derived several behavioral variables and examined the polyserial correlation between these variables and difficulty levels across different word classes. This analysis confirmed that the decks compiled with the proposed algorithm induce an effect on behavioral variables in line with the expectations. In addition, a series of experiments with decks involving varying content types confirmed that this relation is independent of word class.

Some non-acoustic modalities have the ability to reveal certain speech attributes that can be used for synthesizing speech signals without acoustic signals. This study validated the use of ultrasonic Doppler frequency shifts caused by facial movements to implement a silent speech interface system. A 40kHz ultrasonic beam is incident to a speaker's mouth region. The features derived from the demodulated received signals were used to estimate the speech parameters. A nonlinear regression approach was employed in this estimation where the relationship between ultrasonic features and corresponding speech is represented by deep neural networks (DNN). In this study, we investigated the discrepancies between the ultrasonic signals of audible and silent speech to validate the possibility for totally silent communication. Since reference speech signals are not available in silently mouthed ultrasonic signals, a nearest-neighbor search and alignment method was proposed, wherein alignment was achieved by determining the optimal pair of ultrasonic and audible features in the sense of a minimum mean square error criterion. The experimental results showed that the performance of the ultrasonic Doppler-based method was superior to that of EMG-based speech estimation, and was comparable to an image-based method.

Finding the correspondence between two images of the same object or scene is an active research field in computer vision. This paper develops a rapid and effective Content-based Superpixel Image matching and Stitching (CSIS) scheme, which utilizes the content of superpixel through multi-features fusion technique. Unlike popular keypoint-based matching method, our approach proposes a superpixel internal feature-based scheme to implement image matching. In the beginning, we make use of a novel superpixel generation algorithm based on content-based feature representation, named Content-based Superpixel Segmentation (CSS) algorithm. Superpixels are generated in terms of a new distance metric using color, spatial, and gradient feature information. It is developed to balance the compactness and the boundary adherence of resulted superpixels. Then, we calculate the entropy of each superpixel for separating some superpixels with significant characteristics. Next, for each selected superpixel, its multi-features descriptor is generated by extracting and fusing local features of the selected superpixel itself. Finally, we compare the matching features of candidate superpixels and their own neighborhoods to estimate the correspondence between two images. We evaluated superpixel matching and image stitching on complex and deformable surfaces using our superpixel region descriptors, and the results show that new method is effective in matching accuracy and execution speed.

This paper describes graph-based Wave Function Collapse algorithm for procedural content generation. The goal of this system is to enable a game designer to procedurally create key content elements in the game level through simple association rule input. To do this, we propose a graph-based data structure that can be easily integrated with a navigation mesh data structure in a three-dimensional world. With our system, if the user inputs the minimum association rule, it is possible to effectively perform procedural content generation in the three-dimensional world. The experimental results show that the Wave Function Collapse algorithm, which is a texture synthesis algorithm, can be extended to non-grid shape content with high controllability and scalability.

An increasing number of IoT devices are being introduced to the market in many industries, and the number of devices is expected to exceed billions in the near future. With this trend, many researchers have proposed new architectures to manage IoT devices, but the proposed architecture requires a huge memory footprint and computation overheads to look-up billions of devices. This paper proposes a hybrid hashing architecture called H- TLA to solve the problem from an architectural point of view, instead of modifying a hashing algorithm or designing a new one. We implemented a prototype system that shows about a 30% increase in performance while conserving uniformity. Therefore, we show an efficient architecture-level approach for addressing billions of devices.

System logs record system states and significant events at various critical points to help debug performance issues and failures. Therefore, the rapid and accurate detection of the system log is crucial to the security and stability of the system. In this paper, proposed is a novel attention-based neural network model, which would learn log patterns from normal execution. Concretely, our model adopts a GRU module with attention mechanism to extract the comprehensive and intricate correlations and patterns embedded in a sequence of log entries. Experimental results demonstrate that our proposed approach is effective and achieve better performance than conventional methods.

We propose a deep learning-based model for classifying pathological voices using a convolutional neural network and a feedforward neural network. The model uses combinations of heterogeneous parameters, including mel-frequency cepstral coefficients, linear predictive cepstral coefficients and higher-order statistics. We validate the accuracy of this model using the Massachusetts Eye and Ear Infirmary (MEEI) voice disorder database and the Saarbruecken Voice Database (SVD). Our model achieved an accuracy of 99.3% for MEEI and 75.18% for SVD. This model achieved an accuracy that is 7.18% higher than that of competitive models in previous studies.

We combine the siamese network and the recurrent regression network, proposing a two-stage tracking framework termed as SiamReg. Our method solves the problem that the classic siamese network can not judge the target size precisely and simplifies the procedures of regression in the training and testing process. We perform experiments on three challenging tracking datasets: VOT2016, OTB100, and VOT2018. The results indicate that, after offline trained, SiamReg can obtain a higher expected average overlap measure.