Commenced in January 2007
Frequency: Monthly
Edition: International
Paper Count: 10

Verification Related Publications

10 Seamless MATLAB® to Register-Transfer Level Design Methodology Using High-Level Synthesis

Authors: Petri Solanti, Russell Klein

Abstract:

Many designers are asking for an automated path from an abstract mathematical MATLAB model to a high-quality Register-Transfer Level (RTL) hardware description. Manual transformations of MATLAB or intermediate code are needed, when the design abstraction is changed. Design conversion is problematic as it is multidimensional and it requires many different design steps to translate the mathematical representation of the desired functionality to an efficient hardware description with the same behavior and configurability. Yet, a manual model conversion is not an insurmountable task. Using currently available design tools and an appropriate design methodology, converting a MATLAB model to efficient hardware is a reasonable effort. This paper describes a simple and flexible design methodology that was developed together with several design teams.

Keywords: Verification, Design methodology, MATLAB, High-Level Synthesis

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 153
9 I²C Master-Slave Integration

Authors: Rozita Borhan, Lam Kien Sieng

Abstract:

This paper describes I²C Slave implementation using I²C master obtained from the OpenCores website. This website provides free Verilog and VHDL Codes to users. The design implementation for the I²C slave is in Verilog Language and uses EDA tools for ASIC design known as ModelSim from Mentor Graphic. This tool is used for simulation and verification purposes. Common application for this I²C Master-Slave integration is also included. This paper also addresses the advantages and limitations of the said design.

Keywords: Verification, verilog, I²C, master, OpenCores, slave

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3585
8 Validation of the Formal Model of Web Services Applications for Digital Reference Service of Library Information System

Authors: Zainab M. Musa, Nordin M. A. Rahman, Julaily A. Jusoh

Abstract:

The web services applications for digital reference service (WSDRS) of LIS model is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient way of satisfying users’ needs in the reference section of libraries. The formal WSDRS model consists of the Z specifications of all the informal specifications of the model. This paper discusses the formal validation of the Z specifications of WSDRS model. The authors formally verify and thus validate the properties of the model using Z/EVES theorem prover.

Keywords: Validation, Verification, Formal, Theorem Proving

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1061
7 Experimental Verification and Finite Element Analysis of a Sliding Door System Used in Automotive Industry

Authors: C. Guven, M. Tufekci, E. Bayik, O. Gedik, M. Tas

Abstract:

A sliding door system is used in commercial vehicles and passenger cars to allow a larger unobstructed access to the interior for loading and unloading. The movement of a sliding door on vehicle body is ensured by mechanisms and tracks having special cross-section which is manufactured by roll forming and stretch bending process. There are three tracks and three mechanisms which are called upper, central and lower on a sliding door system. There are static requirements as strength on different directions, rigidity for mechanisms, door drop off, door sag; dynamic requirements as high energy slam opening-closing and durability requirement to validate these products. In addition, there is a kinematic requirement to find out force values from door handle during manual operating. In this study, finite element analysis and physical test results which are realized for sliding door systems will be shared comparatively.

Keywords: Experimental, Finite Element Analysis, Verification, sliding door, vehicle tests

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2490
6 Modeling and Verification for the Micropayment Protocol Netpay

Authors: Kaylash Chaudhary, Ansgar Fehnker

Abstract:

There are many virtual payment systems available to conduct micropayments. It is essential that the protocols satisfy the highest standards of correctness. This paper examines the Netpay Protocol [3], provide its formalization as automata model, and prove two important correctness properties, namely absence of deadlock and validity of an ecoin during the execution of the protocol. This paper assumes a cooperative customer and will prove that the protocol is executing according to its description.

Keywords: Verification, model, Micropayment

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1064
5 A Virtual Simulation Environment for a Design and Verification of a GPGPU

Authors: Kwang Y. Lee, Tae R. Park, Jae C. Kwak, Yong S. Koo

Abstract:

When a small H/W IP is designed, we can develop an appropriate verification environment by observing the simulated signal waves, or using the serial test vectors for the fixed output. In the case of design and verification of a massive parallel processor with multiple IPs, it-s difficult to make a verification system with existing common verification environment, and to verify each partial IP. A TestDrive verification environment can build easy and reliable verification system that can produce highly intuitive results by applying Modelsim and SystemVerilog-s DPI. It shows many advantages, for example a high-level design of a GPGPU processor design can be migrate to FPGA board immediately.

Keywords: Verification, GPGPU, Virtual Simulation, IP Design

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1369
4 Verification of Protocol Design using UML - SMV

Authors: Prashanth C.M., K. Chandrashekar Shet

Abstract:

In recent past, the Unified Modeling Language (UML) has become the de facto industry standard for object-oriented modeling of the software systems. The syntax and semantics rich UML has encouraged industry to develop several supporting tools including those capable of generating deployable product (code) from the UML models. As a consequence, ensuring the correctness of the model/design has become challenging and extremely important task. In this paper, we present an approach for automatic verification of protocol model/design. As a case study, Session Initiation Protocol (SIP) design is verified for the property, “the CALLER will not converse with the CALLEE before the connection is established between them ". The SIP is modeled using UML statechart diagrams and the desired properties are expressed in temporal logic. Our prototype verifier “UML-SMV" is used to carry out the verification. We subjected an erroneous SIP model to the UML-SMV, the verifier could successfully detect the error (in 76.26ms) and generate the error trace.

Keywords: Verification, Model checking, unified modeling language, Statechart, Protocol Design

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1426
3 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: Verification, Model checking, Graph Transformation, UML 2.0 Activity, Dynamic Semantics

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1182
2 Biometric Authentication Using Fast Correlation of Near Infrared Hand Vein Patterns

Authors: Mohamed Shahin, Ahmed Badawi, Mohamed Kamel

Abstract:

This paper presents a hand vein authentication system using fast spatial correlation of hand vein patterns. In order to evaluate the system performance, a prototype was designed and a dataset of 50 persons of different ages above 16 and of different gender, each has 10 images per person was acquired at different intervals, 5 images for left hand and 5 images for right hand. In verification testing analysis, we used 3 images to represent the templates and 2 images for testing. Each of the 2 images is matched with the existing 3 templates. FAR of 0.02% and FRR of 3.00 % were reported at threshold 80. The system efficiency at this threshold was found to be 99.95%. The system can operate at a 97% genuine acceptance rate and 99.98 % genuine reject rate, at corresponding threshold of 80. The EER was reported as 0.25 % at threshold 77. We verified that no similarity exists between right and left hand vein patterns for the same person over the acquired dataset sample. Finally, this distinct 100 hand vein patterns dataset sample can be accessed by researchers and students upon request for testing other methods of hand veins matching.

Keywords: Biometrics, Verification, Hand Veins, PatternsSimilarity, Statistical Performance

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3092
1 Global Security Using Human Face Understanding under Vision Ubiquitous Architecture System

Authors: A. Jalal, S. Kim

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: Identification, Recognition, Verification, Ubiquitous architecture

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1063