Deadlock Analysis for a Fault Management Layer
(Industrial Usage Report)
Author: Bettina Buth, Michel Kouvaras, Jan Peleska, Hui Shi
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)