Abstract
In the context of real-time fault-tolerant architecture, as TTA (Time-Triggered Architecture), the temporal validation of the system behavior is very important. Indeed, the fault-tolerant mechanism execution must respects several temporal constraints. To validate the mechanism behaviors, and to give their maximum execution time (temporal bound), we propose here a temporal validation methodology for TTA. This methodology uses the UPPAAL tool, based on the timed automata and the model-checking analysis. This methodology allows us to extract the temporal bounds of the TTA services.
Chapter PDF
Similar content being viewed by others
Keywords
References
Bauer, G. and Kopetz, H. (2000). Transparent redundancy in the time-triggered architecture. In Int. Conf. on Dependable Systems and Networks (DSN 2000), New York, New York.
Bengtsson, J. and Yi, W. (2004). Timed automata: Semantics, algorithms and tools. Uppsala University.
Bouajjani, A. and Merceron, A. (2002). Parametric verification of a group membership algorithm. In 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume LNCS 2469, pages 311–330, Oldenburg (Germany).
Caspi, P., Curie, A., Maignan, A., Sofronis, C., Tripakis, S., and Niebert, P. (2003). From simulink to scade/lustre to tta: a layered approach for distributed embedded applications. In Proc. of the 2003 ACM SIGPLAN conference on Language, compiler, and tool for embedded systems, pages 153–162. ACM Press.
Blum, I., and Mignotte, A. (2004a). Evaluation of model abstractions for the temporal validation of tta with uppaal. Technical Report RR2004-2, Lab. CITI, INSA Lyon.
Blum, I., and Mignotte, A. (2004b). Sdl and timed petri nets versus uppaal for the validation of embedded architecture in automotive. Technical Report RR2004-1, Lab. CITI, INSA Lyon.
Jensen, H. E., Larsen, K. G., and Skou, A. (1996). Modelling and analysis of a collision avoidance protocol using spin and uppaal. In In Proc. of the 2nd SPIN Workshop, New Jersey, USA. Rutgers University.
Kopetz, H. (1998). The time-triggered architecture. In IEEE Int. Symp. on Object-Oriented Real-Time Distributed Computing (ISORC’98), volume LNCS 2469, Kyoto, Japan.
Larsen, K., Pettersson, P., and Yi, W. (1997). UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1):134–152.
Lindahl, M., Pettersson, P., and Yi, W. (1998). Formal Design and Analysis of a Gear-Box Controller. In Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS. Springer-Verlag.
Lönn, H. and Pettersson, P. (1997). Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, pages 235–242.
Pettersson, P. (1999). Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. Phdthesis-technical report docs 99/101, Department of Computer Systems, Uppsala University.
Pfeifer, H. (2000). Formal verification of the ttp group membership algorithm. In IFIP, Int. Conf. on Formal Description Techniques for Distributed Systems and Communication protocols and Protocol Specification, Testing and Verification, FORTE/PSTV 2000, Pisa, Italy.
Pfeifer, H. (2003). Formal Analysis of Fault-Tolerant Algorithms in the Time-Triggered Architecture. PhD thesis, Universitat Ulm, Germany.
Rushby, J. (2002). An overview of formal verification for the time-triggered architecture. In Damm, W. and Olderog, E.-R., editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, Oldenburg, Germany. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer Science + Business Media, Inc.
About this paper
Cite this paper
Godary, K., Augé-Blum, I., Mignotte, A. (2004). Temporal Bounds for TTA : Validation. In: Kleinjohann, B., Gao, G.R., Kopetz, H., Kleinjohann, L., Rettberg, A. (eds) Design Methods and Applications for Distributed Embedded Systems. DIPES 2004. IFIP International Federation for Information Processing, vol 150. Springer, Boston, MA. https://doi.org/10.1007/1-4020-8149-9_8
Download citation
DOI: https://doi.org/10.1007/1-4020-8149-9_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4020-8148-4
Online ISBN: 978-1-4020-8149-1
eBook Packages: Springer Book Archive