Verification of FlexRay membership protocol using UPPAAL

by Mudaliar, Vinodkumar Sekar

Abstract (Summary)
Safety-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.

Bibliographical Information:


School:Kansas State University

School Location:USA - Kansas

Source Type:Master's Thesis

Keywords:flexray membership algorithm uppaal fault detection computer science 0984


Date of Publication:01/01/2008

© 2009 All Rights Reserved.