Off-line signature verification and forgery detection system based on fuzzy modeling

This paper presents an innovative approach for signature verification and forgery detection based on fuzzy modeling. The signature image is binarized and resized to a fixed size window and is then thinned. The thinned image is then partitioned into a fixed number of eight sub-images called boxes. This partition is done using the horizontal density approximation approach. Each sub-image is then further resized and again partitioned into twelve further sub-images using the uniform partitioning approach. The features of consideration are normalized vector angle (α) from each box. Each feature extracted from sample signatures gives rise to a fuzzy set. Since the choice of a proper fuzzification function is crucial for verification, we have devised a new fuzzification function with structural parameters, which is able to adapt to the variations in fuzzy sets. This function is employed to develop a complete forgery detection and verification system.

Development and evaluation of an ion induced x-ray emission system for the analysis of light and medium weight elements

The present work describes the development of a proton induced X-ray emission (PIXE) analysis system, especially designed and builtfor routine quantitative multi-elemental analysis of a large number of samples. The historical and general developments of the analytical technique and the physical processes involved are discussed. The philosophy, design, constructional details and evaluation of a versatile vacuum chamber, an automatic multi-sample changer, an on-demand beam pulsing system and ion beam current monitoring facility are described.The system calibration using thin standard foils of Si, P, S,Cl, K, Ca, Ti, V, Fe, Cu, Ga, Ge, Rb, Y and Mo was undertaken at proton beam energies of 1 to 3 MeV in steps of 0.5 MeV energy and compared with theoretical calculations. An independent calibration check using bovine liver Standard Reference Material was performed.  The minimum detectable limits have been experimentally determined at detector positions of 90° and 135° with respect to the incident beam for the above range of proton energies as a function of atomic number Z. The system has detection limits of typically 10- 7 to 10- 9 g for elements 14analysis and calculations of areal density of thin foils using Rutherford backscattering data.  Amniotic fluid samples supplied by South Sefton Health Authority were successfully analysed for their low base line elemental concentrations. In conclusion the findings of this work are discussed with suggestions for further work .

Design verification and validation in product lifecycle

The verification and validation of engineering designs are of primary importance as they directly influence production performance and ultimately define product functionality and customer perception. Research in aspects of verification and validation is widely spread ranging from tools employed during the digital design phase, to methods deployed for prototype verification and validation. This paper reviews the standard definitions of verification and validation in the context of engineering design and progresses to provide a coherent analysis and classification of these activities from preliminary design, to design in the digital domain and the physical verification and validation of products and processes. The scope of the paper includes aspects of system design and demonstrates how complex products are validated in the context of their lifecycle. Industrial requirements are highlighted and research trends and priorities identified. © 2010 CIRP.

A framework for specification and analysis of software architectures

Software architecture is the abstract design of a software system. It plays a key role as a bridge between requirements and implementation, and is a blueprint for development. The architecture represents a set of early design decisions that are crucial to a system. Mistakes in those decisions are very costly if they remain undetected until the system is implemented and deployed. This is where formal specification and analysis fits in. Formal specification makes sure that an architecture design is represented in a rigorous and unambiguous way. Furthermore, a formally specified model allows the use of different analysis techniques for verifying the correctness of those crucial design decisions. ^ This dissertation presented a framework, called SAM, for formal specification and analysis of software architectures. In terms of specification, formalisms and mechanisms were identified and chosen to specify software architecture based on different analysis needs. Formalisms for specifying properties were also explored, especially in the case of non-functional properties. In terms of analysis, the dissertation explored both the verification of functional properties and the evaluation of non-functional properties of software architecture. For the verification of functional property, methodologies were presented on how to apply existing model checking techniques on a SAM model. For the evaluation of non-functional properties, the dissertation first showed how to incorporate stochastic information into a SAM model, and then explained how to translate the model to existing tools and conducts the analysis using those tools. ^ To alleviate the analysis work, we also provided a tool to automatically translate a SAM model for model checking. All the techniques and methods described in the dissertation were illustrated by examples or case studies, which also served a purpose of advocating the use of formal methods in practice. ^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

Solitons in Exciton-Polariton System: Reduced Modelling, Analysis, and Numerical Studies

In this dissertation, we study the behavior of exciton-polariton quasiparticles in semiconductor microcavities, under the sourceless and lossless conditions.

First, we simplify the original model by removing the photon dispersion term, thus effectively turn the PDEs system to an ODEs system,

and investigate the behavior of the resulting system, including the equilibrium points and the wave functions of the excitons and the photons.

Second, we add the dispersion term for the excitons to the original model and prove that the band of the discontinuous solitons now become dark solitons.

Third, we employ the Strang-splitting method to our sytem of PDEs and prove the first-order and second-order error bounds in the $H^1$ norm and the $L_2$ norm, respectively.

Using this numerical result, we analyze the stability of the steady state bright soliton solution. This solution revolves around the $x$-axis as time progresses

and the perturbed soliton also rotates around the $x$-axis and tracks closely in terms of amplitude but lags behind the exact one. Our numerical result shows orbital

stability but no $L_2$ stability.

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Isolation of Pseudomonas aeruginosa strains from dental office environments and units in Barretos, state of São Paulo, Brazil, and analysis of their susceptibility to antimicrobial drugs

A wide variety of opportunistic pathogens has been detected in the tubing supplying water to odontological equipment, in special in the biofilm lining of these tubes. Among these pathogens, Pseudomonas aeruginosa, one of the leading causes of nosocomial infections, is frequently found in water lines supplying dental units. In the present work, 160 samples of water, and 200 fomite samples from forty dental units were collected in the city of Barretos, State of São Paulo, Brazil and evaluated between January and July, 2005. Seventy-six P. aeruginosa strains, isolated from the dental environment (5 strains) and water system (71 strains), were tested for susceptibility to six antimicrobial drugs most frequently used against P. aeruginosa infections. Susceptibility to ciprofloxacin, followed by meropenem was the predominant profile. The need for effective means of reducing the microbial burden within dental unit water lines is emphasized, and the risk of exposure and cross-infection in dental practice, in special when caused by opportunistic pathogens like P. aeruginosa, are highlighted.

Association of Trypanosoma vivax in extracellular sites with central nervous system lesions and changes in cerebrospinal fluid in experimentally infected goats

Changes in cerebrospinal fluid (CSF) and anatomical and histopathological central nervous system (CNS) lesions were evaluated, and the presence of Trypanosoma vivax in CNS tissues was investigated through PCR. Twelve adult male goats were divided into three groups (G): G1, infected with T. vivax and evaluated during the acute phase; G2, infected goats evaluated during the chronic phase; and G3, consisting of non-infected goats. Each goat from G1 and G2 was infected with 1.25 x 10(5) trypomastigotes. Cerebrospinal fluid (CSF) analysis and investigation of T. vivax was performed at the 15(th) day post-infection (dpi) in G1 goats and on the fifth day after the manifestation of nervous system infection signs in G2 goats. All goats were necropsied, and CNS fragments from G1 and G2 goats were evaluated by PCR for the determination of T. vivax. Hyperthermia, anemia and parasitemia were observed from the fifth dpi for G1 and G2, with the highest parasitemia peak between the seventh and 21(st) dpi. Nervous system infection signs were observed in three G2 goats between the 30(th) and 35(th) dpi. CSF analysis revealed the presence of T. vivax for G2. Meningitis and meningoencephalitis were diagnosed in G2. PCR were positive for T. vivax in all the samples tested. In conclusion, T. vivax may reach the nervous tissue resulting in immune response from the host, which is the cause of progressive clinical and pathological manifestations of the CNS in experimentally infected goats.

Engineering real-time applications with WorldFIP: tools and analysis

WorldFIP is standardised as European Norm EN 50170 - General Purpose Field Communication System. Field communication systems (fieldbuses) started to be widely used as the communication support for distributed computer-controlled systems (DCCS), and are being used in all sorts of process control and manufacturing applications within different types of industries. There are several advantages in using fieldbuses as a replacement of for the traditional point-to-point links between sensors/actuators and computer-based control systems. Indeed they concern economical ones (cable savings) but, importantly, fieldbuses allow an increased decentralisation and distribution of the processing power over the field. Typically DCCS have real-time requirements that must be fulfilled. By this, we mean that process data must be transferred between network computing nodes within a maximum admissible time span. WorldFIP has very interesting mechanisms to schedule data transfers. It explicit distinguishes to types of traffic: periodic and aperiodic. In this paper we describe how WorldFIP handles these two types of traffic, and more importantly, we provide a comprehensive analysis for guaranteeing the real-time requirements of both types of traffic. A major contribution is made in the analysis of worst-case response time of aperiodic transfer requests.

A Logic and tool for local reasoning about security protocols

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

A system verification strategy based on the BST infrastructure

A good verification strategy should bring near the simulation and real functioning environments. In this paper we describe a system-level co-verification strategy that uses a common flow for functional simulation, timing simulation and functional debug. This last step requires using a BST infrastructure, now widely available on commercial devices, specially on FPGAs with medium/large pin-counts.

Rat hepatocyte invasion by Listeria monocytogenes and analysis of TNF-alpha role in apoptosis

Listeria monocytogenes, etiological agent of severe human foodborne infection, uses sophisticated mechanisms of entry into host cytoplasm and manipulation of the cellular cytoskeleton, resulting in cell death. The host cells and bacteria interaction may result in cytokine production as Tumor Necrosis Factor (TNF) alpha. Hepatocytes have potential to produce pro-inflammatory cytokines as TNF-alpha when invaded by bacteria. In the present work we showed the behavior of hepatocytes invaded by L. monocytogenes by microscopic analysis, determination of TNF-alpha production by bioassay and analysis of the apoptosis through TUNEL technique. The presence of bacterium, in ratios that ranged from 5 to 50,000 bacteria per cell, induced the rupture of cellular monolayers. We observed the presence of internalized bacteria in the first hour of incubation by electronic microscopy. The levels of TNF-alpha increased from first hour of incubation to sixth hour, ranging from 0 to 3749 pg/mL. After seven and eight hours of incubation non-significant TNF-alpha levels decrease occurred, indicating possible saturation of cellular receptors. Thus, the quantity of TNF-alpha produced by hepatocytes was dependent of the incubation time, as well as of the proportion between bacteria and cells. The apoptosis rate increased in direct form with the incubation time (1 h to 8 + 24 h), ranging from 0 to 43%, as well as with the bacteria : cells ratio. These results show the ability of hepatocyte invasion by non-hemolytic L. monocytogenes, and the main consequences of this phenomenon were the release of TNF-alpha by hepatocytes and the induction of apoptosis. We speculate that hepatocytes use apoptosis induced by TNF-alpha for release bacteria to extracellular medium. This phenomenon may facilitate the bacteria destruction by the immune system.