Dissertation > Excellent graduate degree dissertation topics show

Verification of ATM Fabric’s Behavior Using SPIN

Author: WuXiaoJun
Tutor: LiLian
School: Lanzhou University
Course: Computer Software and Theory
Keywords: formal methods liveness property safety property SPIN Model Checker Promela language BDD ROBDD
CLC: TN915.2
Type: Master's thesis
Year: 2006
Downloads: 85
Quote: 0
Read: Download Dissertation

Abstract


In recent years, Model checking has emerged as an alternative approach to ensuring the quality and correctness of hardware design, overcoming some of the limitations of traditional validation techniques such as simulation and testing. Because exhaustive testing for nontrivial designs is generally infeasible, testing provides at best only a probabilistic assurance. There are two main aspects to the application of model checking in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and corresponding implementation. Model checking uses rigorous mathematical reasoning to show that a design meets all or parts of specification. Typically, the user provides a high level representation of the model and the specification to be checked. The model checker will either terminate with the answer true, indicating that the model satisfies the specification, or give a counterexample execution that shows why the formula is not satisfied.This paper give a brief introduction of formal methods at first, then mainly introduce the theory and concepts of Model Checking (including CTL~*, CTL, LTL, Kripe structure etc.) and I introduced the Model Checker named SPIN and the language PROMELA accepted by SPIN.At last I investigated hardware implementation of Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric’s high-level behavioral specification which has no restrictions with respect to cell length or word width. The verification is based on the model created by PROMELA. PROMELA is a language accepted by SPIN that is a famous Model Checker. The verification is based on the reachability analysis of the product machine of the implementation and the specification. I verified some LTL properties (including liveness property and safety property) of the ATM Fairisle Switch using by SPIN.

Related Dissertations

  1. Timed automata model - based verification techniques,TP301.1
  2. New Progress of Symbolic Simulator Applications on CMOS Analog Circuit Design Automation,TN432
  3. The Theory and Effect of Formal Method,B812
  4. A Formal Analysis Method and Its Application Based on UML Requirement Modeling,TP311.52
  5. Investigation of Electrochemical Biosensor Based on Boron-Doped Diamond and Newly Nanocomposites,TP212.3
  6. The Research of Test Generation Method for Combinational Circuits Based on Binary Decision Diagrams,TP391.7
  7. A Heuristic Algorithm for Model-Checking Based on Counter Example Finding,TP311.52
  8. Vertification of OSPF Protocol Based on Coloured Petri Net,TP301.6
  9. Research on Tool of Generating Test Cases Automatically from Model on Requirement,TP311.52
  10. Formal Modeling and Verification for Component-Based Model Integrated CNC Systems with IEC 61499 Standard,TP311.52
  11. Analysis and Research on Critical Non-functional Property of Safety-Critical Embedded Real-Time Software,TP368.1
  12. Research on Key Techniques for Software Transactional Memory Parallel Programming Environment,TP311.1
  13. Key Techniques of Trustworthiness Improvement on Hybird Arithmetic Addition of Floating-point Fused Multiply-add Unit,TP302.1
  14. A Study on Formally Modeling and Verifying the Composition of Web Services,TP393.09
  15. Model Oriented Composition Theory,TP311.52
  16. The Formal Modelling and Model Checking Research of Rail Transportation Train Control System,U284.48
  17. Slicing Execution for Verification of C Programs,TP312.1
  18. Detecting and Handling the Inconsistency in Viewpoints Requirement Engineering,TP311.52
  19. Analysis of Aspect-Oriented Technology and Its Application in the Development of Software for Large-Scale Embedded System,TP311.52
  20. Research on the Foundamentals of Compilation Correctness and Safety,TP314
  21. Synthetic Research on Imperfect Coverage, Phased-Mission Systems, and Static and Dynamic Fault Trees,TP18

CLC: > Industrial Technology > Radio electronics, telecommunications technology > Communicate > Communication network > ATM (asynchronous transfer mode ) network
© 2012 www.DissertationTopic.Net  Mobile