Search results for: M. S. Kaiser
31 Investigation of Mg and Zr Addition on the Mechanical Properties of Commercially Pure Al
Authors: Samiul Kaiser, M. S. Kaiser
Abstract:
The influence of Mg and Zr addition on mechanical properties such as hardness, tensile strength and impact energy of commercially pure Al are investigated. The microstructure and fracture behavior are also studied by using Optical and Scanning Electron Microscopy. It is observed that magnesium addition improves the mechanical properties of commercially pure Al at the expense of ductility due to formation of β″ (Al3Mg) and β′ (Al3Mg2) phase into the alloy. Zr addition also plays a positive role through grain refinement effect and the formation of metastable L12 Al3Zr precipitates. In addition, it is observed that the fractured surface of Mg added alloy is brittle and higher numbers of dimples are observed in case of Zr added alloy.
Keywords: Al-alloys, hardness, tensile strength, impact energy, microstructure.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 67730 Design of an M-Channel Cosine Modulated Filter Bank by New Cosh Window Based FIR Filters
Authors: Jyotsna Ogale, Alok Jain
Abstract:
In this paper newly reported Cosh window function is used in the design of prototype filter for M-channel Near Perfect Reconstruction (NPR) Cosine Modulated Filter Bank (CMFB). Local search optimization algorithm is used for minimization of distortion parameters by optimizing the filter coefficients of prototype filter. Design examples are presented and comparison has been made with Kaiser window based filterbank design of recently reported work. The result shows that the proposed design approach provides lower distortion parameters and improved far-end suppression than the Kaiser window based design of recent reported work.Keywords: Window function, Cosine modulated filterbank, Local search optimization.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 260029 Grid Artifacts Suppression in Computed Radiographic Images
Authors: Igor Belykh
Abstract:
Anti-scatter grids used in radiographic imaging for the contrast enhancement leave specific artifacts. Those artifacts may be visible or may cause Moiré effect when digital image is resized on a diagnostic monitor. In this paper we propose an automated grid artifactsdetection and suppression algorithm which is still an actual problem. Grid artifacts detection is based on statistical approach in spatial domain. Grid artifacts suppression is based on Kaiser bandstop filter transfer function design and application avoiding ringing artifacts. Experimental results are discussed and concluded with description of advantages over existing approaches.
Keywords: Computed radiography, grid artifacts, image filtering.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 429228 New Efficient Iterative Optimization Algorithm to Design the Two Channel QMF Bank
Authors: Ram Kumar Soni, Alok Jain, Rajiv Saxena
Abstract:
This paper proposes an efficient method for the design of two channel quadrature mirror filter (QMF) bank. To achieve minimum value of reconstruction error near to perfect reconstruction, a linear optimization process has been proposed. Prototype low pass filter has been designed using Kaiser window function. The modified algorithm has been developed to optimize the reconstruction error using linear objective function through iteration method. The result obtained, show that the performance of the proposed algorithm is better than that of the already exists methods.Keywords: Filterbank, near perfect reconstruction, Kaiserwindow, QMF.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 167627 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 156026 Wet Sliding Wear and Frictional Behavior of Commercially Available Perspex
Authors: S. Reaz Ahmed, M. S. Kaiser
Abstract:
The tribological behavior of commercially used Perspex was evaluated under dry and wet sliding condition using a pin-on-disc wear tester with different applied loads ranging from 2.5 to 20 N. Experiments were conducted with varying sliding distance from 0.2 km to 4.6 km, wherein the sliding velocity was kept constant, 0.64 ms-1. The results reveal that the weight loss increases with applied load and the sliding distance. The nature of the wear rate was very similar in both the sliding environments in which initially the wear rate increased very rapidly with increasing sliding distance and then progressed to a slower rate. Moreover, the wear rate in wet sliding environment was significantly lower than that under dry sliding condition. The worn surfaces were characterized by optical microscope and SEM. It is found that surface modification has significant effect on sliding wear performance of Perspex.
Keywords: Perspex, wear, friction, SEM.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 119625 Time-Delay Estimation Using Cross-ΨB-Energy Operator
Authors: Z. Saidi, A.O. Boudraa, J.C. Cexus, S. Bourennane
Abstract:
In this paper, a new time-delay estimation technique based on the cross IB-energy operator [5] is introduced. This quadratic energy detector measures how much a signal is present in another one. The location of the peak of the energy operator, corresponding to the maximum of interaction between the two signals, is the estimate of the delay. The method is a fully data-driven approach. The discrete version of the continuous-time form of the cross IBenergy operator, for its implementation, is presented. The effectiveness of the proposed method is demonstrated on real underwater acoustic signals arriving from targets and the results compared to the cross-correlation method.Keywords: Teager-Kaiser energy operator, Cross-energyoperator, Time-Delay, Underwater acoustic signals.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 564924 A Computationally Efficient Design for Prototype Filters of an M-Channel Cosine Modulated Filter Bank
Authors: Neela. R. Rayavarapu, Neelam Rup Prakash
Abstract:
The paper discusses a computationally efficient method for the design of prototype filters required for the implementation of an M-band cosine modulated filter bank. The prototype filter is formulated as an optimum interpolated FIR filter. The optimum interpolation factor requiring minimum number of multipliers is used. The model filter as well as the image suppressor will be designed using the Kaiser window. The method will seek to optimize a single parameter namely cutoff frequency to minimize the distortion in the overlapping passband.Keywords: Cosine modulated filter bank, interpolated FIR filter, optimum interpolation factor, prototype filter.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 159623 Optimization of Laser-Induced Breakdown Spectroscopy (LIBS) for Determination of Quantum Dots (Qds) in Liquid Solutions
Authors: David Prochazka, Ľudmila Ballová, Karel Novotný, Jan Novotný, Radomír Malina, Petr Babula, Vojtěch Adam, René Kizek, Klára Procházková, Jozef Kaiser
Abstract:
Here we report on the utilization of Laser-Induced Breakdown Spectroscopy (LIBS) for determination of Quantum Dots (QDs) in liquid solution. The process of optimization of experimental conditions from choosing the carrier medium to application of colloid QDs is described. The main goal was to get the best possible signal to noise ratio. The results obtained from the measurements confirmed the capability of LIBS technique for qualitative and afterwards quantitative determination of QDs in liquid solution.Keywords: Laser-Induced Breakdown Spectroscopy, liquid analysis, nanocrystals, nanotechnology, Quantum dots.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 226322 Promoting Community Food Security and Empowerment among Somali Bantu Refugees: A Case for Community Kitchen Gardens
Authors: Michelle D. Hand, Michelle L. Kaiser
Abstract:
African refugees are among the fastest-growing populations in the United States and nearly half of these refugees come from Somalia, many of whom are Somali Bantus, the most marginalized group in Somali society. Yet limited research is available on Somali Bantu refugees. In this paper, Empowerment Theory is used to guide an in-depth exploration of the potential benefits of using community kitchen gardens to increase community food security among Somali Bantu refugees. In addition, recommendations for future research, policy and practice are offered following existing scholarly and grey source literature guidelines as informed by an Empowerment perspective to best meet the needs of this under-researched and underserved yet growing population.Keywords: Community kitchen gardens, food insecurity, refugees, Somali Bantu.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 74921 Speech Enhancement of Vowels Based on Pitch and Formant Frequency
Authors: R. Rishma Rodrigo, R. Radhika, M. Vanitha Lakshmi
Abstract:
Numerous signal processing based speech enhancement systems have been proposed to improve intelligibility in the presence of noise. Traditionally, studies of neural vowel encoding have focused on the representation of formants (peaks in vowel spectra) in the discharge patterns of the population of auditory-nerve (AN) fibers. A method is presented for recording high-frequency speech components into a low-frequency region, to increase audibility for hearing loss listeners. The purpose of the paper is to enhance the formant of the speech based on the Kaiser window. The pitch and formant of the signal is based on the auto correlation, zero crossing and magnitude difference function. The formant enhancement stage aims to restore the representation of formants at the level of the midbrain. A MATLAB software’s are used for the implementation of the system with low complexity is developed.
Keywords: Formant estimation, formant enhancement, pitch detection, speech analysis.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 164120 Precipitation Hardening Behavior of Directly Cold Rolled Al-6Mg Alloy Containing Ternary Sc and Quaternary Zi/Ti
Authors: M. S. Kaiser
Abstract:
Ageing of 75% cold rolled Al-6Mg alloy with ternary 0.4 wt% scandium and quaternary zirconium and titanium has been carried out. Alloy samples are naturally, isochronally and isothermally aged for different time and temperatures. Hardness values of the differently processed alloys have been measured to understand the ageing behavior of Al-6Mg alloy with scandium and quaternary zirconium and titanium addition. Resistivity changes with annealing time and temperature were measured to understand the precipitation behavior and recovery of strain of the alloy. Attempts were also made to understand the grain refining effect of scandium in Al-6Mg alloy. It is observed that significant hardening takes place in the aged alloys due to the precipitation of scandium aluminides and the dendrites of the Al-6Mg alloy have been refined significantly due to addition of scandium.
Keywords: Al-Mg alloys, age hardening, resistivity, metastable phase.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 208819 Optimization of the Transfer Molding Process by Implementation of Online Monitoring Techniques for Electronic Packages
Authors: Burcu Kaya, Jan-Martin Kaiser, Karl-Friedrich Becker, Tanja Braun, Klaus-Dieter Lang
Abstract:
Quality of the molded packages is strongly influenced by the process parameters of the transfer molding. To achieve a better package quality and a stable transfer molding process, it is necessary to understand the influence of the process parameters on the package quality. This work aims to comprehend the relationship between the process parameters, and to identify the optimum process parameters for the transfer molding process in order to achieve less voids and wire sweep. To achieve this, a DoE is executed for process optimization and a regression analysis is carried out. A systematic approach is represented to generate models which enable an estimation of the number of voids and wire sweep. Validation experiments are conducted to verify the model and the results are presented.Keywords: Epoxy molding compounds, optimization, regression analysis, transfer molding process, voids, wire sweep.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 153018 Effect of Heat Input on the Weld Metal Toughness of Chromium-Molybdenum Steel
Authors: M. S. Kaiser
Abstract:
An attempt has been made to determine the strength and impact properties of Cr-Mo steel weld and base materials by varying the current during manual metal arc welding. Toughness over a temperature range from -32 to 100°C of base, heat affected zone (HAZ) and weld zones at three current settings are made. It is observed that the deterioration in notch toughness at any zone with the temperature decreases. The values of notch toughness for all zones at -32°C are almost same for any current settings. The values of notch toughness at HAZ area are higher than that of weld area due to the coarsening of ferrite grain of HAZ occurs with higher heat input. From microhardness and microstructure result, it can be concluded that large inclusion content in weld deposit is the cause of lower notch toughness value.Keywords: Chromium-Molybdenum steel, post-weld heat treatment, heat affected zone, microstructure.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 364317 Peakwise Smoothing of Data Models using Wavelets
Authors: D Sudheer Reddy, N Gopal Reddy, P V Radhadevi, J Saibaba, Geeta Varadan
Abstract:
Smoothing or filtering of data is first preprocessing step for noise suppression in many applications involving data analysis. Moving average is the most popular method of smoothing the data, generalization of this led to the development of Savitzky-Golay filter. Many window smoothing methods were developed by convolving the data with different window functions for different applications; most widely used window functions are Gaussian or Kaiser. Function approximation of the data by polynomial regression or Fourier expansion or wavelet expansion also gives a smoothed data. Wavelets also smooth the data to great extent by thresholding the wavelet coefficients. Almost all smoothing methods destroys the peaks and flatten them when the support of the window is increased. In certain applications it is desirable to retain peaks while smoothing the data as much as possible. In this paper we present a methodology called as peak-wise smoothing that will smooth the data to any desired level without losing the major peak features.Keywords: smoothing, moving average, peakwise smoothing, spatialdensity models, planar shape models, wavelets.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 175016 Investigation of Chip Formation Characteristics during Surface Finishing of HDPE Samples
Authors: M. S. Kaiser, S. Reaz Ahmed
Abstract:
Chip formation characteristics are investigated during surface finishing of high density polyethylene (HDPE) samples using a shaper machine. Both the cutting speed and depth of cut are varied continually to enable observations under various machining conditions. The generated chips are analyzed in terms of their shape, size, and deformation. Their physical appearances are also observed using digital camera and optical microscope. The investigation shows that continuous chips are obtained for all the cutting conditions. It is observed that cutting speed is more influential than depth of cut to cause dimensional changes of chips. Chips curl radius is also found to increase gradually with the increase of cutting speed. The length of continuous chips remains always smaller than the job length, and the corresponding discrepancies are found to be more prominent at lower cutting speed. Microstructures of the chips reveal that cracks are formed at higher cutting speeds and depth of cuts, which is not that significant at low depth of cut.
Keywords: HDPE, surface-finishing, chip formation, deformation, roughness.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 54015 Localizing Acoustic Touch Impacts using Zip-stuffing in Complex k-space Domain
Authors: R. Bremananth, Andy W. H. Khong, A. Chitra
Abstract:
Visualizing sound and noise often help us to determine an appropriate control over the source localization. Near-field acoustic holography (NAH) is a powerful tool for the ill-posed problem. However, in practice, due to the small finite aperture size, the discrete Fourier transform, FFT based NAH couldn-t predict the activeregion- of-interest (AROI) over the edges of the plane. Theoretically few approaches were proposed for solving finite aperture problem. However most of these methods are not quite compatible for the practical implementation, especially near the edge of the source. In this paper, a zip-stuffing extrapolation approach has suggested with 2D Kaiser window. It is operated on wavenumber complex space to localize the predicted sources. We numerically form a practice environment with touch impact databases to test the localization of sound source. It is observed that zip-stuffing aperture extrapolation and 2D window with evanescent components provide more accuracy especially in the small aperture and its derivatives.Keywords: Acoustic source localization, Near-field acoustic holography (NAH), FFT, Extrapolation, k-space wavenumber errors.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 164814 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 159113 Corrosion Behaviour of Hypereutectic Al-Si Automotive Alloy in Different pH Environment
Authors: M. Al Nur, M. S. Kaiser
Abstract:
Corrosion behaviour of hypereutectic Al-19Si automotive alloy in different pH=1, 3, 5, 7, 9, 11, and 13 environments was carried out using conventional gravimetric measurements and was complemented by resistivity, optical micrograph, scanning electron microscopy (SEM) and X-ray analyzer (EDX) investigations. Gravimetric analysis confirmed that the highest corrosion rate is shown at pH 13 followed by pH 1. Minimum corrosion occurs in the pH range of 3.0 to 11 due to establishment of passive layer on the surface. The highest corrosion rate at pH 13 is due to the presence of sodium hydroxide in the solution which dissolves the surface oxide film at a steady rate. At pH 1, it can be attributed that the presence of aggressive chloride ions serves to pick up the damage of the passive films at localized regions. With varying exposure periods by both, the environment complies with the normal corrosion rate profile that is an initial steep rise followed by a nearly constant value of corrosion rate. Resistivity increases in case of pH 1 solution for the higher pit formation and decreases at pH 13 due to formation of thin film. The SEM image of corroded samples immersed in pH 1 solution clearly shows pores on the surface and in pH 13 solution, and the corrosion layer seems more compact and homogenous and not porous.
Keywords: Al-Si alloy, corrosion, pH, resistivity, SEM.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 101812 Person-Environment Fit (PE Fit): Evidence from Brazil
Authors: Jucelia Appio, Danielle Deimling De Carli, Bruno Henrique Rocha Fernandes, Nelson Natalino Frizon
Abstract:
The purpose of this paper is to investigate if there are positive and significant correlations between the dimensions of Person-Environment Fit (Person-Job, Person-Organization, Person-Group and Person-Supervisor) at the “Best Companies to Work for” in Brazil in 2017. For that, a quantitative approach was used with a descriptive method being defined as a research sample the "150 Best Companies to Work for", according to data base collected in 2017 and provided by Fundação Instituto of Administração (FIA) of the University of São Paulo (USP). About the data analysis procedures, asymmetry and kurtosis, factorial analysis, Kaiser-Meyer-Olkin (KMO) tests, Bartlett sphericity and Cronbach's alpha were used for the 69 research variables, and as a statistical technique for the purpose of analyzing the hypothesis, Pearson's correlation analysis was performed. As a main result, we highlight that there was a positive and significant correlation between the dimensions of Person-Environment Fit, corroborating the H1 hypothesis that there is a positive and significant correlation between Person-Job Fit, Person-Organization Fit, Person-Group Fit and Person-Supervisor Fit.
Keywords: Human resource management, person-environment fit, strategic people management, best companies to work for.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 100111 Extracting Single Trial Visual Evoked Potentials using Selective Eigen-Rate Principal Components
Authors: Samraj Andrews, Ramaswamy Palaniappan, Nidal Kamel
Abstract:
In single trial analysis, when using Principal Component Analysis (PCA) to extract Visual Evoked Potential (VEP) signals, the selection of principal components (PCs) is an important issue. We propose a new method here that selects only the appropriate PCs. We denote the method as selective eigen-rate (SER). In the method, the VEP is reconstructed based on the rate of the eigen-values of the PCs. When this technique is applied on emulated VEP signals added with background electroencephalogram (EEG), with a focus on extracting the evoked P3 parameter, it is found to be feasible. The improvement in signal to noise ratio (SNR) is superior to two other existing methods of PC selection: Kaiser (KSR) and Residual Power (RP). Though another PC selection method, Spectral Power Ratio (SPR) gives a comparable SNR with high noise factors (i.e. EEGs), SER give more impressive results in such cases. Next, we applied SER method to real VEP signals to analyse the P3 responses for matched and non-matched stimuli. The P3 parameters extracted through our proposed SER method showed higher P3 response for matched stimulus, which confirms to the existing neuroscience knowledge. Single trial PCA using KSR and RP methods failed to indicate any difference for the stimuli.Keywords: Electroencephalogram, P3, Single trial VEP.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 164110 Wear Behavior of Commercial Aluminium Engine Block and Piston under Dry Sliding Condition
Authors: M. S. Kaiser, Swagata Dutta
Abstract:
In the present work, the effect of load and sliding distance on the performance tribology of commercially used aluminium-silicon engine block and piston was evaluated at ambient conditions with humidity of 80% under dry sliding conditions using a pin-on-disc with two different loads of 5N and 20N yielding applied pressure of 0.30MPa and 1.4MPa, respectively, at sliding velocity of 0.29ms-1 and with varying sliding distance ranging from 260m- 4200m. Factors and conditions that had significant effect were identified. The results showed that the load and the sliding distance affect the wear rate of the alloys and the wear rate increased with increasing load for both the alloys. Wear rate also increases almost linearly at low loads and increase to a maximum then attain a plateau with increasing sliding distance. For both applied loads the piston alloy showed the better performance due to higher Ni and Mg content. The worn surface and wear debris was characterized by optical microscope, SEM and EDX analyzer. The worn surface was characterized by surface with shallow grooves at loads while the groove width and depth increased as the loads increases. Oxidative wear was found to be the predominant mechanisms in the dry sliding of Al-Si alloys at low loads.
Keywords: Wear, friction, gravimetric analysis, aluminiumsilicon alloys, SEM, EDX.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 25319 Informal Education and Developing Entrepreneurial Skills among Farmers in Malaysia
Authors: Golnaz Rezai, Zainalabidin Mohamed, Mad Nasir Shamsudin
Abstract:
The Malaysian government is promoting entrepreneurship development skills amongst farmers through informal courses. These courses will concentrate on teaching managerial skills as inevitable means for small farms to succeed by making farmers more creative and innovative. Therefore it is important to assess the effect of informal agri-entrepreneurial training in developing entrepreneurship among the farmers in Malaysia. Seven hundred and ninety six farmers (796) farmers were interviewed via structured questionnaire to define their opinion on whether the current informal educational and training establishments are sufficient to teach and develop entrepreneurial skills. Factor analysis and logic regression analysis were used to determine the motivating factors and predict their impact on the development of entrepreneurial skills. The result from the factor analysis led us to investigate the association between these factors and farmers- opinions about the development of entrepreneurial skills and traits through participating in informal entrepreneurship training or education. The outcome has shown us that the importance of informal training to promote entrepreneurship among farmers is crucial. The training should be intensified to encourage farmers to not only focus on the modern technologies but also on the fundamental changes in their attitude towards agriculture as a business. DOA: KMO: Kaiser- Meyer- Olkin Test MOA: Ministry of Agriculture NMP: Ninth Malaysia Plan NAP: Third National Agricultural Policy (2000-2010)Keywords: Entrepreneurial skills, farmers, informal education, Malaysia
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 37698 Formal Analysis of a Public-Key Algorithm
Authors: Markus Kaiser, Johannes Buchmann
Abstract:
In this article, a formal specification and verification of the Rabin public-key scheme in a formal proof system is presented. 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. A major objective of this article is the presentation of the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Moreover, we explicate a (computer-proven) formalization of correctness as well as a computer verification of security properties using a straight-forward computation model in Isabelle/HOL. The analysis uses a given database to prove formal properties of our implemented functions with computer support. The main task in designing a practical formalization of correctness as well as efficient computer proofs of 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 efficient formal proofs. Consequently, we get reliable proofs with a minimal error rate augmenting the used database, what 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 15377 A Formal Approach for Proof Constructions in Cryptography
Authors: Markus Kaiser, Johannes Buchmann
Abstract:
In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 14706 Computer Verification in Cryptography
Authors: Markus Kaiser, Johannes Buchmann
Abstract:
In this paper we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (o--algebras, probability spaces and condi¬tional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes' Formula. Besides we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this paper shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.
Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 21815 Teager-Huang Analysis Applied to Sonar Target Recognition
Authors: J.-C. Cexus, A.O. Boudraa
Abstract:
In this paper, a new approach for target recognition based on the Empirical mode decomposition (EMD) algorithm of Huang etal. [11] and the energy tracking operator of Teager [13]-[14] is introduced. The conjunction of these two methods is called Teager-Huang analysis. This approach is well suited for nonstationary signals analysis. The impulse response (IR) of target is first band pass filtered into subsignals (components) called Intrinsic mode functions (IMFs) with well defined Instantaneous frequency (IF) and Instantaneous amplitude (IA). Each IMF is a zero-mean AM-FM component. In second step, the energy of each IMF is tracked using the Teager energy operator (TEO). IF and IA, useful to describe the time-varying characteristics of the signal, are estimated using the Energy separation algorithm (ESA) algorithm of Maragos et al .[16]-[17]. In third step, a set of features such as skewness and kurtosis are extracted from the IF, IA and IMF energy functions. The Teager-Huang analysis is tested on set of synthetic IRs of Sonar targets with different physical characteristics (density, velocity, shape,? ). PCA is first applied to features to discriminate between manufactured and natural targets. The manufactured patterns are classified into spheres and cylinders. One hundred percent of correct recognition is achieved with twenty three echoes where sixteen IRs, used for training, are free noise and seven IRs, used for testing phase, are corrupted with white Gaussian noise.
Keywords: Target recognition, Empirical mode decomposition, Teager-Kaiser energy operator, Features extraction.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 22844 Utilization of Laser-Ablation Based Analytical Methods for Obtaining Complete Chemical Information of Algae
Authors: Pavel Pořízka, David Prochazka, Karel Novotný, Ota Samek, ZdeněkPilát, Klára Procházková, and Jozef Kaiser
Abstract:
Themain goal of this article is to find efficient methods for elemental and molecular analysis of living microorganisms (algae) under defined environmental conditions and cultivation processes. The overall knowledge of chemical composition is obtained utilizing laser-based techniques, Laser- Induced Breakdown Spectroscopy (LIBS) for acquiring information about elemental composition and Raman Spectroscopy for gaining molecular information, respectively. Algal cells were suspended in liquid media and characterized using their spectra. Results obtained employing LIBS and Raman Spectroscopy techniques will help to elucidate algae biology (nutrition dynamics depending on cultivation conditions) and to identify algal strains, which have the potential for applications in metal-ion absorption (bioremediation) and biofuel industry. Moreover, bioremediation can be readily combined with production of 3rd generation biofuels. In order to use algae for efficient fuel production, the optimal cultivation parameters have to be determinedleading to high production of oil in selected cellswithout significant inhibition of the photosynthetic activity and the culture growth rate, e.g. it is necessary to distinguish conditions for algal strain containing high amount of higher unsaturated fatty acids. Measurements employing LIBS and Raman Spectroscopy were utilized in order to give information about alga Trachydiscusminutus with emphasis on the amount of the lipid content inside the algal cell and the ability of algae to withdraw nutrients from its environment and bioremediation (elemental composition), respectively. This article can serve as the reference for further efforts in describing complete chemical composition of algal samples employing laserablation techniques.Keywords: Laser-Induced Breakdown Spectroscopy, Raman Spectroscopy, Algae, Algal strains, Bioremediation, Biofuels.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 22503 Comparison of Power Generation Status of Photovoltaic Systems under Different Weather Conditions
Authors: Zhaojun Wang, Zongdi Sun, Qinqin Cui, Xingwan Ren
Abstract:
Based on multivariate statistical analysis theory, this paper uses the principal component analysis method, Mahalanobis distance analysis method and fitting method to establish the photovoltaic health model to evaluate the health of photovoltaic panels. First of all, according to weather conditions, the photovoltaic panel variable data are classified into five categories: sunny, cloudy, rainy, foggy, overcast. The health of photovoltaic panels in these five types of weather is studied. Secondly, a scatterplot of the relationship between the amount of electricity produced by each kind of weather and other variables was plotted. It was found that the amount of electricity generated by photovoltaic panels has a significant nonlinear relationship with time. The fitting method was used to fit the relationship between the amount of weather generated and the time, and the nonlinear equation was obtained. Then, using the principal component analysis method to analyze the independent variables under five kinds of weather conditions, according to the Kaiser-Meyer-Olkin test, it was found that three types of weather such as overcast, foggy, and sunny meet the conditions for factor analysis, while cloudy and rainy weather do not satisfy the conditions for factor analysis. Therefore, through the principal component analysis method, the main components of overcast weather are temperature, AQI, and pm2.5. The main component of foggy weather is temperature, and the main components of sunny weather are temperature, AQI, and pm2.5. Cloudy and rainy weather require analysis of all of their variables, namely temperature, AQI, pm2.5, solar radiation intensity and time. Finally, taking the variable values in sunny weather as observed values, taking the main components of cloudy, foggy, overcast and rainy weather as sample data, the Mahalanobis distances between observed value and these sample values are obtained. A comparative analysis was carried out to compare the degree of deviation of the Mahalanobis distance to determine the health of the photovoltaic panels under different weather conditions. It was found that the weather conditions in which the Mahalanobis distance fluctuations ranged from small to large were: foggy, cloudy, overcast and rainy.
Keywords: Fitting, principal component analysis, Mahalanobis distance, SPSS, MATLAB.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 6752 The Examination of Prospective ICT Teachers’ Attitudes towards Application of Computer Assisted Instruction
Authors: Agâh Tuğrul Korucu, Ismail Fatih Yavuzaslan, Lale Toraman
Abstract:
Nowadays, thanks to development of technology, integration of technology into teaching and learning activities is spreading. Increasing technological literacy which is one of the expected competencies for individuals of 21st century is associated with the effective use of technology in education. The most important factor in effective use of technology in education institutions is ICT teachers. The concept of computer assisted instruction (CAI) refers to the utilization of information and communication technology as a tool aided teachers in order to make education more efficient and improve its quality in the process of educational. Teachers can use computers in different places and times according to owned hardware and software facilities and characteristics of the subject and student in CAI. Analyzing teachers’ use of computers in education is significant because teachers are the ones who manage the course and they are the most important element in comprehending the topic by students. To accomplish computer-assisted instruction efficiently is possible through having positive attitude of teachers. Determination the level of knowledge, attitude and behavior of teachers who get the professional knowledge from educational faculties and elimination of deficiencies if any are crucial when teachers are at the faculty. Therefore, the aim of this paper is to identify ICT teachers' attitudes toward computer-assisted instruction in terms of different variables. Research group consists of 200 prospective ICT teachers studying at Necmettin Erbakan University Ahmet Keleşoğlu Faculty of Education CEIT department. As data collection tool of the study; “personal information form” developed by the researchers and used to collect demographic data and "the attitude scale related to computer-assisted instruction" are used. The scale consists of 20 items. 10 of these items show positive feature, while 10 of them show negative feature. The Kaiser-Meyer-Olkin (KMO) coefficient of the scale is found 0.88 and Barlett test significance value is found 0.000. The Cronbach’s alpha reliability coefficient of the scale is found 0.93. In order to analyze the data collected by data collection tools computer-based statistical software package used; statistical techniques such as descriptive statistics, t-test, and analysis of variance are utilized. It is determined that the attitudes of prospective instructors towards computers do not differ according to their educational branches. On the other hand, the attitudes of prospective instructors who own computers towards computer-supported education are determined higher than those of the prospective instructors who do not own computers. It is established that the departments of students who previously received computer lessons do not affect this situation so much. The result is that; the computer experience affects the attitude point regarding the computer-supported education positively.
Keywords: Attitude, computer based instruction, information and communication technologies, technology based instruction, teacher candidate.
Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1740