Master of Science / Department of Computing and Information Sciences / Mitchell L. Neilsen / 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.
| Identifer | oai:union.ndltd.org:KSU/oai:krex.k-state.edu:2097/914 |
| Date | January 1900 |
| Creators | Mudaliar, Vinodkumar Sekar |
| Publisher | Kansas State University |
| Source Sets | K-State Research Exchange |
| Language | en_US |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.0025 seconds