Combining Methods for the Livelock Analysis of a Fault-Tolerant System

Author: Bettina Buth, Jan Peleska, Hui Shi

This article presents experiences gained from the verification of communication properties of a large-scale real-world embedded system by means of formal methods. This industrial verification project was performed for a fault-tolerant system designed and implemented by Daimler-Benz Aerospace for the International Space Station ISS and focussd essentially on deadlock and livelock analysis. The approach is based on CSP specifications and the model-checking tool FDR. The tasks are split into manageable subtasks by applying abstraction techniques for restricting the specifications to the essential communication behaviour, modularization according to the process structure, and a set of generic theories developed for the application.

compressed poscript file (100KB)