Abstract
We present a modular formal analysis of the communication properties of the Time-Triggered Protocol TTP/C based on the guardian approach. The guardian is an independent component that employs static knowledge about the system to transform arbitrary node failures into failure modes that are covered by the rather optimistic fault hypothesis of TTP/C. Through a hierarchy of formal models, we give a precise description of the arguments that support the desired correctness properties of TTP/C. First, requirements for correct communication are expressed on an abstract level. By stepwise refinement we show that the abstract requirements are met under the optimistic fault hypothesis, and how the guardian model allows a broader class of failures be tolerated.
This research was supported by the European Commission under the IST project NEXT TTA (IST-2001-32111).
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
Kopetz, H.: The Time-Triggered Approach to Real-Time System Design. In: Predictably Dependable Computing Systems. Springer, Heidelberg (1995)
Kopetz, H.: The Time-Triggered Architecture. In: Proc. 1st Intl. Symp. on Object-Oriented Real-Time Distributed Computing, pp. 22–31 (1998)
Kopetz, H., Bauer, G.: The Time-Triggered Architecture. Proceedings of the IEEE 91, 112–126 (2003)
Heiner, G., Thurner, T.: Time-Triggered Architecture for Safety-Related Distributed Real-Time Systems in Transportation Systems. In: Proc. 28th Intl. Symp. on Fault-Tolerant Computing. IEEE Computer Society, Los Alamitos (1998)
Bauer, G., Kopetz, H., Steiner, W.: Byzantine Fault Containment in TTP/C. In: Proc. Intl. Workshop on Real-Time LANs in the Internet Age, pp. 13–16 (2002)
Bauer, G., Kopetz, H., Steiner, W.: The Central Guardian Approach to Enforce Fault Isolation in the Time-Triggered Architecture. In: Proc. 6th Intl. Symp. on Autonomous Decentralized Systems, pp. 37–44 (2003)
Pfeifer, H., Schwier, D., von Henke, F.: Formal Verification for Time-Triggered Clock Synchronization. In: Proc. of Dependable Computing for Critical Applications, vol. 7, pp. 207–226. IEEE Computer Society, Los Alamitos (1999)
Katz, S., Lincoln, P., Rushby, J.: Low-Overhead Time-Triggered Group Membership. In: Mavronicolas, M. (ed.) WDAG 1997. LNCS, vol. 1320, pp. 155–169. Springer, Heidelberg (1997)
Pfeifer, H.: Formal Verification of the TTP Group Membership Algorithm. In: Proc. of FORTE XIII / PSTV XX, pp. 3–18. Kluwer Academic Publishers, Dordrecht (2000)
Bouajjani, A., Merceron, A.: Parametric Verification of a Group Membership Algorithm. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 311–330. Springer, Heidelberg (2002)
Merceron, A., Müllerburg, M., Pinna, G.: Verifying a Time-Triggered Protocol in a Multi-Language Environment. In: Ehrenberger, W. (ed.) SAFECOMP 1998. LNCS, vol. 1516, pp. 185–195. Springer, Heidelberg (1998)
Steiner, W., Rushby, J., Sorea, M., Pfeifer, H.: Model Checking a Fault-Tolerant Startup Algorithm: From Design Exploration To Exhaustive Fault Simulation. In: Proc. Conf. on Dependable Systems and Networks. IEEE Computer Society, Los Alamitos (2004)
Rushby, J.: An Overview of Formal Verification for the Time-Triggered Architecture. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 83–105. Springer, Heidelberg (2002)
Rushby, J.: Systematic Formal Verification for Fault-Tolerant Time-Triggered Algorithms. IEEE Trans. on Software Engineering 25, 651–660 (1999)
Owre, S., Rushby, J., Shankar, N., Stringer-Calvert, D.: PVS: An Experience Report. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 338–345. Springer, Heidelberg (1999)
Bauer, G., Kopetz, H., Puschner, P.: Assumption Coverage under Different Failure Modes in the Time-Triggered Architecture. In: Proc. 8th IEEE Intl. Conf. on Emerging Technologies and Factory Automation, pp. 333–341 (2001)
TTTech: Time-Triggered Protocol TTP/C High-Level Specification Document (2003), available at: http://www.tttech.com/technology/specification.html
Kopetz, H.: The Time-Triggered (TT) Model of Computation. In: Proc. 19th IEEE Real-Time Systems Symposium, pp. 168–177 (1998)
Pfeifer, H., von Henke, F.: Modular Formal Analysis of the Central Guardian in the Time-Triggered Architecture. Technical report, Fakultät für Informatik, Universität Ulm, Germany (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pfeifer, H., von Henke, F.W. (2004). Modular Formal Analysis of the Central Guardian in the Time-Triggered Architecture. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2004. Lecture Notes in Computer Science, vol 3219. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30138-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-30138-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23176-9
Online ISBN: 978-3-540-30138-7
eBook Packages: Springer Book Archive