Search results for: Tomokazu Nagata

Authors: Jawid Ahmad Baktash, Mursal Dawodi, Tomokazu Nagata

Abstract:

With the rapid growth of Cloud Computing, Formal Methods became a good choice for the refinement of message specification and verification for Dynamic Routing in Cloud Computing. Cloud-based Dynamic Routing is becoming increasingly popular. We propose feedback in Formal Methods for Dynamic Routing and Cloud Computing; the model and topologies show how to send messages from index zero to all others formally. The responsibility of proper verification becomes crucial with Dynamic Routing in the cloud. Formal Methods can play an essential role in the routing and development of Networks, and the testing of distributed systems. Event-B is a formal technique that consists of describing the problem rigorously and introduces solutions or details in the refinement steps. Event-B is a variant of B, designed for developing distributed systems and message passing of the dynamic routing. In Event-B and formal methods, the events consist of guarded actions occurring spontaneously rather than being invoked.

Keywords: cloud, dynamic routing, formal method, Pro-B, event-B

Procedia PDF Downloads 422

Authors: Jawid Ahmad Baktash, Tadashi Shiroma, Tomokazu Nagata, Yuji Taniguchi, Morikazu Nakamura

Abstract:

The goal of this paper is to explore the use of formal methods for Dynamic Routing, The purpose of network communication with dynamic routing is sending a massage from one node to others by using pacific protocols. In dynamic routing connections are possible based on protocols of Distance vector (Routing Information Protocol, Border Gateway protocol), Link State (Open Shortest Path First, Intermediate system Intermediate System), Hybrid (Enhanced Interior Gateway Routing Protocol). The responsibility for proper verification becomes crucial with Dynamic Routing. Formal methods can play an essential role in the Routing, development of Networks and testing of distributed systems. Event-B is a formal technique consists of describing rigorously the problem; introduce solutions or details in the refinement steps to obtain more concrete specification, and verifying that proposed solutions are correct. The system is modeled in terms of an abstract state space using variables with set theoretic types and the events that modify state variables. Event-B is a variant of B, was designed for developing distributed systems. In Event-B, the events consist of guarded actions occurring spontaneously rather than being invoked. The invariant state properties must be satisfied by the variables and maintained by the activation of the events.

Keywords: dynamic rout RIP, formal method, event-B, pro-B

Procedia PDF Downloads 401

Authors: Tomokazu Nagata, Jawid Ahmad Baktash

Abstract:

The goal of this paper is to explore the use of formal methods for Electronic Identity Card System. Nowadays, one of the core research directions in a constantly growing distributed environment is the improvement of the communication process. The responsibility for proper verification becomes crucial. Formal methods can play an essential role in the development and testing of systems. The thesis presents two different methodologies for assessing correctness. Our first approach employs abstract interpretation techniques for creating a trace based model for Electronic Identity Card System. The model was used for building a semi decidable procedure for verifying the system model. We also developed the code for the eID System and can cover three parts login to system sending of Acknowledgment from user side, receiving of all information from server side and log out from system. The new concepts of impasse and spawned sessions that we introduced led our research to original statements about the intruder’s knowledge and eID system coding with respect to secrecy. Furthermore, we demonstrated that there is a bound on the number of sessions needed for the analysis of System.Electronic identity (eID) cards promise to supply a universal, nation-wide mechanism for user authentication. Most European countries have started to deploy eID for government and private sector applications. Are government-issued electronic ID cards the proper way to authenticate users of online services? We use the eID project as a showcase to discuss eID from an application perspective. The new eID card has interesting design features, it is contact-less, it aims to protect people’s privacy to the extent possible, and it supports cryptographically strong mutual authentication between users and services. Privacy features include support for pseudonymous authentication and per service controlled access to individual data items. The article discusses key concepts, the eID infrastructure, observed and expected problems, and open questions. The core technology seems ready for prime time and government projects deploy it to the masses. But application issues may hamper eID adoption for online applications.

Keywords: eID, event-B, Pro-B, formal method, message passing

Procedia PDF Downloads 234

Authors: Tomokazu Shirai, Akihiko Kondo

Abstract:

Technologies of metabolic engineering or synthetic biology are essential for effective microbial bioproduction. It is especially important to develop an in silico tool for designing a metabolic pathway producing an unnatural and valuable chemical such as fossil materials of fuel or plastics. We here demonstrated two in silico tools for designing novel metabolic pathways: BioProV and HyMeP. Furthermore, we succeeded in creating an artificial metabolic pathway by enzyme engineering.

Keywords: bioinformatics, metabolic engineering, synthetic biology, genome scale model

Procedia PDF Downloads 339

Authors: Yuji Kageyama, Shin Nagata, Tatsuya Takino, Izuru Nomura, Hiroyuki Kamata

Abstract:

In previous study, technique to estimate a self-location by using a lunar image is proposed. We consider the improvement of the conventional method in consideration of FPGA implementation in this paper. Specifically, we introduce Artificial Bee Colony algorithm for reduction of search time. In addition, we use fixed point arithmetic to enable high-speed operation on FPGA.

Keywords: SLIM, Artificial Bee Colony Algorithm, location estimate, evolutional triangle similarity

Procedia PDF Downloads 517

Authors: Izuru Nomura, Tatsuya Takino, Yuji Kageyama, Shin Nagata, Hiroyuki Kamata

Abstract:

We propose a method of crater detection from the image of the lunar surface captured by the small space probe. We use the principal component analysis (PCA) to detect craters. Nevertheless, considering　severe environment of the space, it is impossible to use generic computer in practice. Accordingly, we have to implement the method in FPGA. This paper compares FPGA and generic computer by the processing time of a method of crater detection using principal component analysis.

Keywords: crater, PCA, eigenvector, strength value, FPGA, processing time

Procedia PDF Downloads 553

Authors: Tatsuya Takino, Izuru Nomura, Yuji Kageyama, Shin Nagata, Hiroyuki Kamata

Abstract:

We propose a method of detecting the craters from the image of the lunar surface. This proposal assumes that it is applied to SLIM (Smart Lander for Investigating Moon) working group aiming at the pinpoint landing on the lunar surface and investigating scientific research. It is difficult to equip and use high-performance computers for the small space probe. So, it is necessary to use a small computer with an exclusive hardware such as FPGA. We have studied the crater detection using principal component analysis (PCA), In this paper, We implement detection algorithm into the FPGA, and the detection is performed on the data that was captured from the CMOS camera.

Keywords: crater detection, PCA, FPGA, image processing

Procedia PDF Downloads 548

Authors: Tatsuya Kato, Masanobu Nagata, Hidetoshi Nakashima, Kazunori Matsuo

Abstract:

Localization of mobile robots are important tasks for developing autonomous mobile robots. This paper proposes a method to estimate positions of a mobile robot using an omnidirectional camera on the robot. Landmarks for points of references are set up on a field where the robot works. The omnidirectional camera which can obtain 360 [deg] around images takes photographs of these landmarks. The positions of the robots are estimated from directions of these landmarks that are extracted from the images by image processing. This method can obtain the robot positions without accumulative position errors. Accuracy of the estimated robot positions by the proposed method are evaluated through some experiments. The results show that it can obtain the positions with small standard deviations. Therefore the method has possibilities of more accurate localization by tuning of appropriate offset parameters.

Keywords: mobile robots, localization, omnidirectional camera, estimating positions

Procedia PDF Downloads 440

Authors: Syhalath Xaphakdy, Toshio Nagata, Saykham Phommathat, Pavy Souwannavong, Vilayvanh Srithilat, Phoxay Sengdala, Bounaom Phetarnousone, Boualay Siharath, Xaya Chemcheng

Abstract:

The National University of Laos (NUOL) invited a group of volunteers from the Japan International Cooperation Agency (JICA) to revise the physics experiments to utilize the materials that were already available to students. The intension was to review and revise the materials regularly utilized in physics class. The project had access to limited materials and a small budget for the class in the unit; however, by developing experimental textbooks related to mechanics, electricity, and wave and vibration, the group found a way to apply them in the classroom and enhance the students teaching activities. The aim was to introduce a way to incorporate the materials and practices in the classroom to enhance the students learning and teaching skills, particularly when they graduate and begin working as high school teachers.

Keywords: NUOL, JICA, physics experiment materials, small budget, mechanics, electricity

Procedia PDF Downloads 235

Authors: Shota Nagata, Kazuya Okubo, Toru Fujii

Abstract:

The purpose of this study is to investigate the proper condition in extracting carbon fibers as the reinforcement of composite molded by injection method. Recycled carbon fibers were extracted from wasted CFRP by pyrolyzing epoxy matrix of CFRP under air atmosphere at different temperature conditions 400, 600 and 800°C in this study. Recycled carbon fiber reinforced polypropylene (RCF/PP) pellets were prepared using twin screw extruder. The RCF/PP specimens were molded into dumbbell shaped specimens using injection molding machine. The tensile strength of recycled carbon fiber was decreased with rising pyrolysis temperature from 400 to 800°C. However, superior mechanical properties of tensile strength, tensile modulus and fracture strain of RCF/PP specimen were obtained when the extracting temperature was 600°C. Almost fibers in RCF/PP specimens were aligned in the mold filling direction in this study when the extracting temperature was 600°C. To discuss the results, the failure mechanisms of RCF/PP specimens was shown schematically. Finally, it was concluded that the temperature condition at 600°C should be selected in extracting carbon fibers as the reinforcement of RCF/PP composite molded by injection method.

Keywords: CFRP, recycled carbon fiber, injection molding, mechanical properties, fiber orientation, failure mechanism

Procedia PDF Downloads 445

Authors: Agada N. Ihuoma, Nagata Yasunori

Abstract:

Artificial intelligence (AI) techniques play a crucial role in predicting the expected energy outcome and its performance, analysis, modeling, and control of renewable energy. Renewable energy is becoming more popular for economic and environmental reasons. In the face of global energy consumption and increased depletion of most fossil fuels, the world is faced with the challenges of meeting the ever-increasing energy demands. Therefore, incorporating artificial intelligence to predict solar radiation outcomes from the intermittent sunlight is crucial to enable a balance between supply and demand of energy on loads, predict the performance and outcome of solar energy, enhance production planning and energy management, and ensure proper sizing of parameters when generating clean energy. However, one of the major problems of forecasting is the algorithms used to control, model, and predict performances of the energy systems, which are complicated and involves large computer power, differential equations, and time series. Also, having unreliable data (poor quality) for solar radiation over a geographical location as well as insufficient long series can be a bottleneck to actualization. To overcome these problems, this study employs the anaconda Navigator (Jupyter Notebook) for machine learning which can combine larger amounts of data with fast, iterative processing and intelligent algorithms allowing the software to learn automatically from patterns or features to predict the performance and outcome of Solar Energy which in turns enables the balance of supply and demand on loads as well as enhance production planning and energy management.

Keywords: artificial Intelligence, backward elimination, linear regression, solar energy

Procedia PDF Downloads 155

Authors: T. Nagata, S. Xaphakdy, P. Souvannavong, P. Chanthamaly, K. Sithavong, C. H. Lee, S. Phommathat, V. Srithilat, P. Sengdala, B. Phetarnousone, B. Siharath, X. Chemcheng, T. Yamaguchi, A. Suenaga, S. Kashima

Abstract:

National University of Laos (NUOL) requested Japan International Cooperation Agency (JICA) volunteers to begin a physics experiments class using multi media. However, there are issues. NUOL had no physics experiment class, no space for physics experiments, experiment materials were not used for many years and were scattered in various places, and there is no projector and laptop computer in the unit. This raised the question: How do authors begin the physics experiments class using multimedia? To solve this problem, the JICA took some steps, took stock of what was available and reviewed the syllabus. The JICA then revised the experiment materials to assess what was available and then developed textbooks for experiments using them; however, the question remained, what about the multimedia component of the course? Next, the JICA reviewed Physics teacher Pavy Souvannavong’s YouTube channel, where he and his students upload video reports of their physics classes at NUOL using their smartphones. While they use multi-media, almost all the videos recorded were of class presentations. To improve the multimedia style, authors edited the videos in the style of another YouTube channel, “Science for Lao,” which is a science education group made up of Japan Overseas Cooperation Volunteers (JOCV) in Laos. They created the channel to enhance science education in Laos, and hold regular monthly meetings in the capital, Vientiane, and at teacher training colleges in the country. They edit the video clips in three parts, which are the materials and procedures part including pictures, practice footage of the experiment part, and then the result and conclusion part. Then students perform experiments and prepare for presentation by following the videos. The revised experiment presentation reports use PowerPoint presentations, material pictures and experiment video clips. As for providing textbooks and submitting reports, the students use the e-Learning system of “Moodle” of the Information Technology Center in Dongdok campus of NUOL. The Korean International Cooperation Agency (KOICA) donated those facilities. The authors have passed the process of the revised materials, developed textbooks, the PowerPoint slides presented by students, downloaded textbooks and uploaded reports, to begin the physics experiments class using multimedia. This is the practice research report for beginning a physics experiments class using multimedia in the physics unit at the Department of Natural Science, Faculty of Education, at the NUOL.

Keywords: NUOL, JICA, KOICA, physics experiment materials, smartphone, Moodle, IT center, Science for Lao

Procedia PDF Downloads 351

Authors: Sylvana A. Vega, Cesar E. Huilinir, Carlos J. Gonzalez

Abstract:

Co-digestion in anaerobic biodigesters is a technology improving hydrolysis by increasing methane generation. In the present study, the dimensional computational fluid dynamics (CFD) is numerically analyzed using Ansys Fluent software for agitation in a full-scale Continuous Stirred Tank Reactor (CSTR) biodigester during the co-digestion process. For this, a rheological study of the substrate is carried out, establishing rotation speeds of the stirrers depending on the microbial activity and energy ranges. The substrate is organic waste from industrial sources of sanitary water, butcher, fishmonger, and dairy. Once the rheological behavior curves have been obtained, it is obtained that it is a non-Newtonian fluid of the pseudoplastic type, with a solids rate of 12%. In the simulation, the rheological results of the fluid are considered, and the full-scale CSTR biodigester is modeled. It was coupling the second-order continuity differential equations, the three-dimensional Navier Stokes, the power-law model for non-Newtonian fluids, and three turbulence models: k-ε RNG, k-ε Realizable, and RMS (Reynolds Stress Model), for a 45° tilt vane impeller. It is simulated for three minutes since it is desired to study an intermittent mixture with a saving benefit of energy consumed. The results show that the absolute errors of the power number associated with the k-ε RNG, k-ε Realizable, and RMS models were 7.62%, 1.85%, and 5.05%, respectively, the numbers of power obtained from the analytical-experimental equation of Nagata. The results of the generalized Reynolds number show that the fluid dynamics have a transition-turbulent flow regime. Concerning the Froude number, the result indicates there is no need to implement baffles in the biodigester design, and the power number provides a steady trend close to 1.5. It is observed that the levels of design speeds within the biodigester are approximately 0.1 m/s, which are speeds suitable for the microbial community, where they can coexist and feed on the substrate in co-digestion. It is concluded that the model that more accurately predicts the behavior of fluid dynamics within the reactor is the k-ε Realizable model. The flow paths obtained are consistent with what is stated in the referenced literature, where the 45° inclination PBT impeller is the right type of agitator to keep particles in suspension and, in turn, increase the dispersion of gas in the liquid phase. If a 24/7 complete mix is considered under stirred agitation, with a plant factor of 80%, 51,840 kWh/year are estimated. On the contrary, if intermittent agitations of 3 min every 15 min are used under the same design conditions, reduce almost 80% of energy costs. It is a feasible solution to predict the energy expenditure of an anaerobic biodigester CSTR. It is recommended to use high mixing intensities, at the beginning and end of the joint phase acetogenesis/methanogenesis. This high intensity of mixing, in the beginning, produces the activation of the bacteria, and once reaching the end of the Hydraulic Retention Time period, it produces another increase in the mixing agitations, favoring the final dispersion of the biogas that may be trapped in the biodigester bottom.

Keywords: anaerobic co-digestion, computational fluid dynamics, CFD, net power, organic waste

Procedia PDF Downloads 113