Search results for: Physical verification
1606 Computer Aided Assembly Attributes Retrieval Methods for Automated Assembly Sequence Generation
Authors: M. V. A. Raju Bahubalendruni, Bibhuti Bhusan Biswal, B. B. V. L. Deepak
Abstract:
Achieving an appropriate assembly sequence needs deep verification for its physical feasibility. For this purpose, industrial engineers use several assembly predicates; namely, liaison, geometric feasibility, stability and mechanical feasibility. However, testing an assembly sequence for these predicates requires huge assembly information. Extracting such assembly information from an assembled product is a time consuming and highly skillful task with complex reasoning methods. In this paper, computer aided methods are proposed to extract all the necessary assembly information from computer aided design (CAD) environment in order to perform the assembly sequence planning efficiently. These methods use preliminary capabilities of three-dimensional solid modelling and assembly modelling methods used in CAD software considering equilibrium laws of physical bodies.
Keywords: Assembly automation, assembly attributes, assembly sequence generation, computer aided design.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 12651605 Computer Proven Correctness of the Rabin Public-Key Scheme
Authors: Johannes Buchmann, Markus Kaiser
Abstract:
We decribe a formal specification and verification of the Rabin public-key scheme in the formal proof system Is-abelle/HOL. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. The analysis presented uses a given database to prove formal properties of our implemented functions with computer support. Thema in task in designing a practical formalization of correctness as well as security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as eficient formal proofs. This yields the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Consequently, we get reliable proofs with a minimal error rate augmenting the used database. This provides a formal basis for more computer proof constructions in this area.Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 15461604 Wind Farm Power Performance Verification Using Non-Parametric Statistical Inference
Authors: M. Celeska, K. Najdenkoski, V. Dimchev, V. Stoilkov
Abstract:
Accurate determination of wind turbine performance is necessary for economic operation of a wind farm. At present, the procedure to carry out the power performance verification of wind turbines is based on a standard of the International Electrotechnical Commission (IEC). In this paper, nonparametric statistical inference is applied to designing a simple, inexpensive method of verifying the power performance of a wind turbine. A statistical test is explained, examined, and the adequacy is tested over real data. The methods use the information that is collected by the SCADA system (Supervisory Control and Data Acquisition) from the sensors embedded in the wind turbines in order to carry out the power performance verification of a wind farm. The study has used data on the monthly output of wind farm in the Republic of Macedonia, and the time measuring interval was from January 1, 2016, to December 31, 2016. At the end, it is concluded whether the power performance of a wind turbine differed significantly from what would be expected. The results of the implementation of the proposed methods showed that the power performance of the specific wind farm under assessment was acceptable.
Keywords: Canonical correlation analysis, power curve, power performance, wind energy.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 9661603 Automatic Checkpoint System Using Face and Card Information
Authors: Kriddikorn Kaewwongsri, Nikom Suvonvorn
Abstract:
In the deep south of Thailand, checkpoints for people verification are necessary for the security management of risk zones, such as official buildings in the conflict area. In this paper, we propose an automatic checkpoint system that verifies persons using information from ID cards and facial features. The methods for a person’s information abstraction and verification are introduced based on useful information such as ID number and name, extracted from official cards, and facial images from videos. The proposed system shows promising results and has a real impact on the local society.
Keywords: Face comparison, card recognition, OCR, checkpoint system, authentication.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 17351602 Student Records Management System Using Smart Cards and Biometric Technology for Educational Institutions
Authors: Patrick O. Bobbie, Prince S. Attrams
Abstract:
In recent times, the rapid change in new technologies has spurred up the way and manner records are handled in educational institutions. Also, there is a need for reliable access and ease-of use to these records, resulting in increased productivity in organizations. In academic institutions, such benefits help in quality assessments, institutional performance, and assessments of teaching and evaluation methods. Students in educational institutions benefit the most when advanced technologies are deployed in accessing records. This research paper discusses the use of biometric technologies coupled with smartcard technologies to provide a unique way of identifying students and matching their data to financial records to grant them access to restricted areas such as examination halls. The system developed in this paper, has an identity verification component as part of its main functionalities. A systematic software development cycle of analysis, design, coding, testing and support was used. The system provides a secured way of verifying student’s identity and real time verification of financial records. An advanced prototype version of the system has been developed for testing purposes.Keywords: Biometrics, fingerprints, identity-verification, smartcards.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 20031601 Forensic Speaker Verification in Noisy Environmental by Enhancing the Speech Signal Using ICA Approach
Authors: Ahmed Kamil Hasan Al-Ali, Bouchra Senadji, Ganesh Naik
Abstract:
We propose a system to real environmental noise and channel mismatch for forensic speaker verification systems. This method is based on suppressing various types of real environmental noise by using independent component analysis (ICA) algorithm. The enhanced speech signal is applied to mel frequency cepstral coefficients (MFCC) or MFCC feature warping to extract the essential characteristics of the speech signal. Channel effects are reduced using an intermediate vector (i-vector) and probabilistic linear discriminant analysis (PLDA) approach for classification. The proposed algorithm is evaluated by using an Australian forensic voice comparison database, combined with car, street and home noises from QUT-NOISE at a signal to noise ratio (SNR) ranging from -10 dB to 10 dB. Experimental results indicate that the MFCC feature warping-ICA achieves a reduction in equal error rate about (48.22%, 44.66%, and 50.07%) over using MFCC feature warping when the test speech signals are corrupted with random sessions of street, car, and home noises at -10 dB SNR.Keywords: Noisy forensic speaker verification, ICA algorithm, MFCC, MFCC feature warping.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 9261600 Automatic Translation of Ada-ECATNet Using Rewriting Logic
Authors: N. Boudiaf
Abstract:
One major difficulty that faces developers of concurrent and distributed software is analysis for concurrency based faults like deadlocks. Petri nets are used extensively in the verification of correctness of concurrent programs. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high-level Petri nets. ECATNets have 'sound' and 'complete' semantics because of their integration in rewriting logic and its programming language Maude. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems We proposed previously a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet) and we showed that ECATNets formalism provides a more compact translation for Ada programs compared to the other approaches based on simple Petri nets or Colored Petri nets. We showed also previously how the ECATNet formalism offers to Ada many validation and verification tools like simulation, Model Checking, accessibility analysis and static analysis. In this paper, we describe the implementation of our translation of the Ada programs into ECATNets.Keywords: Ada tasking, Analysis, Automatic Translation, ECATNets, Maude, Rewriting Logic.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 15481599 A Computer Proven Application of the Discrete Logarithm Problem
Authors: Sebastian Kusch, Markus Kaiser
Abstract:
In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.
Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 15141598 Authentication Analysis of the 802.11i Protocol
Authors: Zeeshan Furqan, Shahabuddin Muhammad, Ratan Guha
Abstract:
IEEE has designed 802.11i protocol to address the security issues in wireless local area networks. Formal analysis is important to ensure that the protocols work properly without having to resort to tedious testing and debugging which can only show the presence of errors, never their absence. In this paper, we present the formal verification of an abstract protocol model of 802.11i. We translate the 802.11i protocol into the Strand Space Model and then prove the authentication property of the resulting model using the Strand Space formalism. The intruder in our model is imbued with powerful capabilities and repercussions to possible attacks are evaluated. Our analysis proves that the authentication of 802.11i is not compromised in the presented model. We further demonstrate how changes in our model will yield a successful man-in-the-middle attack.Keywords: authentication, formal analysis, formal verification, security.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14721597 Influence of Atmospheric Physical Effects on Static Behavior of Building Plate Components Made of Fiber-Cement-Based Materials
Authors: Jindrich J. Melcher, Marcela Karmazínová
Abstract:
The paper presents the brief information on particular results of experimental study focused to the problems of behavior of structural plated components made of fiber-cement-based materials and used in building constructions, exposed to atmospheric physical effects given by the weather changes in the summer period. Weather changes represented namely by temperature and rain cause also the changes of the temperature and moisture of the investigated structural components. This can affect their static behavior that means stresses and deformations, which have been monitored as the main outputs of tests performed. Experimental verification is based on the simulation of the influence of temperature and rain using the defined procedure of warming and water sprinkling with respect to the corresponding weather conditions during summer period in the South Moravian region at the Czech Republic, for which the application of these structural components is mainly planned. Two types of components have been tested: (i) glass-fiber-concrete panels used for building façades and (ii) fiber-cement slabs used mainly for claddings, but also as a part of floor structures or lost shuttering, and so on.
Keywords: Atmospheric physical effect, building component, experiment, fiber-cement, glass-fiber-concrete, simulation, static behavior, test, warming, water sprinkling, weather.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 12021596 Physical and Thermo-Physical Properties of High Strength Concrete Containing Raw Rice Husk after High Temperature Effect
Authors: B. Akturk, N. Yuzer, N. Kabay
Abstract:
High temperature is one of the most detrimental effects that cause important changes in concrete’s mechanical, physical, and thermo-physical properties. As a result of these changes, especially high strength concrete (HSC), may exhibit damages such as cracks and spallings. To overcome this problem, incorporating polymer fibers such as polypropylene (PP) in concrete is a very well-known method. In this study, using RRH, as a sustainable material, instead of PP fiber in HSC to prevent spallings and improve physical and thermo-physical properties were investigated. Therefore, seven HSC mixtures with 0.25 water to binder ratio were prepared incorporating silica fume and blast furnace slag. PP and RRH were used at 0.2-0.5% and 0.5-3% by weight of cement, respectively. All specimens were subjected to high temperatures (20 (control), 300, 600 and 900˚C) with a heating rate of 2.5˚C/min and after cooling, residual physical and thermo-physical properties were determined.
Keywords: High temperature, high strength concrete, polypropylene fiber, raw rice husk, thermo-physical properties.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 21181595 Interactive Model Based On an Extended CPN
Authors: Shuzhen Yao, Fengjing Zhao, Jianwei He
Abstract:
The UML modeling of complex distributed systems often is a great challenge due to the large amount of parallel real-time operating components. In this paper the problems of verification of such systems are discussed. ECPN, an Extended Colored Petri Net is defined to formally describe state transitions of components and interactions among components. The relationship between sequence diagrams and Free Choice Petri Nets is investigated. Free Choice Petri Net theory helps verifying the liveness of sequence diagrams. By converting sequence diagrams to ECPNs and then comparing behaviors of sequence diagram ECPNs and statecharts, the consistency among models is analyzed. Finally, a verification process for an example model is demonstrated.
Keywords: Consistency, liveness, Petri Net, sequence diagram.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 15671594 Application of Augmented Reality for Simulation of Robotized Workcell Activity
Authors: J. Novak-Marcincin, J. Barna, M. Janak
Abstract:
Augmented Reality (AR) shows great promises for its usage as a tool for simulation and verification of design proposal of new technological systems. Main advantage of augmented reality application usage is possibility of creation and simulation of new technological unit before its realization. This may contribute to increasing of safety and ergonomics and decreasing of economical aspects of new proposed unit. Virtual model of proposed workcell could reveal hidden errors which elimination in later stage of new workcell creation should cause great difficulties. Paper describes process of such virtual model creation and possibilities of its simulation and verification by augmented reality tools.Keywords: Augmented reality, simulation, workcell design.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 16431593 Where has All the Physical Education Gone? Results of a Generalist Primary Schools Teachers- Survey on Teaching Physical Education
Authors: Vicki Cowley, Michael J. Hamlin, Michael Grimley
Abstract:
Concerns about low levels of children-s physical activity and motor skill development, prompted the Ministry of Education to trial a physical activity pilot project (PAPP) in 16 New Zealand primary schools. The project comprised professional development and training in physical education for lead teachers and introduced four physical activity coordinators to liaise with and increase physical activity opportunities in the pilot schools. A survey of generalist teachers (128 baseline, 155 post-intervention) from these schools looked at timetabled physical activity sessions and issues related to teaching physical education. The authors calculated means and standard deviations of data relating to timetabled PE sessions and used a one-way analysis of variance to determine significant differences. Results indicated time devoted to physical activity related subjects significantly increased over the course of the intervention. Teacher-s reported improved confidence and competence, which resulted in an improvement in quality physical education delivered more often.
Keywords: children, physical education, primary school, teaching
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 16971592 Formal Modeling and Verification of Software Models
Authors: Siamak Rasulzadeh
Abstract:
Graph transformation has recently become more and more popular as a general visual modeling language to formally state the dynamic semantics of the designed models. Especially, it is a very natural formalism for languages which basically are graph (e.g. UML). Using this technique, we present a highly understandable yet precise approach to formally model and analyze the behavioral semantics of UML 2.0 Activity diagrams. In our proposal, AGG is used to design Activities, then using our previous approach to model checking graph transformation systems, designers can verify and analyze designed Activity diagrams by checking the interesting properties as combination of graph rules and LTL (Linear Temporal Logic) formulas on the Activities.Keywords: UML 2.0 Activity, Verification, Model Checking, Graph Transformation, Dynamic Semantics.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14011591 Finite Element and Subspace Identification Approaches to Model Development of a Smart Acoustic Box with Experimental Verification
Authors: Tamara Nestorović, Jean Lefèvre, Stefan Ringwelski, Ulrich Gabbert
Abstract:
Two approaches for model development of a smart acoustic box are suggested in this paper: the finite element (FE) approach and the subspace identification. Both approaches result in a state-space model, which can be used for obtaining the frequency responses and for the controller design. In order to validate the developed FE model and to perform the subspace identification, an experimental set-up with the acoustic box and dSPACE system was used. Experimentally obtained frequency responses show good agreement with the frequency responses obtained from the FE model and from the identified model.
Keywords: Acoustic box, experimental verification, finite element model, subspace identification.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 15171590 Efficient Aggregate Signature Algorithm and Its Application in MANET
Authors: Daxing Wang, Jikai Teng
Abstract:
An aggregate signature scheme can aggregate n signatures on n distinct messages from n distinct signers into a single signature. Thus, n verification equations can be reduced to one. So the aggregate signature adapts to Mobile Ad hoc Network (MANET). In this paper, we propose an efficient ID-based aggregate signature scheme with constant pairing computations. Compared with the existing ID-based aggregate signature scheme, this scheme greatly improves the efficiency of signature communication and verification. In addition, in this work, we apply our ID-based aggregate sig- nature to authenticated routing protocol to present a secure routing scheme. Our scheme not only provides sound authentication and a secure routing protocol in ad hoc networks, but also meets the nature of MANET.
Keywords: Identity-based cryptography, Aggregate signature, Bilinear pairings, Authenticated routing scheme.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 20601589 A P-SPACE Algorithm for Groebner Bases Computation in Boolean Rings
Authors: Quoc-Nam Tran
Abstract:
The theory of Groebner Bases, which has recently been honored with the ACM Paris Kanellakis Theory and Practice Award, has become a crucial building block to computer algebra, and is widely used in science, engineering, and computer science. It is wellknown that Groebner bases computation is EXP-SPACE in a general setting. In this paper, we give an algorithm to show that Groebner bases computation is P-SPACE in Boolean rings. We also show that with this discovery, the Groebner bases method can theoretically be as efficient as other methods for automated verification of hardware and software. Additionally, many useful and interesting properties of Groebner bases including the ability to efficiently convert the bases for different orders of variables making Groebner bases a promising method in automated verification.Keywords: Algorithm, Complexity, Groebner basis, Applications of Computer Science.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 17771588 Design and Application of NFC-Based Identity and Access Management in Cloud Services
Authors: Shin-Jer Yang, Kai-Tai Yang
Abstract:
In response to a changing world and the fast growth of the Internet, more and more enterprises are replacing web-based services with cloud-based ones. Multi-tenancy technology is becoming more important especially with Software as a Service (SaaS). This in turn leads to a greater focus on the application of Identity and Access Management (IAM). Conventional Near-Field Communication (NFC) based verification relies on a computer browser and a card reader to access an NFC tag. This type of verification does not support mobile device login and user-based access management functions. This study designs an NFC-based third-party cloud identity and access management scheme (NFC-IAM) addressing this shortcoming. Data from simulation tests analyzed with Key Performance Indicators (KPIs) suggest that the NFC-IAM not only takes less time in identity identification but also cuts time by 80% in terms of two-factor authentication and improves verification accuracy to 99.9% or better. In functional performance analyses, NFC-IAM performed better in salability and portability. The NFC-IAM App (Application Software) and back-end system to be developed and deployed in mobile device are to support IAM features and also offers users a more user-friendly experience and stronger security protection. In the future, our NFC-IAM can be employed to different environments including identification for mobile payment systems, permission management for remote equipment monitoring, among other applications.
Keywords: Cloud service, multi-tenancy, NFC, IAM, mobile device.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 10751587 Modelling of the Fire Pragmatism in the Area of Military Management and Its Experimental Verification
Authors: Ivana Mokrá
Abstract:
The article deals with modelling of the fire pragmatism in the area of military management and its experimental verification. Potential approaches are based on the synergy of mathematical and theoretical ideas, operational and tactical requirements and the military decision-making process. This issue has taken on importance in recent times, particularly with the increasing trend of digitized battlefield, the development of C4ISR systems and intention to streamline the command and control process at the lowest levels of command. From fundamental and philosophical point of view, these new approaches seek to significantly upgrade and enhance the decision-making process of the tactical commanders.
Keywords: Military management, decision-making process, strike modeling, experimental evaluation, pragmatism, tactical strike modeling
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14871586 Framework and Characterization of Physical Internet
Authors: Charifa Fergani, Adiba El Bouzekri El Idrissi, Suzanne Marcotte, Abdelowahed Hajjaji
Abstract:
Over the last years, a new paradigm known as Physical Internet has been developed, and studied in logistics management. The purpose of this global and open system is to deal with logistics grand challenge by setting up an efficient and sustainable Logistics Web. The purpose of this paper is to review scientific articles dedicated to Physical Internet topic, and to provide a clustering strategy enabling to classify the literature on the Physical Internet, to follow its evolution, as well as to criticize it. The classification is based on three factors: Logistics Web, organization, and resources. Several papers about Physical Internet have been classified and analyzed along the Logistics Web, resources and organization views at a strategic, tactical and operational level, respectively. A developed cluster analysis shows which topics of the Physical Internet that are the less covered actually. Future researches are outlined for these topics.Keywords: Logistics web, Physical Internet, PI characterization, taxonomy.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 7831585 Optimization of Element Type for FE Model and Verification of Analyses with Physical Tests
Authors: M. Tufekci, C. Guven
Abstract:
In Automotive Industry, sliding door systems that are also used as body closures are safety members. Extreme product tests are realized to prevent failures in design process, but these tests realized experimentally result in high costs. Finite element analysis is an effective tool used for design process. These analyses are used before production of prototype for validation of design according to customer requirement. In result of this, substantial amount of time and cost is saved. Finite element model is created for geometries that are designed in 3D CAD programs. Different element types as bar, shell and solid, can be used for creating mesh model. Cheaper model can be created by selection of element type, but combination of element type that was used in model, number and geometry of element and degrees of freedom affects the analysis result. Sliding door system is a good example which used these methods for this study. Structural analysis was realized for sliding door mechanism by using FE models. As well, physical tests that have same boundary conditions with FE models were realized. Comparison study for these element types, were done regarding test and analyses results then optimum combination was achieved.Keywords: Finite Element Analysis, Sliding Door Mechanism, Element Type, Structural Analysis.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 19191584 A Study of Quality Assurance and Unit Verification Methods in Safety Critical Environment
Authors: Miklos Taliga
Abstract:
In the present case study we examined the development and testing methods of systems that contain safety-critical elements in different industrial fields. Consequentially, we observed the classical object-oriented development and testing environment, as both medical technology and automobile industry approaches the development of safety critical elements that way. Subsequently, we examined model-based development. We introduce the quality parameters that define development and testing. While taking modern agile methodology (scrum) into consideration, we examined whether and to what extent the methodologies we found fit into this environment.
Keywords: Safety-critical elements, quality management, unit verification, model base testing, agile methods, scrum, metamodel, object-oriented programming, field specific modelling, sprint, user story, UML Standard.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 7831583 Global Security Using Human Face Understanding under Vision Ubiquitous Architecture System
Abstract:
Different methods containing biometric algorithms are presented for the representation of eigenfaces detection including face recognition, are identification and verification. Our theme of this research is to manage the critical processing stages (accuracy, speed, security and monitoring) of face activities with the flexibility of searching and edit the secure authorized database. In this paper we implement different techniques such as eigenfaces vector reduction by using texture and shape vector phenomenon for complexity removal, while density matching score with Face Boundary Fixation (FBF) extracted the most likelihood characteristics in this media processing contents. We examine the development and performance efficiency of the database by applying our creative algorithms in both recognition and detection phenomenon. Our results show the performance accuracy and security gain with better achievement than a number of previous approaches in all the above processes in an encouraging mode.Keywords: Ubiquitous architecture, verification, Identification, recognition
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 12681582 Enhanced Automated Teller Machine Using Short Message Service Authentication Verification
Authors: Rasheed Gbenga Jimoh, Akinbowale Nathaniel Babatunde
Abstract:
The use of Automated Teller Machine (ATM) has become an important tool among commercial banks, customers of banks have come to depend on and trust the ATM conveniently meet their banking needs. Although the overwhelming advantages of ATM cannot be over-emphasized, its alarming fraud rate has become a bottleneck in it’s full adoption in Nigeria. This study examined the menace of ATM in the society another cost of running ATM services by banks in the country. The researcher developed a prototype of an enhanced Automated Teller Machine Authentication using Short Message Service (SMS) Verification. The developed prototype was tested by Ten (10) respondents who are users of ATM cards in the country and the data collected was analyzed using Statistical Package for Social Science (SPSS). Based on the results of the analysis, it is being envisaged that the developed prototype will go a long way in reducing the alarming rate of ATM fraud in Nigeria.
Keywords: ATM, ATM Fraud, E-banking, Prototyping.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 21371581 Verification of Space System Dynamics Using the MATLAB Identification Toolbox in Space Qualification Test
Authors: Y. V. Kim
Abstract:
This article presents an approach with regards to the Functional Testing of Space System (SS) that could be a space vehicle (spacecraft-S/C) and/or its equipment and components – S/C subsystems. This test should finalize the Space Qualification Tests (SQT) campaign. It could be considered as a generic test and used for a wide class of SS that, from the point of view of System Dynamics and Control Theory, may be described by the ordinary differential equations. The suggested methodology is based on using semi-natural experiment laboratory stand that does not require complicated, precise and expensive technological control-verification equipment. However, it allows for testing totally assembled system during Assembling, Integration and Testing (AIT) activities at the final phase of SQT, involving system hardware (HW) and software (SW). The test physically activates system input (sensors) and output (actuators) and requires recording their outputs in real time. The data are then inserted in a laboratory computer, where it is post-experiment processed by the MATLAB/Simulink Identification Toolbox. It allows for estimating the system dynamics in the form of estimation of its differential equation coefficients through the verification experimental test and comparing them with expected mathematical model, prematurely verified by mathematical simulation during the design process. Mathematical simulation results presented in the article show that this approach could be applicable and helpful in SQT practice. Further semi-natural experiments should specify detail requirements for the test laboratory equipment and test-procedures.
Keywords: system dynamics, space system ground tests, space qualification, system dynamics identification, satellite attitude control, assembling integration and testing
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 4721580 Modeling Biology Inspired Reactive Agents Using X-machines
Authors: George Eleftherakis, Petros Kefalas, Anna Sotiriadou, Evangelos Kehris
Abstract:
Recent advances in both the testing and verification of software based on formal specifications of the system to be built have reached a point where the ideas can be applied in a powerful way in the design of agent-based systems. The software engineering research has highlighted a number of important issues: the importance of the type of modeling technique used; the careful design of the model to enable powerful testing techniques to be used; the automated verification of the behavioural properties of the system; the need to provide a mechanism for translating the formal models into executable software in a simple and transparent way. This paper introduces the use of the X-machine formalism as a tool for modeling biology inspired agents proposing the use of the techniques built around X-machine models for the construction of effective, and reliable agent-based software systems.
Keywords: Biology inspired agent, formal methods, x-machines.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14541579 A Collusion-Resistant Distributed Signature Delegation Based on Anonymous Mobile Agent
Authors: Omaima Bamasak
Abstract:
This paper presents a novel method that allows an agent host to delegate its signing power to an anonymous mobile agent in such away that the mobile agent does not reveal any information about its host-s identity and, at the same time, can be authenticated by the service host, hence, ensuring fairness of service provision. The solution introduces a verification server to verify the signature generated by the mobile agent in such a way that even if colluding with the service host, both parties will not get more information than what they already have. The solution incorporates three methods: Agent Signature Key Generation method, Agent Signature Generation method, Agent Signature Verification method. The most notable feature of the solution is that, in addition to allowing secure and anonymous signature delegation, it enables tracking of malicious mobile agents when a service host is attacked. The security properties of the proposed solution are analyzed, and the solution is compared with the most related work.Keywords: Anonymous signature delegation, collusion resistance, e-commerce fairness, mobile agent security.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14001578 Stages of Changes for Physical Activity among Iranian Adolescent Girls
Authors: Ashraf Pirasteh, Alireza Hidarnia, Ali Asghari, Soghrate Faghihzadeh, Fazlollah Ghofranipour
Abstract:
Background: Regular physical activity contributes positively to physical and psychological health. In the present study, the stages of change of physical activity and the total physical Aims: The aim of this study was to investigate the proportion of adolescent girls in each stages of change and the causative factors associated with physical activity such as the related social support and self efficacy in a sample of the high school students. Methods: In this study, Social Cognitive Theory (SCT) and the Transtheorical Model (TTM) guided instrument development. The data regarding the demographics, psychosocial determinants of physical activity, stage of change and physical activity was gathered by questionnaires. Several measures of psychosocial determinants of physical activity were translated from English into Persian using the back-translation technique. These translated measures were administered to 512 ninth and tenth-grade Iranian high school students for factor analysis. Results: The distribution of the stage of change for physical activity was as follow: 18/5% in precontemplation, 23.4% in contemplation, 38.2% in preparation, 4.6% in action and 15.3% in maintenance. They were in 80.1% pre-adoption stages (precontemplation stage, contemplation stage and preparation stage) and 19.9% post-adoption stages (action stage and maintenance stage) of physical activity. There was a significant relate between age and physical activity in adolescent girls (age-related decline of physical activity) p<0001. Conclusion: The findings of the present study can contribute to improve health behaviors and for administration of health promotion programs in the adolescent populations.Keywords: Adolescent, Iranian girls, Physical activity, Stages of change
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 19231577 Verification and Application of Finite Element Model Developed for Flood Routing in Rivers
Authors: A. L. Qureshi, A. A. Mahessar, A. Baloch
Abstract:
Flood wave propagation in river channel flow can be enunciated by nonlinear equations of motion for unsteady flow. It is difficult to find analytical solution of these non-linear equations. Hence, in this paper verification of the finite element model has been carried out against available numerical predictions and field data. The results of the model indicate a good matching with both Preissmann scheme and HEC-RAS model for a river reach of 29km at both sites (15km from upstream and at downstream end) for discharge hydrographs. It also has an agreeable comparison with the Preissemann scheme for the flow depth (stage) hydrographs. The proposed model has also been applying to forecast daily discharges at 400km downstream in the Indus River from Sukkur barrage of Sindh, Pakistan, which demonstrates accurate model predictions with observed the daily discharges. Hence, this model may be utilized for flood warnings in advance.
Keywords: Finite Element Method, Flood Forecasting, HEC-RAS, Indus river.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2627