Advertisement

A Protocol for Loosely Time-Triggered Architectures

  • Albert Benveniste
  • Paul Caspi
  • Paul Le Guernic
  • Hervé Marchand
  • Jean -Pierre Talpin
  • Stavros Tripakis
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)

Abstract

A distributed real-time control system has a time-triggered nature, just because the physical system for control is bound to physics. Loosely Time-Triggered Architectures (LTTA) are a weaker form of the strictly synchronous Time-Triggered Architecture proposed by Kopetz, in which the different periodic clocks are not synchronized, and thus may suffer from relative offset or jitter.

We propose a protocol that ensures a coherent system of logical clocks on the top of LTTA, and we provide several proofs for it, both manual and automatic, based on synchronous languages and associated model checkers. We briefly discuss how this can be used for correct deployment of synchronous designs on an LTTA.

Keywords

Model Checker Virtual Channel Coherent System Periodic Clock Synchronous Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. Alur, T.A. Henzinger, and M.Y. Vardi. Parametric Real-time Reasoning. In Proc. of the 25th Annual Symposium on Theory of Computing (STOC), ACM Press, 1993, pp. 592–601.Google Scholar
  2. 2.
    R. Bannatyne. Time Triggered Protocol: TTP/C, Embedded Systems Programming, 9/98, pp. 52–54.Google Scholar
  3. 3.
    A. Benveniste, B. Caillaud, and P. Le Guernic. From synchrony to asynchrony. In J.C.M. Baeten and S. Mauw, editors, CONCUR’99, Concurrency Theory, 10th International Conference, volume 1664 of Lecture Notes in Computer Science, pages 162–177. Springer, August 1999.CrossRefGoogle Scholar
  4. 4.
    A. Benveniste, B. Caillaud, and P. Le Guernic. Compositionality in dataflow synchronous languages: specification & distributed code generation. Information and Computation, 163, 125–171 (2000).zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    A. Benveniste. Some synchronization issues when designing embedded systems from components. In Proc. of 1st Int. Workshop on Embedded Software, EMSOFT’01, T.A. Henzinger and C.M. Kirsch Eds., LNCS 2211, 32–49, Springer Verlag, 2001.Google Scholar
  6. 6.
    P. Caspi, C. Mazuet, R. Salem, and D. Weber. Formal design of distributed control systems with lustre. In Proc. Safecomp’99, September 1999.Google Scholar
  7. 7.
    P. Caspi. Embedded control: from asynchrony to synchrony and back. In Proc. of 1st Int. Workshop on Embedded Software, EMSOFT’01, T.A. Henzinger and C.M. Kirsch Eds., LNCS 2211, 80–96, Springer Verlag, 2001.Google Scholar
  8. 8.
    C Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Proceedings of ”Hybrid Systems III, Verification and Control”, 1996. Lecture Notes in Computer Science 1066, Springer-Verlag.Google Scholar
  9. 9.
    P. Le Guernic, T. Gautier, M. Le Borgne, C. Le Maire. Programming Real-Time Applications with Signal. Proceedings of the IEEE, 79(9):1321–1336, September 1991.Google Scholar
  10. 10.
    N. Halbwachs, F. Lagnier and P. Raymond. Synchronous observers and the verification of reactive systems. In Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST’93, Twente, M. Nivat and C Rattray and T. Rus and G. Scollo, Eds., Workshops in Computing, Springer Verlag. Jun. 1993.Google Scholar
  11. 11.
    H. Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications. Kluwer Academic Publishers. 1997. ISBN 0-7923-9894-7.Google Scholar
  12. 12.
    L. Lamport. Time, clocks and the ordering of events in a distributed system. Communication of the ACM, 21:558–565, 1978.zbMATHCrossRefGoogle Scholar
  13. 13.
    Kim G. Larsen, P. Pettersson, and Wang Yi. UPPAAL in a Nutshell. In Springer International Journal of Software Tools for Technology Transfer, 1(1–2), 134–152, Dec. 1997.Google Scholar
  14. 14.
    H. Marchand, E. Rutten, M. Le Borgne, M. Samaan. Formal Verification of SIGNAL programs: Application to a Power Transformer Station Controller. Science of Computer Programming, 41(1):85–104, Aug. 2001.Google Scholar
  15. 15.
    M. Pease, R.E. Shostak, and L. Lamport. Reaching agreement in the presence of faults. Journal of the ACM, 27(2):228–237, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    J. Rushby. Bus architectures for safety-critical embedded systems. In Proc. of 1st Int. Workshop on Embedded Software, EMSOFT’01, T.A. Henzinger and C.M. Kirsch Eds., LNCS 2211, 306–323, Springer Verlag, 2001.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Albert Benveniste
    • 1
  • Paul Caspi
    • 2
  • Paul Le Guernic
    • 1
  • Hervé Marchand
    • 1
  • Jean -Pierre Talpin
    • 1
  • Stavros Tripakis
    • 2
  1. 1.Irisa/InriaRennesFrance
  2. 2.Verimag, Centre EquationGieres

Personalised recommendations