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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
N. A. Brock and D. M. Jackson: Formal Verification of a Fault Tolerant Computer. In Proceedings of 1992 Digital Avionics Systems Conference. (1992)
B. Buth and J. Peleska: Daimler-Benz Aerospace — Project DMS-R, FTC Development — Verification of Avionics Interface AVI. Technical Report, JP Software-Consulting, (1996).
B. Buth, J. Peleska and H. Shi: Daimler-Benz Aerospace — Project DMS-R, FTC Development — Fault Management Layer (FML): Verification of Deadlock Freedom. Technical Report, JP Software-Consulting, (1996).
Daimler-Benz Aerospace: DMS-R FTC Detailed Design Document Volume 3 (FML Software)
J. Davies: Specification and Proof in Real-Time CSP. Cambridge University Press (1993).
Formal Systemes: Failures Divergence Refinement FDR2 Preliminary Manual. Formal Systems (Europe) Lts (1995).
C. A. R. Hoare: Communicating Sequential Processes. Prentice-Hall Internationaal (1985).
Kolyang, C. Lüth and B. Wolff: Generic Interfaces for Formal Development Support Tools. To appear in Proceedings of the International Workshop for Tool Support in Verification and Validation. LNCS (1997).
L. Lamport, R. Shostak, and M. Pease, The Byzantine Generals Problem, In: ACM Transactions on Programming Languages and Systems, Vol.4, Nr. 3, (1982)
A. W. Roscoe: Model-Checking CSP. In: A Classical Mind, Eassys in Honour of C.A.R. Hoare. Prentice-Hall Internationaal (1994).
A. W. Roscoe: CSP and determinism in security modelling. In: IEEE Symposium of Security and Privacy, (1995).
H. Tej and B. Wolff: A Corrected Failures-Divergence Model for CSP in Isabelle/HOL. To appear in Proceedings of the Formal Methods Europe, LNCS (1997).
B. Krieg-Brückner, J. Peleska, E.-R. Olderog, D. Balzer and A. Baer. Universal Formal Methods Workbench. In U. Grote and G. Wolf, editors, Statusseminar Softwaretechnologie des BMBF, March 1996, Berlin, Deutsche Forschungsanstanlt für Luft-und Raumfahrt, Berlin, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buth, B., Kouvaras, M., Peleska, J., Shi, H. (1997). Deadlock analysis for a fault-tolerant system. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000463
Download citation
DOI: https://doi.org/10.1007/BFb0000463
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63888-9
Online ISBN: 978-3-540-69661-2
eBook Packages: Springer Book Archive