• Admin
    UC Research Repository
    View Item 
       
    • UC Home
    • Library
    • UC Research Repository
    • College of Engineering
    • Engineering: Theses and Dissertations
    • View Item
       
    • UC Home
    • Library
    • UC Research Repository
    • College of Engineering
    • Engineering: Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Browse

    All of the RepositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    Statistics

    View Usage Statistics

    Model Checking Time Triggered CAN Protocols

    Thumbnail
    View/Open
    thesis_fulltext.pdf (1.607Mb)
    Author
    Keating, Daniel
    Date
    2011
    Permanent Link
    http://hdl.handle.net/10092/5754
    Thesis Discipline
    Electrical Engineering
    Degree Grantor
    University of Canterbury
    Degree Level
    Masters
    Degree Name
    Master of Engineering

    Model checking is used to aid in the design and verification of complex concurrent systems. An abstracted finite state model of a system and a set of mathematically based correctness properties based on the design specifications are defined. The model checker then performs an exhaustive state space search of the model, checking that the correctness properties hold at each step. This thesis describes how the SPIN model checker has been used to find and correct problems in the software design of a distributed marine vessel control system currently under development at a control systems specialist in New Zealand. The system under development is a mission critical control system used on large marine vessels. Hence, the requirement to study its architecture and verify the implementation of the system. The model checking work reported here focused on analysing the implementation of the Time-Triggered Controller-Area-Network (TTCAN) protocol, as this is used as the backbone for communications between devices and thus is a crucial part of their control system.

    A model of the ISO TTCAN protocol has been created using the SPIN model checker. This was based on work previously done by Leen and Heffernan modelling the protocol with the UPPAAL model checker [Leen and Heffernan 2002a]. In the process of building the ISO TTCAN model, a set of general techniques were developed for model checking TTCAN-like protocols. The techniques developed include modelling the progression of time efficiently in SPIN, TTCAN message transmission, TTCAN error handling, and CAN bus arbitration. These techniques then form the basis of a set of models developed to check the sponsoring organisation’s implementation of TTCAN as well as the fault tolerance schemes added to the system. Descriptions of the models and properties developed to check the correctness of the TTCAN implementation are given, and verification results are presented and discussed. This application of model checking to an industrial design problem has been successful in identifying a number of potential issues early in the design phase. In cases where problems are identified, the sequences of events leading to the problems are described, and potential solutions are suggested and modelled to check their effect of the system.

    Subjects
    TTCAN
     
    CAN
     
    model checking
     
    SPIN
    Collections
    • Engineering: Theses and Dissertations [2155]
    Rights
    http://library.canterbury.ac.nz/thesis/etheses_copyright.shtml

    UC Research Repository
    University Library
    University of Canterbury
    Private Bag 4800
    Christchurch 8140

    Phone
    364 2987 ext 8718

    Email
    ucresearchrepository@canterbury.ac.nz

    Follow us
    FacebookTwitterYoutube

    © University of Canterbury Library
    Send Feedback | Contact Us