Verification of MILS Partition Scheduling Module Using Layered Methods

MILS partition scheduling module ensures isolation of data between different domains completely by enforcing secure strategies. Although small in size, it involves complicated data structures and algorithms that make monolithic verification of the scheduling module difficult using traditional verification logic (e.g., separation logic). In this paper, we simplify the verification task by dividing data representation and data operation into different layers and then to link them together by composing a series of abstraction layers. The layered method also supports function calls from higher implementation layers into lower abstraction layers, allowing us to ignore implementation details in the lower implementation layers. Using this methodology, we have verified a realistic MILS partition scheduling module that can schedule operating systems (Ubuntu 14.04, VxWorks 6.8 and RTEMS 11.0) located in different domains. The entire verification has been mechanized in the Coq Proof Assistant.

Propose System Architecture Technology Hub for the New Normal in Sibuyan Island, Romblon (PSATH)

The new era of technologies around the globe continues transforming the process of innovation particularly in the province of Romblon where the community is being active and updated about the trends of technology, however, due to the limited bandwidth signal of internet connection, their telecommunications are affected especially during this new normal where the Business Transactions, Learning Management System, and other Essential Services are done through online. The purpose of this study is to propose an IT business project especially a technology hub that will cater to and satisfy the needs of the community on the Island. The impact of this study is simply for connecting and moving people into the fastest and easiest way of communication using social media and other online platforms. The proposed Technology hub is composed of four areas, the Internet Café, Printing Press, Research Learning Area, and Photo Studio. This is very beneficial to the people in the community especially to the students that needs IT services. This study aims to help the people, the Local Government Unit, and the University to make their goals put into reality. This study will truly change and innovate the lives of the people even for the progress of the economy, culture, and lifestyle of the place. This study is also recommended for the implementation of Techno hub within the island since this could give an opportunity to give new jobs, especially for the IT professions. This is very responsive to the needs of the society in terms of socialization, communication, and education.

Convergence Analysis of Particle Swarm Optimization via Illustration Styles

Particle swarm optimization (PSO) is the most important and popular algorithm to solving the engineering optimization problem due to its simple updating formulas and excellent searching capacity. This algorithm is one of evolutionary computations and is also a population-based algorithm. Traditionally, to demonstrate the convergence analysis of the PSO algorithm or its related variations, simulation results in a numerical presentation are often given. This way may be unclear or unsuitable for some particular cases. Hence, this paper will adopt the illustration styles instead of numeric simulation results to more clearly clarify the convergence behavior of the algorithm. In addition, it is well known that three parameters used in the algorithm, i.e., the inertia weight w, position constants c1 and c2, sufficiently dominate the whole searching performance. The influence of these parameter settings on the algorithm convergence will be considered and examined via a simple two-dimensional function optimization problem. All simulation results are displayed using a series of illustrations with respect to various iteration numbers. Finally, some simple rules on how to suitably assign these parameters are also suggested

A Guide on Using Xilinx System Generator to Design and Implement Real-Time Audio Effects on FPGA

The enormous progress in communication technology has led to a tremendous need to provide an ideal environment for the transmission, storing, and processing of digital multimedia content, where the audio signal takes the lion's share of it. Audio processing covers many diverse fields, its main aim is presenting sound to human listeners. Recently, digital audio processing became an active research area, it covers everything from theory to practice in relation to transmission, compression, filtering, and adding special effects to an audio signal. The aim of this work is to present the real-time implementation steps of some audio effects namely, the echo and Flanger effects on Field Programmable Gate Array (FPGA). Today, FPGAs are the best choice in data processing because they provide more flexibility, performance, and huge processing capabilities with great power efficiency. Designs are achieved using the XSG tool (Xilinx System Generator), which makes complex designs easier without prior knowledge of hardware description languages. The paper is presented as a guide with deep technical details about designing and real-time implementation steps. We decided to transfer some experience to designers who want to rapidly prototype their ideas using tools such as XSG. All the designs have been simulated and verified under Simulink/Matlab environment, then exported to Xilinx ISE (Integrated Synthesis Environment) tool for the rest of the implementation steps. The paper also gives an idea of interfacing the FPGA with the LM4550 AC’97 codec using VHDL coding. The ATLYS development board based on Xilinx Spartan-6 LX45 FPGA is used for the real-time implementation.

Fictitious Crisis Scenario Development Related to a Bank Following a Breakdown in the Communication Network to Show Critical Infrastructure Digitization

The notion of critical infrastructure represents for states a vital asset for the functioning of society and the economy. These critical infrastructures cover many areas such as transportation, electricity, hospitals, and recently telecommunications which are taking more and more place in our economies due to the digitalization of our society. Business Continuity Plans (BCP) are often an obligation here to ensure the fastest possible recovery of these critical infrastructures in the event of a crisis. However, the scenarios that allow simulation exercises to be carried out remain very "logistically" oriented, while critical infrastructures linked in general to the digitization of the economy are poorly prepared for a major critical incident. To compensate for these weaknesses in the development of crisis scenarios linked to digitalization, we take the case of critical digital banking infrastructures and use counterfactual thinking to develop a crisis scenario that takes better account of the entire dematerialization dimension inherent in them.

Temporal Feature Aggregation for Text Classification Based on Ensembled Deep-Learning Models

In this paper, we focus on the text classification task, which is a most import task in the area of Natural Language Processing (NLP). We propose an innovative convolutional neural network (CNN) model to perform temporal feature aggregation (TFA) effectively, which has a highly representative capacity to extract sequential features from vectorized numerical embeddings. First, we feed embedded vectors into a bi-directional LSTM (Bi-LSTM) model to capture the contextual information of each word. Afterwards, we propose to use the state-of-the-art deep-learning models as key components of the architecture, i.e., the Xception model and the WaveNet model, to extract temporal features from deep convolutional layers concurrently. To facilitate an effective feature fusion, we concatenate the outputs of two component models before forwarding to a drop-out layer to alleviate over-fitting and subsequently a fully-connected dense layer to perform the final classification of input texts. Experiments demonstrate that the proposed method achieves performance comparable to the state-of-the-art models while at a significantly lower computational complexity. Our approach obtains the cross-validation score of 95.83% for the Quora Insincere Question Classification (QIQC) dataset, and the cross-validation score of 83.10% for the Spooky Author Identification (SAI) dataset, respectively, which are among the best published results. The proposed method can be readily generalized to signal processing tasks, e.g., environmental sound classification (ESC) and machine fault analysis (MFA).

Smart Home Powered by Social Network for Citizen Security

Nowadays, the Internet of Things is used to transfer information from human to human and from human to machine. In this paper, we propose the use of IoT platforms to link those homes that are equipped with IoT capabilities, in order to increase security and prevent from a crime to a fire, and even monitor health status of a person. Using a microcontroller, it is possible to send information to a cloud server capable of sharing this information with other households connected to the platform, as well as allowing linking this data to one of the most used social networks in the world: Facebook. Linking smart homes with social network, allows to consult the status of sensors and IoT devices empowering citizen security against crime, violence and events that could put the integrity of people at risk both in their property and their health. The study is carried out for a particular region of Latin America, given its high rates of violence against citizens that have occurred in recent years.

IoT Platform with Distributed Brokerson MQTT

Various wide-area Internet of Things services have been deployed. In most of these IoT services, a significant number of tiny data blocks are transferred across wide-area networks. Therefore, the transfer mechanisms should be simplified. One promising candidate for use as a transfer mechanism is MQ Telemetry Transport (MQTT). In this paper, an architecture for a distributed MQTT broker, referred to as a virtual ring approach, is proposed. This architecture complies with the IoT Data Exchange Platform, as discussed in ISO/IEC JTC 1/SC 41. The operations of this distributed broker architecture using a virtual ring network for real-time communication is also described, along with the superiority of the architecture based on a performance analysis using queuing models

Quantized Turbo Equalization for Non-binary LDPC Coded Partial-Response Channels

In this paper, we consider iterative detection and decoding (i.e., turbo equalization) for nonbinary low-density parity-check (LDPC) coded partial-response channels, where a quantizer is present to discretize the continuous received signal. We propose a turbo equalizer that uses the pre-computed quantized channel transition probabilities in the symbol-level BCJR channel detection algorithm, which significantly reduces the computational complexity by avoiding real-time floating-point multiplications. The proposed approach is further extended to nonbinary LDPC coded bit-patterned media recording (BPMR) channels. Simulation results show that with a small number of quantization bits, the proposed receiver approaches closely the performance of the conventional turbo equalizer operating on unquantized signals.