Edward A. Lee

University of California, Berkeley

Stavros Tripakis

University of California, Berkeley

Published in: 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools; Oslo; Norway; October 3

Linköping Electronic Conference Proceedings 47:2, p. 11-21

Published: 2010-09-21

ISBN: 978-91-7519-824-8

ISSN: 1650-3686 (print), 1650-3740 (online)

Ptolemy is an open-source and extensible modeling and simulation framework. It offers heterogeneous modeling capabilities by allowing different models of computation to be composed hierarchically in an arbitrary fashion. This paper describes modal models; which allow to hierarchically compose finite-state machines with other models of computation; both untimed and timed. The semantics of modal models in Ptolemy are defined in a modular manner.

Hierarchy; State machines; Modes; Heterogeneity; Modularity; Modeling; Semantics; Simulation; Cyber-physical systems

[1] Ptolemy II Design Documents. Available at http: //ptolemy.eecs.berkeley.edu/ptolemyII/ designdoc.htm.

[2] R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. ACM Trans. Program. Lang. Syst.; 26(2):339–369; 2004.

[3] R. Alur; S. Kannan; and M. Yannakakis. Communicating hierarchical state machines. In 26th International Colloquium on Automata; Languages; and Programming; volume LNCS 1644; pages 169–178. Springer; 1999.

[4] R. Alur and M. Yannakakis. Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst.; 23(3):273–303; 2001.

[5] C. André. SyncCharts: A visual representation of reactive behaviors. Technical Report RR 95–52; rev. RR (96–56); I3S; April 1996.

[6] C. André. Semantics of S.S.M (Safe State Machine). Technical report; Esterel Technologies; April 2003.

[7] A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non deterministic recursive programs. Fundamenta Informaticae; 11(2):181–205; 1980.

[8] K. Bae; P. Csaba Olveczky; T. H. Feng; E. A. Lee; and S. Tripakis. Verifying Hierarchical Ptolemy II Discrete- Event Models using Real-Time Maude. Technical Report UCB/EECS-2010-50; EECS Department; University of California; Berkeley; May 2010.

[9] C. Baier and M. E. Majster-Cederbaum. Denotational semantics in the CPO and metric approach. Theoretical Computer Science; 135(2):171–220; 1994.

[10] M. von der Beeck. A comparison of Statecharts variants. In H. Langmaack; W. P. de Roever; and J. Vytopil; editors; 3rd Intl. Symp. Formal Techniques in Real-Time and Fault- Tolerant Systems; volume 863 of LNCS; pages 128–148; Lübeck; Germany; 1994. Springer-Verlag.

[11] A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proceedings of the IEEE; 79(9):1270–1282; 1991.

[12] W. Damm; B. Josko; H. Hungar; and A. Pnueli. A Compositional Real-time Semantics of STATEMATE Designs. In Compositionality: The Significant Difference; volume 1536 of LNCS; pages 186–238. Springer; 1998.

[13] D. Dill. Timing assumptions and verification of finitestate concurrent systems. In J. Sifakis; editor; Automatic Verification Methods for Finite State Systems; volume 407 of LNCS; pages 197–212. Springer; 1989.

[14] S. A. Edwards and E. A. Lee. The semantics and execution of a synchronous block-diagram language. Science of Computer Programming; 48(1); 2003.

[15] J. Eker; J. W. Janneck; E. A. Lee; J. Liu; X. Liu; J. Ludvig; S. Neuendorffer; S. Sachs; and Y. Xiong. Taming heterogeneity—the Ptolemy approach. Proceedings of the IEEE; 91(2):127–144; 2003.

[16] R. Eshuis. Reconciling statechart semantics. Sci. Comput. Program.; 74(3):65–99; 2009.

[17] S. Graf; I. Ober; and I. Ober. A real-time profile for UML. Soft. Tools Tech. Transfer; 8(2):113–127; 2006.

[18] Y. Gurevich. Evolving algebras: An attempt to discover semantics. In G. Rozenberg and A. Salomaa; editors; Current Trends in Theoretical Computer Science; pages 266–292. World Scientific; 1993.

[19] N. Halbwachs; P. Caspi; P. Raymond; and D. Pilaud. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE; 79(9):1305–1319; 1991.

[20] G. Hamon. A denotational semantics for stateflow. In EMSOFT ’05: Proceedings of the 5th ACM international conference on Embedded software; pages 164–172; New York; NY; USA; 2005. ACM.

[21] G. Hamon and J. Rushby. An operational semantics for Stateflow. In Fundamental Approaches to Software Engineering (FASE); volume 2984 of LNCS; pages 229– 243; Barcelona; Spain; 2004. Springer.

[22] D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming; 8:231–274; 1987.

[23] E. A. Lee. Modeling concurrent real-time processes using discrete events. Annals of Software Engineering; 7:25–45; 1999.

[24] E. A. Lee. Finite State Machines and Modal Models in Ptolemy II. Technical Report UCB/EECS-2009-151; EECS Department; University of California; Berkeley; Nov 2009.

[25] E. A. Lee. Disciplined heterogeneous modeling. In O. Haugen D.C. Petriu; N. Rouquette; editor; Proceedings of the ACM/IEEE 13th International Conference on Model Driven Engineering; Languages; and Systems (MODELS); pages 273–287. IEEE; October 2010.

[26] E. A. Lee and D. G. Messerschmitt. Synchronous data flow. Proceedings of the IEEE; 75(9):1235–1245; 1987.

[27] E. A. Lee and S. Neuendorffer. Tutorial: Building Ptolemy II Models Graphically. Technical Report UCB/EECS-2007- 129; EECS Department; University of California; Berkeley; Oct 2007.

[28] E. A. Lee and H. Zheng. Operational semantics of hybrid systems. In Manfred Morari and Lothar Thiele; editors; Hybrid Systems: Computation and Control (HSCC); volume LNCS 3414; pages pp. 25–53; Zurich; Switzerland; 2005. Springer-Verlag.

[29] E. A. Lee and H. Zheng. Leveraging synchronous language principles for heterogeneous modeling and design of embedded systems. In EMSOFT; Salzburg; Austria; 2007. ACM.

[30] X. Liu and E. A. Lee. CPO semantics of timed interactive actor networks. Theoretical Computer Science; 409(1):110– 125; 2008.

[31] X. Liu; E. Matsikoudis; and E. A. Lee. Modeling timed concurrent systems. In CONCUR 2006 - Concurrency Theory; volume LNCS 4137; Bonn; Germany; 2006. Springer.

[32] Z. Manna and A. Pnueli. Verifying hybrid systems. Hybrid Systems; pages 4–35; 1992.

[33] G. M. Reed and A. W. Roscoe. Metric spaces as models for real-time concurrency. In 3rd Workshop on Mathematical Foundations of Programming Language Semantics; pages 331–343; London; UK; 1988.

[34] N. Scaife; C. Sofronis; P. Caspi; S. Tripakis; and F. Maraninchi. Defining and Translating a “Safe” Subset of Simulink/Stateflow into Lustre. In Proceedings of the 4th ACM Intl. Conf. on Embedded Software (EMSOFT’04); pages 259–268. ACM; September 2004.

[35] G. Simon; T. Kovácsházy; and G. Péceli. Transient management in reconfigurable systems. In IWSAS’ 2000: Proc. 1st Intl. Workshop on Self-Adaptive Software; pages 90–98; Secaucus; NJ; USA; 2000. Springer.

[36] J. Sztipanovits; D.M. Wilkes; G. Karsai; C. Biegl; and L.E. Lynd. The multigraph and structural adaptivity. IEEE Trans. Signal Proc.; pages 2695–2716; August 1993.

[37] R. K. Yates. Networks of real-time processes. In E. Best; editor; Proc. of the 4th Int. Conf. on Concurrency Theory (CONCUR); volume LNCS 715. Springer-Verlag; 1993.

[38] G. Zhou; M.-K. Leung; and E. A. Lee. A code generation framework for actor-oriented models with partial evaluation. In Y.-H. Lee et al.; editor; Internation Conference on Embedded Software and Systems (ICESS); volume LNCS 4523; pages 786–799; Daegu; Korea; 2007. Springer-Verlag.