Composing heterogeneous reactive systems

ABSTRACT

We present a compositional theory of heterogeneous reactive systems. The approach is based on the concept of tags marking the events of the signals of a system. Tags can be used for multiple purposes from indexing evolution in time (time stamping) to expressing relations among signals, like coordination (e.g., synchrony and asynchrony) and causal dependencies. The theory provides flexibility in system modeling because it can be used both as a unifying mathematical framework to relate heterogeneous models of computations and as a formal vehicle to implement complex systems by combining heterogeneous components. In particular, we introduce an algebra of tag structures to define heterogeneous parallel composition formally. Morphisms between tag structures are used to define relationships between heterogeneous models at different levels of abstraction. In particular, they can be used to represent design transformations from tightly synchronized specifications to loosely-synchronized implementations. The theory has an important application in the correct-by-construction deployment of synchronous design on distributed architectures.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999 [doi>10.1023/A:1008739929481]
• 2: Alur, R., Dang, T., Esposito, J., Hur, Y., Ivancic, F., Kumar, V., Lee, I., Mishra, P., Pappas, G. J., and Sokolsky, O. 2003. Hierarchical modeling and analysis of embedded systems. Proc. IEEE 91, 1, 11--28.
• 3: Felice Balarin , Yosinori Watanabe , Harry Hsieh , Luciano Lavagno , Claudio Passerone , Alberto Sangiovanni-Vincentelli, Metropolis: An Integrated Electronic System Design Environment, Computer, v.36 n.4, p.45-52, April 2003 [doi>10.1109/MC.2003.1193228]
• 4: Albert Benveniste , Benoît Caillaud , Paul Le Guernic, From Synchrony to Asynchrony, Proceedings of the 10th International Conference on Concurrency Theory, p.162-177, August 24-27, 1999
• 5: Albert Benveniste , Benoˆt Caillaud , Paul Le Guernic, Compositionality in dataflow synchronous languages: specification and distributed code generation 1,2,3, Information and Computation, v.163 n.1, p.125-171, Nov. 25, 2000 [doi>10.1006/inco.2000.9999]
• 6: Albert Benveniste , Paul Caspi , Paul Le Guernic , Hervé Marchand , Jean-Pierre Talpin , Stavros Tripakis, A Protocol for Loosely Time-Triggered Architectures, Proceedings of the Second International Conference on Embedded Software, p.252-265, October 07-09, 2002
• 7: Benveniste, A., Carloni, L. P., Caspi, P., and Sangiovanni-Vincentelli, A. L. 2003. Heterogeneous reactive systems modeling and correct-by-construction deployment. In Proceedings of the 3rd International Conference on Embedded Software (EMSOFT'03). Lecture Notes in Computer Science, vol. 2855, Springer, Berlin.
• 8: Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., and de Simone, R. 2003. The synchronous language twelve years later. Proc. IEEE 91, 1, 64--83.
• 9: Berry, G. 2000. The Foundations of Esterel. MIT Press, Cambridge, MA.
• 10: Jerry Burch , Roberto Passerone , Alberto L. Sangiovanni-Vincentelli, Overcoming Heterophobia: Modeling Concurrency in Heterogeneous Systems, Proceedings of the Second International Conference on Application of Concurrency to System Design, p.13, June 25-29, 2001
• 11: Giorgio C. Buttazzo, Scalable Applications for Energy-Aware Processors, Proceedings of the Second International Conference on Embedded Software, p.153-165, October 07-09, 2002
• 12: Carloni, L. P., McMillan, K. L., and Sangiovanni-Vincentelli, A. L. 2001. Theory of latency-insensitive design. IEEE Trans. Comput.-Aid. Design Integr. Circuits Syst. 20, 9, 1059--1076.
• 13: Paul Caspi, Embedded Control: From Asynchrony to Synchrony and Back, Proceedings of the First International Workshop on Embedded Software, p.80-96, October 08-10, 2001
• 14: Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , Freddy Y. C. Mang, Synchronous and Bidirectional Component Interfaces, Proceedings of the 14th International Conference on Computer Aided Verification, p.414-427, July 27-31, 2002
• 15: Cortadella, J., Kondratyev, A., Lavagno, L., and Sotiriou, C. 2003. A concurrent model for de-synchronization. In Proceedings of the International Workshop on Logic Synthesis.
• 16: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 17: Luca de Alfaro , Thomas A. Henzinger, Interface Theories for Component-Based Design, Proceedings of the First International Workshop on Embedded Software, p.148-165, October 08-10, 2001
• 18: Eker, J., Janneck, J. W., Lee, E. A., Liu, J., Ludwig, J., Neuendorffer, S., Sachs, S., and Xiong, Y. 2003. Taming heterogeneity—The Ptolemy approach. Proc. IEEE, 91, 1, 127--144. http://ptolemy.eecs.berkeley.edu/ptolemyII/
• 19: Halbwachs, N., Caspi, P., Raymond, P., and Pilaud, D. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9, 1305--1320.
• 20: Karsai, G., Sztipanovits, J., Ledeczi, A., and Bapty, T. 2003. Model-integrated development of embedded software. Proc. IEEE 91, 1, 127--144.
• 21: Hermann Kopetz, Real-Time Systems: Design Principles for Distributed Embedded Applications, Kluwer Academic Publishers, Norwell, MA, 1997
• 22: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 23: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 24: Le Guernic, P., Gautier, T., Le Borgne, M., and Le Maire, C. 1991. Programming real-time applications with SIGNAL. Proc. IEEE 79, 9, 1326--1333.
• 25: Le Guernic, P., Talpin, J.-P., and Le Lann, J.-C. 2003. Polychrony for system design. J. Circuits Syst. Comput.
• 26: Lee, E. A. and Sangiovanni-Vincentelli, A. 1998. A framework for comparing models of computation. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 17, 12, 1217--1229.
• 27: Edward A. Lee , Yuhong Xiong, System-Level Types for Component-Based Design, Proceedings of the First International Workshop on Embedded Software, p.237-253, October 08-10, 2001
• 28: Mattern, F. 1989. Virtual time and global states of distributed systems. In Proceedings of the International Workshop on Parallel & Distributed Algorithms. M. Cosnard et al. Eds., Elsevier Science, Berlin, 215--226.
• 29: Mathaikutty, D., Patel, H., and Shukla, S. 2004. A functional programming framework of heterogeneous model of computations for system design. In Proceedings of the Forum on Specification and Design Languages (FDL).
• 30: Mathaikutty, D., Patel, H., Shukla, S., and Jantsch, A. 2005. UMoC++: A C++ -based multi-MoC modeling environment. In Advances in Design and Specification Languages for SoCs—Selected Contributions from FDL'05, A. Vachoux, Ed. Chapter 7. Springer, Berlin.
• 31: Concurrency in Synchronous Systems, Proceedings of the Fourth International Conference on Application of Concurrency to System Design, p.67, June 16-18, 2004
• 32: Dumitru Potop-Butucaru , Benoit Caillaud, Correct-by-Construction Asynchronous Implementation of Modular Synchronous Specifications, Proceedings of the Fifth International Conference on Application of Concurrency to System Design, p.48-57, June 07-09, 2005 [doi>10.1109/ACSD.2005.10]
• 33: Sander, I. and Jantsch, A. 2004. System modeling and transformational design refinement in ForSyDe, IEEE Trans. Comput. Aided Design Integr. Circuits Syst. 23, 1, 17--32.
• 34: Glynn Winskel, Event Structure Semantics for CCS and Related Languages, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.561-576, July 12-16, 1982

INDEX TERMS

Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Interactive and reactive computation

General Terms:
Design, Theory

Keywords:
Compositionality, GALS, correct-by-construction design, models of computation, reactive systems