Deadlock Analysis for a Fault Management Layer (Industrial Usage Report)

Author: Bettina Buth, Michel Kouvaras, Jan Peleska, Hui Shi

Abstract:
This article presents an approach for the verification of communication properties in large-scale real-world embedded systems by means of formal methods. It is illustrated by examples and results obtained during an industrial verification project performed for a fault-tolerant system designed and implemented by Daimler-Benz Aerospace for the International Space Station ISS. The approach is based on CSP specifications and the model-checking tool FDR. The task is split into manageable subtasks by applying an abstraction technique 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 (97KB)