A Pattern Recognition Model of Voice-Based Personal Verification Systems for Forensic Applications

Abstract-The success of automatic speaker recognition in laboratory environments suggests applications in forensic science for establishing the Identity of individuals on the basis of features extracted from speech. A theoretical model for such a verification scheme for continuous normaliy distributed featureIss developed. The three cases of using a) single feature, b)multipliendependent measurements of a single feature, and c)multpleindependent features are explored.The number iofndependent features needed for areliable personal identification is computed based on the theoretcal model and an expklatory study of some speech featues.

A computational algorithm for the verification of tautologies in propositional calculus

A computational algorithm (based on Smullyan's analytic tableau method) that varifies whether a given well-formed formula in propositional calculus is a tautology or not has been implemented on a DEC system 10. The stepwise refinement approch of program development used for this implementation forms the subject matter of this paper. The top-down design has resulted in a modular and reliable program package. This computational algoritlhm compares favourably with the algorithm based on the well-known resolution principle used in theorem provers.

Verification of the applicability of lattice model to concrete fracture by AE study

Notched three-point bend specimens (TPB) were tested under crack mouth opening displacement (CMOD) control at a rate of 0.0004 mm/s and the entire fracture process was simulated using a regular triangular two-dimensional lattice network only over the expected fracture proces zone width. The rest of the beam specimen was discretised by a coarse triangular finite element mesh. The discrete grain structure of the concrete was generated assuming the grains to be spherical. The load versus CMOD plots thus simulated agreed reasonably well with the experimental results. Moreover, acoustic emission (AE) hits were recorded during the test and compared with the number of fractured lattice elements. It was found that the cumulative AE hits correlated well with the cumulative fractured lattice elements at all load levels thus providing a useful means for predicting when the micro-cracks form during the fracturing process, both in the pre-peak and in the post-peak regimes.

Formal Verification of Full-Wave Rectifier: A Case Study

We present a case study of formal verification of full-wave rectifier for analog and mixed signal designs. We have used the Checkmate tool from CMU [1], which is a public domain formal verification tool for hybrid systems. Due to the restriction imposed by Checkmate it necessitates to make the changes in the Checkmate implementation to implement the complex and non-linear system. Full-wave rectifier has been implemented by using the Checkmate custom blocks and the Simulink blocks from MATLAB from Math works. After establishing the required changes in the Checkmate implementation we are able to efficiently verify, the safety properties of the full-wave rectifier.

A generalized mathematical theory and experimental verification of proportional notches

A theory and generalized synthesis procedure is advocated for the design of weir notches and orifice-notches having a base in any given shape, to a depth a, such that the discharge through it is proportional to any singular monotonically-increasing function of the depth of flow measured above a certain datum. The problem is reduced to finding an exact solution of a Volterra integral equation in Abel form. The maximization of the depth of the datum below the crest of the notch is investigated. Proof is given that for a weir notch made out of one continuous curve, and for a flow proportional to the mth power of the head, it is impossible to bring the datum lower than (2m − 1)a below the crest of the notch. A new concept of an orifice-notch, having discontinuity in the curve and a division of flow into two distinct portions, is presented. The division of flow is shown to have a beneficial effect in reducing the datum below (2m − 1)a from the crest of the weir and still maintaining the proportionality of the flow. Experimental proof with one such orifice-notch is found to have a constant coefficient of discharge of 0.625. The importance of this analysis in the design of grit chambers is emphasized.

Wavelength/Time Multiple-Pulses-per-Row codes: Construction and verification

Two dimensional Optical Orthogonal Codes (OOCs) named Wavelength/Time Multiple-Pulses-per-Row (W/T MPR) codes suitable for use in incoherent fiber-optic code division multiple access (FO-CDMA) networks are reported in [6]. In this paper, we report the construction of W/T MPR codes, using Greedy Algorithm (GA), with distinct 1-D OOCs [1] as the row vectors. We present the W/T MPR codes obtained using the GA. Further, we verify the correlation properties of the generated W/T MPR codes using Matlab.

Experimental Verification of the Lateral Periodicity of Axially Periodic Incoherent Fields Using the Lau Effect

General' objects, which are specially prepared to possess restricted spatial frequency spectra, have been used in the conventional Lau experiment to obtain experimental proof for the existence of lateral periodicity arising from axial periodicity, for a subclass of axially periodic wavefields in an incoherent situation.

Automatic verification of distributed logic specifications

Formal specification is vital to the development of distributed real-time systems as these systems are inherently complex and safety-critical. It is widely acknowledged that formal specification and automatic analysis of specifications can significantly increase system reliability. Although a number of specification techniques for real-time systems have been reported in the literature, most of these formalisms do not adequately address to the constraints that the aspects of 'distribution' and 'real-time' impose on specifications. Further, an automatic verification tool is necessary to reduce human errors in the reasoning process. In this regard, this paper is an attempt towards the development of a novel executable specification language for distributed real-time systems. First, we give a precise characterization of the syntax and semantics of DL. Subsequently, we discuss the problems of model checking, automatic verification of satisfiability of DL specifications, and testing conformance of event traces with DL specifications. Effective solutions to these problems are presented as extensions to the classical first-order tableau algorithm. The use of the proposed framework is illustrated by specifying a sample problem.

Recommendations for driver licensing and traffic law enforcement in India aiming to improve road safety

During the last decade, developing countries such as India have been exhibiting rapid increase in human population and vehicles, and increase in road accidents. Inappropriate driving behaviour is considered one of the major causes of road accidents in India as compared to defective geometric design of pavement or mechanical defects in vehicles. It can result in conditions such as lack of lane discipline, disregard to traffic laws, frequent traffic violations, increase in crashes due to self-centred driving, etc. It also demotivates educated drivers from following good driving practices. Hence, improved driver behaviour can be an effective countermeasure to reduce the vulnerability of road users and inhibit crash risks. This article highlights improved driver behaviour through better driver education, driver training and licensing procedures along with good on-road enforcement; as an effective countermeasure to ensure road safety in India. Based on the review and analysis, the article also recommends certain measures pertaining to driver licensing and traffic law enforcement in India aimed at improving road safety.

Off-line signature verification using genetically optimized weighted features

This paper is concerned with off-line signature verification. Four different types of pattern representation schemes have been implemented, viz., geometric features, moment-based representations, envelope characteristics and tree-structured Wavelet features. The individual feature components in a representation are weighed by their pattern characterization capability using Genetic Algorithms. The conclusions of the four subsystems teach depending on a representation scheme) are combined to form a final decision on the validity of signature. Threshold-based classifiers (including the traditional confidence-interval classifier), neighbourhood classifiers and their combinations were studied. Benefits of using forged signatures for training purposes have been assessed. Experimental results show that combination of the Feature-based classifiers increases verification accuracy. (C) 1999 Pattern Recognition Society. Published by Elsevier Science Ltd. All rights reserved.

A Systematic Approach to Synthesis of Verification Test-suites for Modular SoC Designs

Verification is one of the important stages in designing an SoC (system on chips) that consumes upto 70% of the design time. In this work, we present a methodology to automatically generate verification test-cases to verify a class of SoCs and also enable re-use of verification resources created from one SoC to another. A prototype implementation for generating the test-cases is also presented.

CFD Based Design Optimizations of the Diffuser of a Gas Dynamically Driver Laser Cavity

Based on the an earlier CFD analysis of the performance of the gas-dynamically controlled laser cavity [1]it was found that there is possibility of optimizing the geometry of the diffuser that can bring about reductions in both size and cost of the system by examining the critical dimensional requirements of the diffuser. Consequently,an extensive CFD analysis has been carried out for a range of diffuser configurations by simulating the supersonic flow through the arrangement including the laser cavity driven by a bank of converging – diverging nozzles and the diffuser. The numerical investigations with 3D-RANS code are carried out to capture the flow patterns through diffusers past the cavity that has multiple supersonic jet interactions with shocks leading to complex flow pattern. Varying length of the diffuser plates is made to be the basic parameter of the study. The analysis reveals that the pressure recovery pattern during the flow through the diffuser from the simulation, being critical for the performance of the laser device shows its dependence on the diffuser length is weaker beyond a critical lower limit and this evaluation of this limit would provide a design guideline for a more efficient system configuration.The observation based on the parametric study shows that the pressure recovery transients in the near vicinity of the cavity is not affected for the reduction in the length of the diffuser plates up to its 10% of the initial size, indicating the design in the first configuration that was tested experimentally has a large factor of margin. The flow stability in the laser cavity is found to be unaffected since a strong and stable shock is located at the leading edge of the diffuser plates while the downstream shock and flow patterns are changed, as one would expect. Results of the study for the different lengths of diffusers in the range of 10% to its full length are presented, keeping the experimentally tested configuration used in the earlier study [1] as the reference length. The conclusions drawn from the analysis is found to be of significance since it provides new design considerations based on the understanding of the intricacies of the flow, allowing for a hardware optimization that can lead to substantial size reduction of the device with no loss of performance.

H-DBUG: A High-level Debugging Framework for Protocol Verification using Assertions

The success of an ABV IP depends highly on the associated debugging environment. An efficient debugging environment helps the user to find out the exact location of the failure. Moreover, it provides information to the user in a refined detail of abstraction and permit adequate interaction. It has also been realized that adequate visualization support helps in tracking the behavioral aspects of the Design Under Test (DUT). Currently, the debugging tools provide information in the signal level and do not provide any information about the high-level behavior of the DUT. We present a debugging framework that takes the design specification, assertions and the user intent in a simple format and provides detailed information by processing the design trace on-line, or off-line. We also present a visualization framework to ease the debugging procedure. We have experimented with industrial standard on-chip bus protocols that ensure that this utility can be incorporated successfully in the present functional verification flow.

Carnatic music analysis: Shadja, swara identification and rAga verification in AlApana using stochastic models

We analyze the AlApana of a Carnatic music piece without the prior knowledge of the singer or the rAga. AlApana is ameans to communicate to the audience, the flavor or the bhAva of the rAga through the permitted notes and its phrases. The input to our analysis is a recording of the vocal AlApana along with the accompanying instrument. The AdhAra shadja(base note) of the singer for that AlApana is estimated through a stochastic model of note frequencies. Based on the shadja, we identify the notes (swaras) used in the AlApana using a semi-continuous GMM. Using the probabilities of each note interval, we recognize swaras of the AlApana. For sampurNa rAgas, we can identify the possible rAga, based on the swaras. We have been able to achieve correct shadja identification, which is crucial to all further steps, in 88.8% of 55 AlApanas. Among them (48 AlApanas of 7 rAgas), we get 91.5% correct swara identification and 62.13% correct R (rAga) accuracy.