Abstract
Reliable communication among avionic applications is a crucial prerequisite for today’s all-electronic fly-by-wire aircraft technology. The AFDX switched Ethernet has been developed as a scalable, cost-effective network, based upon IEEE 802.3 Ethernet. It uses redundant links to increase the availability. Typical consensus strategies for the redundancy management task are not feasible, as they introduce too heavy delays. In this paper, we formally investigate AFDX redundancy management algorithms, making use of Lamport’s Temporal Logic of Actions (TLA). Furthermore, we present our experiences made with TLA + and the TLA + model checker TLC.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alexander, A.: Komposition Temporallogischer Spezifikationen - Spezifikation und Verifikation von Systemen mit Temporal Logic of Distributed Actions. PhD thesis, Humboldt-Universität zu Berlin (2005)
ARINC Incorporated. Homepage, http://www.arinc.com
Breyer, R., Riley, S.: Switched, Fast and Gigabit Ethernet, 3rd edn. MacMillan Technical Publishing (1999)
Floyd, R.W.: Assigning meaning to programs. In: Proceedings AMS Symposium Applied Mathematics, pp. 19–31 (1967)
Goralski, W.: Introduction to ATM Networking. McGraw-Hill, New York (1995)
Hanxleden, R.V., Gambardella, E.: AFDX Redundancy Management (February 2001)
Lamport, L.: A summary of TLA+. http://research.microsoft.com/users/lamport/tla/tla.html
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16 3, 872–923 (1994)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002), http://research.microsoft.com/users/lamport/tla/book.html
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)
Pnueli, A.: The temporal logic of programs. In: In Proceedings of the 18th Symposium on Foundations of Programming Semantics, pp. 46–57 (1977)
Sinha, P., Suri, N.: On simplifying modular specification and verification of distributed protocols. In: HASE 2001: The 6th IEEE International Symposium on High-Assurance Systems Engineering, pp. 173–181. IEEE Computer Society Press, Washington (2001)
Sommerfeld, L.: Spezifikation eines 20 l-Perfusionsbioreaktor in TLA+. Diploma thesis, Universität Bielefeld (1997)
Tanenbaum, A.S.: Computernetzwerke, 4th edn. Prenctice Hall (2003)
Täubrich, J.: Formal specification and analysis of a redundancy management system with TLA+. Diploma thesis, Christian-Albrechts-Universität zu Kiel, Department of Computer Science (March 2006), http://rtsys.informatik.uni-kiel.de/~biblio/downloads/theses/jat-dt.pdf
US Department of Defense. Aircraft internal time division command/response multiplex data bus (mil-std-1553b). US Department of Defense, 1978-09-21, http://dodssp.daps.dla.mil
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA + specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999), http://link.springer.de/link/service/series/0558/bibs/1703/17030054.htm
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Täubrich, J., von Hanxleden, R. (2007). Formal Specification and Analysis of AFDX Redundancy Management Algorithms. In: Saglietti, F., Oster, N. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2007. Lecture Notes in Computer Science, vol 4680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75101-4_42
Download citation
DOI: https://doi.org/10.1007/978-3-540-75101-4_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75100-7
Online ISBN: 978-3-540-75101-4
eBook Packages: Computer ScienceComputer Science (R0)