Heterogeneous reactive systems modeling: capturing causality and the correctness of loosely time-triggered architectures (LTTA)

ABSTRACT

We present an extension of a mathematical framework proposed by the authors to deal with the composition of heterogeneous reactive systems. Our extended framework encompasses diverse models of computation and communication such as synchronous, asynchronous, causality-based partial orders, and earliest execution times. We introduce an algebra of tag structures and morphisms between tag sets to define heterogeneous parallel composition formally and we use a result on pullbacks from category theory to handle properly the case of systems derived by composing many heterogeneous components. The extended framework allows us to establish theorems, from which design techniques for correct-by-construction deployment of abstract specifications can be derived. We illustrate this by providing a complete formal support for correct-by-construction distributed deployment of a synchronous design specification over an ltta medium.

References

1. R. Alur, T. Dang, J. Esposito, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. J. Pappas and O. Sokolsky. Hierarchical Modeling and Analysis of Embedded Systems. Proc. of the IEEE, 91(1), 11--28, Jan. 2003.]]
2. A. Benveniste, B. Caillaud, and P. Le Guernic. From synchrony to asynchrony. In J.C.M. Baeten and S. Mauw, Eds., CONCUR'99, Concurrency Theory, 10th Intl. Conference, LNCS 1664, pages 162--177. Springer, 1999.]]
3. A. Benveniste, B. Caillaud, and P. Le Guernic. Compositionality in dataflow synchronous languages: specification & distributed code generation. Information and Computation, 163, 125--171 (2000).]]
4. A. Benveniste, B. Caillaud, L. P. Carloni, P. Caspi, and A. L. Sangiovanni-Vincentelli. Composing Heterogeneous Reactive Systems. Submitted to ACM Transactions in Embedded Computing Systems.]]
5. A. Benveniste, L. P. Carloni, P. Caspi, and A. L. Sangiovanni-Vincentelli. Heterogeneous reactive systems modeling and correct-by-construction deployment. In R. Alur and I. Lee, Eds., Proc. of the 3rd. Intl. Conf. on Embedded Software, EMSOFT'03, LNCS 2855, Springer, 2003.]]
6. A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J-P. Talpin and S. Tripakis. A Protocol for Loosely Time-Triggered Architectures. In A. Sangiovanni-Vincentelli and J. Sifakis Eds., Proc. of the 2nd Intl. Workshop, EMSOFT 2002, LNCS vol. 2491, 252--265, Springer, 2002.]]
7. G. Buttazzo. Scalable Applications for Energy-Aware Processors. In A. Sangiovanni-Vincentelli and J. Sifakis Eds., Proc. of the 2nd Intl. Workshop, EMSOFT'02, LNCS vol. 2491, 153-165, Springer, 2002.]]
8. P. Caspi. Embedded control: from asynchrony to synchrony and back. In T.A. Henzinger and C.M. Kirsch Eds., Proc. of 1st Int. Workshop on Embedded Software, EMSOFT'01, LNCS 2211, 80--96, Springer, 2001.]]
9. J. Eker, J.W. Janneck, E.A. Lee, J. Liu, J. Ludwig, S. Neuendorffer, S. Sachs, and Y. Xiong. Taming heterogeneity---The Ptolemy approach. Proc. of the IEEE, 91(1), 127--144, Jan. 2003.]]
10. L. de Alfaro and T.A. Henzinger. Interface Theories for Component-Based Design. In T.A. Henzinger and C.M. Kirsch Eds., Proc. of 1st Int. Workshop on Embedded Software, EMSOFT'01, LNCS 2211, Springer, 2001.]]
11. R. Goldblatt.phTopoi, the categorical analysis of logic. Studies in logic and the foundations of mathematics, Vol. 98, North-Holland, 1984.]]
12. E.A. Lee and Y. Xiong. System-Level Types for Component-Based Design. In T.A. Henzinger and C.M. Kirsch Eds., Proc. of 1st Int. Workshop on Embedded Software, EMSOFT'01, LNCS 2211, Springer, 2001.]]
13. G. Karsai, J. Sztipanovits, A. Ledeczi, and T. Bapty. Model-Integrated Development of Embedded Software. Proc. of the IEEE, 91(1), 127--144, Jan. 2003.]]
14. H. Kopetz. Real-Time Systems: Design Principles for Distributed Embedded Applications. Kluwer Academic Publishers. 1997. ISBN 0-7923-9894-7.]]
15. E.A. Lee and A. Sangiovanni-Vincentelli. A Framework for Comparing Models of Computation. phIEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 17(12), 1217--1229, Dec. 1998.]]
16. D. Potop-Butucaru, B. Caillaud and A. Benveniste. Concurrency in Synchronous Systems. InphProc. of the 4th Int. Conf. on Applications of Concurrency in System Design (ACSD), Hamilton, Canada, June 2004.]]

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

  • Real-time systems