Verification of FlexRay membership protocol using UPPAAL

dc.contributor.authorMudaliar, Vinodkumar Sekar
dc.date.accessioned2008-08-12T15:42:15Z
dc.date.available2008-08-12T15:42:15Z
dc.date.graduationmonthAugusten
dc.date.issued2008-08-12T15:42:15Z
dc.date.published2008en
dc.description.abstractSafety-critical systems embedded in avionics and automotive systems are becoming increasing complex. Components with different requirements typically share a common distributed platform for communication. To accommodate varied requirements, many of these distributed real-time systems use FlexRay communication network. FlexRay supports both time triggered and event-triggered communications. In such systems, it is vital to establish a consistent view of all the associated processes to handle fault-tolerance. This task can be accomplished through the use of a Process Group Membership Protocol. This protocol must provide a high level of assurance that it operates correctly. In this thesis, we provide for the verification of one such protocol using Model Checking. Through this verification, we found that the protocol may remove nodes from the group of operational nodes in the communicating network at a fast rate. This may lead to exhaustion of the system resources by the protocol, hampering system performance. We determine allowable rates of failure that do not hamper system performance.en
dc.description.advisorMitchell L. Neilsenen
dc.description.degreeMaster of Scienceen
dc.description.departmentDepartment of Computing and Information Sciencesen
dc.description.levelMastersen
dc.identifier.urihttp://hdl.handle.net/2097/914
dc.language.isoen_USen
dc.publisherKansas State Universityen
dc.subjectFlexRayen
dc.subjectMembership Algorithmen
dc.subjectUPPAALen
dc.subjectFault Detectionen
dc.subject.umiComputer Science (0984)en
dc.titleVerification of FlexRay membership protocol using UPPAALen
dc.typeThesisen

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
VinodkumarMudaliar2008.pdf
Size:
856.97 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.69 KB
Format:
Item-specific license agreed upon to submission
Description: