Hostname: page-component-8448b6f56d-xtgtn Total loading time: 0 Render date: 2024-04-18T13:55:30.556Z Has data issue: false hasContentIssue false
  • English
  • Français

A modular formal semantics for Ptolemy†

Published online by Cambridge University Press:  08 July 2013

STAVROS TRIPAKIS ,
CHRISTOS STERGIOU ,
CHRIS SHAVER  and
EDWARD A. LEE
STAVROS TRIPAKIS
Affiliation:
University of California, Berkeley, California, U.S.A. Email: stavros@eecs.berkeley.edu; chster@eecs.berkeley.edu; shaver@eecs.berkeley.edu; eal@eecs.berkeley.edu
CHRISTOS STERGIOU
Affiliation:
University of California, Berkeley, California, U.S.A. Email: stavros@eecs.berkeley.edu; chster@eecs.berkeley.edu; shaver@eecs.berkeley.edu; eal@eecs.berkeley.edu
CHRIS SHAVER
Affiliation:
University of California, Berkeley, California, U.S.A. Email: stavros@eecs.berkeley.edu; chster@eecs.berkeley.edu; shaver@eecs.berkeley.edu; eal@eecs.berkeley.edu
EDWARD A. LEE
Affiliation:
University of California, Berkeley, California, U.S.A. Email: stavros@eecs.berkeley.edu; chster@eecs.berkeley.edu; shaver@eecs.berkeley.edu; eal@eecs.berkeley.edu
Get access Rights & Permissions [Opens in a new window]

Abstract

Ptolemy‡ is an open-source and extensible modelling and simulation framework. It offers heterogeneous modeling capabilities by allowing different models of computation, both untimed and timed, to be composed hierarchically in an arbitrary fashion. This paper proposes a formal semantics for Ptolemy that is modular in the sense that atomic actors and their compositions are treated in a unified way. In particular, all actors conform to an executable interface that contains four functions: fire (produce outputs given current state and inputs); postfire (update state instantaneously); deadline (how much time the actor is willing to let elapse); and time-update (update the state with the passage of time). Composite actors are obtained using composition operators that in Ptolemy are called directors. Different directors realise different models of computation. In this paper, we formally define the directors for the following models of computation: synchronous- reactive, discrete event, continuous time, process networks and modal models.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Special Issue 4: Lightweight and Practical Formal Methods in the Design and Analysis of Safety-Critical Systems , August 2013 , pp. 834 - 881
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This work was partially supported by NSF project ExCAPE: Expeditions in Computer Augmented Program Engineering, and by the Center for Hybrid and Embedded Software Systems (CHESS) at UC Berkeley, which receives support from the National Science Foundation (NSF awards #0720882 (CSR-EHS: PRET) and #0931843 (ActionWebs), the U.S. Army Research Office (ARO #W911NF-11-2-0038), the Air Force Research Lab (AFRL), the Multiscale Systems Center (MuSyC) (which is one of six research centres funded under the Focus Center Research Program), a Semiconductor Research Corporation program and the following companies: Bosch, National Instruments, Thales and Toyota.

References

Aiguier, M., Golden, B. and Krob, D. (2011) Modeling of Complex Systems II: A minimalist and unified semantics for heterogeneous integrated systems. Applied Mathematics and Computation. 218 (16)8039–8055.Google Scholar
Alur, R.et al. (1995) The algorithmic analysis of hybrid systems. Theoretical Computer Science 138 3–34.CrossRefGoogle Scholar
Alur, R. and Dill, D. L. (1994) A theory of timed automata. Theoretical Computer Science 126 (2)183–235.CrossRefGoogle Scholar
André, C. (1996) SyncCharts: A visual representation of reactive behaviors. Technical Report RR 95–52, rev. RR (96–56), I3S.Google Scholar
André, C. (2003) Semantics of S.S.M (Safe State Machine). Technical report, Esterel Technologies.Google Scholar
Arbab, F. (2004) Reo: A channel-based coordination model for component composition. Mathematical Structures in Computer Science 14 (3)329–366.CrossRefGoogle Scholar
Arnold, A. and Nivat, M. (1980) Metric interpretations of infinite trees and semantics of non-deterministic recursive programs. Fundamenta Informaticae 11 (2)181–205.Google Scholar
Bae, K., Csaba Ölveczky, P., Feng, T. H., Lee, E. A. and Tripakis, S. (2012) Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude. Science of Computer Programming 77 (12)1235–1271.CrossRefGoogle Scholar
Baier, C. and Majster-Cederbaum, M. E. (1994) Denotational semantics in the CPO and metric approach. Theoretical Computer Science 135 (2)171–220.CrossRefGoogle Scholar
Balarin, F., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A. L. and Watanabe, Y. (2003) Metropolis: an integrated electronic system design environment. Computer 36 (4).CrossRefGoogle Scholar
Basu, A., Bozga, M. and Sifakis, J. (2006) Modeling heterogeneous real-time components in BIP. In: International Conference on Software Engineering and Formal Methods (SEFM 06), IEEE Computer Society 3–12.CrossRefGoogle Scholar
von der Beeck, M. (1994) A comparison of Statecharts variants. In: Langmaack, H., de Roever, W. P. and Vytopil, J. (eds.) 3rd International Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer-Verlag Lecture Notes in Computer Science 863 128–148.CrossRefGoogle Scholar
Benveniste, A. and Berry, G. (1991) The synchronous approach to reactive and real-time systems. Proceedings of the IEEE 79 (9)1270–1282.CrossRefGoogle Scholar
Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P. and de Simone, R. (2003) The synchronous languages 12 years later. Proceedings of the IEEE 91 (1)64–83.CrossRefGoogle Scholar
Benveniste, A., Caspi, P., Lublinerman, R. and Tripakis, S. (2009) Actors without directors: a Kahnian view of heterogeneous systems. In: Majumdar, R. and Tabuada, P. (eds.) Hybrid Systems: Computation and Control – 12th International Conference, HSCC 2009. Springer-Verlag Lecture Notes in Computer Science 5469 46–60.Google Scholar
Berry, G. (1996) The Constructive Semantics of Pure Esterel (book draft).Google Scholar
Bliudze, S. and Krob, D. (2009) Modelling of complex systems: Systems as dataflow machines. Fundamenta Informaticae 91 251–274.CrossRefGoogle Scholar
Bliudze, S. and Sifakis, J. (2008a) The algebra of connectors – structuring interaction in BIP. IEEE Transactions on Computers 57 (10)1315–1330.CrossRefGoogle Scholar
Bliudze, S. and Sifakis, J. (2008b) A notion of glue expressiveness for component-based systems. In: van Breugel, F. and Chechik, M. (eds.) CONCUR 2008. Springer-Verlag Lecture Notes in Computer Science 5201 508–522.CrossRefGoogle Scholar
Boulanger, F., Hardebolle, C., Jacquet, C. and Marcadet, D. (2011) Semantic Adaptation for Models of Computation. In: Proceedings of ACSD 2011 (Application of Concurrency to System Design), IEEE Computer Society 153–162.Google Scholar
Bozga, M., Sfyrla, V. and Sifakis, J. (2009) Modeling synchronous systems in BIP. In: Chakraborty, S. and Halbwachs, N. (eds.) EMSOFT '09: Proceedings of the 9th ACM International Conference on Embedded Software, ACM 77–86.CrossRefGoogle Scholar
Broy, M. and Stolen, K. (2001) Specification and Development of Interactive Systems, Monographs in Computer Science 62, Springer-Verlag.CrossRefGoogle Scholar
Bruneton, E., Coupaye, T., Leclercq, M., Quéma, V. and Stefani, J.-B. (2006) The FRACTAL component model and its support in Java. Software: Practice and Experience 36 1257–1284.Google Scholar
Buck, J. T. (1993) Scheduling Dynamic Dataflow Graphs with Bounded Memory Using the Token Flow Model, Ph.D. thesis, University of California, Berkeley.CrossRefGoogle Scholar
Buck, J. T., Ha, S., Lee, E. A. and Messerschmitt, D. G. (1994) Ptolemy: A framework for simulating and prototyping heterogeneous systems. International Journal of Computer Simulation (special issue on ‘Simulation Software Development’) 4 155–182.Google Scholar
Burch, J. R., Passerone, R. and Sangiovanni-Vincentelli, A. L. (2001) Overcoming heterophobia: Modeling concurrency in heterogeneous systems. In: ACSD '01 Proceedings of the Second International Conference on Application of Concurrency to System Design, IEEE Computer Society 13.Google Scholar
Cataldo, A., Lee, E., Liu, X., Matsikoudis, E. and Zheng, H. (2006) A constructive fixed-point theorem and the feedback semantics of timed systems. In: Proceedings of the 8th International Workshop on Discrete-Event Systems (WODES'06), IEEE.Google Scholar
Damm, W., Josko, B., Hungar, H. and Pnueli, A. (1998) A Compositional Real-time Semantics of STATEMATE Designs. In: de Roever, W.-P., Langmaack, H. and Pnueli, A. (eds.) Compositionality: The Significant Difference – Revised Lectures, International Symposium, COMPOS'97. Springer-Verlag Lecture Notes in Computer Science 1536 186–238.CrossRefGoogle Scholar
Davey, B. A. and Priestley, H. A. (2002) Introduction to Lattices and Order, 2nd edition, Cambridge University Press.CrossRefGoogle Scholar
Denckla, B. and Mosterman, P. (2008) Stream- and state-based semantics of hierarchy in block diagrams. In: Proceedings 17th IFAC World Congress 7955–7960.CrossRefGoogle Scholar
Dijkstra, E. W. (1976) A Discipline of Programming, Prentice Hall.Google Scholar
Dill, D. L. (1988) Trace theory for automatic hierarchical verification of speed-independent circuits, Ph.D., Carnegie-Mellon University.CrossRefGoogle Scholar
Edwards, S. A. and Lee, E. A. (2003) The semantics and execution of a synchronous block-diagram language. Science of Computer Programming 48 (1).CrossRefGoogle Scholar
Eker, J.et al. (2003) Taming heterogeneity – the Ptolemy approach. Proceedings of the IEEE 91 (2)127–144.CrossRefGoogle Scholar
Eshuis, R. (2009) Reconciling statechart semantics. Science of Computer Programming 74 (3)65–99.CrossRefGoogle Scholar
Feredj, M., Boulanger, F. and Mbobi, A. M. (2009) A model of domain-polymorph component for heterogeneous system design. The Journal of Systems and Software 82 112–120.CrossRefGoogle Scholar
Floyd, R. W. (1967) Assigning meaning to programs. In Proceedings of Symposium on Applied Mathematics 19, AMS 19–32.Google Scholar
Geilen, M. and Basten, T. (2003) Requirements on the execution of Kahn process networks. In: Degano, P. (ed.) Programming Languages and Systems: 12th European Symposium on Programming, ESOP 2003. Springer-Verlag Lecture Notes in Computer Science 2618 319–334.CrossRefGoogle Scholar
Geilen, M. and Basten, T. (2004) Reactive process networks. In: EMSOFT '04: Proceedings of the 4th ACM International Conference on Embedded Software, ACM 137–146.CrossRefGoogle Scholar
Goderis, A., Brooks, C., Altintas, I., Lee, E. A. and Goble, C. (2009) Heterogeneous composition of models of computation. Future Generation Computer Systems 25 (5)552–560.CrossRefGoogle Scholar
Goessler, G. and Sangiovanni-Vincentelli, A. (2002) Compositional modeling in Metropolis. In: Sangiovanni-Vincentelli, A. and Sifakis, J. (eds.) Embedded Software: Proceedings Second International Conference, EMSOFT 2002. Springer-Verlag Lecture Notes in Computer Science 2491 93–107.CrossRefGoogle Scholar
Graf, S., Ober, I. and Ober, I. (2006) A real-time profile for UML. Software Tools for Technology Transfer 8 (2)113–127.CrossRefGoogle Scholar
Gurevich, Y. (1993) Evolving algebras: An attempt to discover semantics. In: Rozenberg, G. and Salomaa, A. (eds.) Current Trends in Theoretical Computer Science, World Scientific 266–292.CrossRefGoogle Scholar
Halbwachs, N., Caspi, P., Raymond, P. and Pilaud, D. (1991) The synchronous data flow programming language LUSTRE. Proceedings of the IEEE 79 (9)1305–1319.CrossRefGoogle Scholar
Hamon, G. (2005) A denotational semantics for stateflow. In: EMSOFT '05: Proceedings of the 5th ACM International Conference on Embedded Software, ACM 164–172.CrossRefGoogle Scholar
Hamon, G. and Rushby, J. (2004) An operational semantics for Stateflow. In: Wermelinger, M. and Margaria-Steffen, T. (eds.) Fundamental Approaches to Software Engineering: 7th International Conference, FASE 2004. Springer-Verlag Lecture Notes in Computer Science 2984 229–243.CrossRefGoogle Scholar
Hardebolle, C., Boulanger, F., Marcadet, D. and Vidal-Naquet, G. (2007) A generic execution framework for models of computation. In: Proceedings of the Fourth International Workshop on Model-Based Methodologies for Pervasive and Embedded Software: MOMPES '07, IEEE Computer Society 45–54.Google Scholar
Harel, D. (1987) Statecharts: A visual formalism for complex systems. Science of Computer Programming 8 231–274.CrossRefGoogle Scholar
Herrera, F. and Villar, E. (2006) A framework for embedded system specification under different models of computation in SystemC. In: DAC '06: Proceedings of the 43rd annual Design Automation Conference, ACM.Google Scholar
Jantsch, A. (2003) Modeling Embedded Systems and SoCs – Concurrency and Time in Models of Computation, Morgan Kaufmann.Google Scholar
Kahn, G. (1974) The semantics of a simple language for parallel programming. In: Proceedings of the IFIP Congress 74, North-Holland.Google Scholar
Karsai, G. (1995) A configurable visual programming environment: A tool for domain-specific programming. IEEE Computer 36–44.CrossRefGoogle Scholar
Kohavi, Z. (1978) Switching and finite automata theory, McGraw-Hill.Google Scholar
Ledeczi, A.et al. (2001) Composing domain-specific design environments. IEEE Computer 34 (11)44–51.CrossRefGoogle Scholar
Lee, E. A. (1999) Modeling concurrent real-time processes using discrete events. Annals of Software Engineering 7 25–45.CrossRefGoogle Scholar
Lee, E. A. (2009) Finite State Machines and Modal Models in Ptolemy II. Technical Report UCB/EECS-2009-151, EECS Department, University of California, Berkeley.CrossRefGoogle Scholar
Lee, E. A. (2010) Disciplined heterogeneous modeling. In: Petriu, D. C., Rouquette, N. and Haugen, Ø. (eds.) Model Driven Engineering Languages and Systems, 13th International Conference, MODELS 2010: Proceedings, Part II. Springer-Verlag Lecture Notes in Computer Science 6395 273–287.CrossRefGoogle Scholar
Lee, E. A. and Matsikoudis, E. (2009) The semantics of dataflow with firing. In: Huet, G., Plotkin, G., Lévy, J.-J. and Bertot, Y. (eds.) From Semantics to Computer Science: Essays in memory of Gilles Kahn, Cambridge University Press.Google Scholar
Lee, E. A. and Messerschmitt, D. G. (1987) Synchronous data flow. Proceedings of the IEEE 75 (9)1235–1245.CrossRefGoogle Scholar
Lee, E. A. and Parks, T. M. (1995) Dataflow process networks. Proceedings of the IEEE 83 (5)773–801.CrossRefGoogle Scholar
Lee, E. A. and Sangiovanni-Vincentelli, A. (1998) A framework for comparing models of computation. IEEE Transactions on Computer-Aided Design of Circuits and Systems 17 (12)1217–1229.CrossRefGoogle Scholar
Lee, E. A. and Tripakis, S. (2010) Modal Models in Ptolemy. In: EOOLT 2010 – 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools, Linköping University Electronic Press.Google Scholar
Lee, E. A. and Zheng, H. (2005) Operational semantics of hybrid systems. In: Morari, M. and Thiele, L. (eds.) Hybrid Systems: Computation and Control – 8th International Workshop, HSCC 2005. Springer-Verlag Lecture Notes in Computer Science 3414 25–53.CrossRefGoogle Scholar
Lee, E. A. and Zheng, H. (2007) Leveraging synchronous language principles for heterogeneous modeling and design of embedded systems. In: EMSOFT '07: Proceedings of the 7th ACM and IEEE International Conference on Embedded Software, ACM.Google Scholar
Liu, J. and Lee, E. A. (2003) On the causality of mixed-signal and hybrid models. In: Maler, O. and Pnueli, A. (eds.) Hybrid Systems: Computation and Control 6th International Workshop, HSCC 2003. Springer-Verlag Lecture Notes in Computer Science 2623 328–342.CrossRefGoogle Scholar
Liu, X. and Lee, E. A. (2008) CPO semantics of timed interactive actor networks. Theoretical Computer Science 409 (1)110–125.CrossRefGoogle Scholar
Liu, X., Matsikoudis, E. and Lee, E. A. (2006) Modeling timed concurrent systems. In: Baier, C. and Hermanns, H. (eds.) Concurrency Theory: 17th International Conference, CONCUR 2006. Springer-Verlag Lecture Notes in Computer Science 4137 1–15.CrossRefGoogle Scholar
Lublinerman, R., Szegedy, C. and Tripakis, S. (2009) Modular Code Generation from Synchronous Block Diagrams – Modularity vs. Code Size. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'09), ACM 78–89.CrossRefGoogle Scholar
Malik, S. (1994) Analysis of cyclic combinational circuits. IEEE Transactions on Computer-Aided Design 13 (7)950–956.CrossRefGoogle Scholar
Manna, Z. and Pnueli, A. (1992) Verifying hybrid systems. Hybrid Systems 4–35.Google Scholar
Maraninchi, F. and Bhouhadiba, T. (2007) 42: Programmable models of computation for a component-based approach to heterogeneous embedded systems. In: GPCE '07: Proceedings of the 6th International Conference on Generative Programming and Component Engineering, ACM 53–62.CrossRefGoogle Scholar
Maraninchi, F. and Rémond, Y. (2003) Mode-automata: a new domain-specific construct for the development of safe critical systems. Science of Computer Programming 46 219–254.CrossRefGoogle Scholar
Meyer, B. (1992) Applying ‘design by contract’. Computer 25 (10)40–51.CrossRefGoogle Scholar
Nordstrom, G., Sztipanovits, J., Karsai, G. and Ledeczi, A. (1999) Metamodeling – rapid design and evolution of domain-specific modeling environments. In ECBS'99: Proceedings of the 1999 IEEE Conference on Engineering of Computer-Based Systems, IEEE Computer Society 68–74.Google Scholar
Patel, H. D. and Shukla, S. K. (2004) SystemC Kernel Extensions for Heterogeneous System Modelling, Kluwer.Google Scholar
Reed, G. M. and Roscoe, A. W. (1988) Metric spaces as models for real-time concurrency. In: Main, M., Melton, A., Mislove, M. and Schmidt, D. (eds.) Mathematical Foundations of Programming Language Semantics: Proceedings 3rd Workshop, Tulane University, New Orleans. Springer-Verlag Lecture Notes in Computer Science 298 331–343.CrossRefGoogle Scholar
Sander, I. and Jantsch, A. (2004) System modeling and transformational design refinement in ForSyDe. IEEE Transactions on Computer-Aided Design of Circuits and Systems 23 (1)17–32.CrossRefGoogle Scholar
Scaife, N., Sofronis, C., Caspi, P., Tripakis, S. and Maraninchi, F. (2004) Defining and Translating a ‘Safe’ Subset of Simulink/Stateflow into Lustre. In: EMSOFT '04: Proceedings of the 4th ACM International Conference on Embedded Software, ACM 259–268.CrossRefGoogle Scholar
Shiple, T., Berry, G. and Touati, H. (1996) Constructive analysis of cyclic circuits. In: European Design and Test Conference (EDTC'96), IEEE Computer Society.Google Scholar
Sifakis, J. (1977) Use of petri nets for performance evaluation. In: Measuring, modelling and evaluating computer systems, North-Holland 75–93.Google Scholar
Simon, G., Kovácsházy, T. and Péceli, G. (2001) Transient management in reconfigurable systems. In: Robertson, P., Shrobe, H. and Laddaga, R. (eds.) Self-Adaptive Software: First International Workshop, IWSAS 2000: Revised Papers. Springer-Verlag Lecture Notes in Computer Science 1936 90–98.CrossRefGoogle Scholar
Sztipanovits, J., Wilkes, D., Karsai, G., Biegl, C. and Lynd, L. (1993) The multigraph and structural adaptivity. IEEE Transactions on Signal Processing 41 (8)2695–2716.CrossRefGoogle Scholar
Tripakis, S., Bui, D., Geilen, M., Rodiers, B. and Lee, E. A. (2010). Compositionality in Synchronous Data Flow: Modular Code Generation from Hierarchical SDF Graphs. Preprint available as a technical report from http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-143.html.Google Scholar
Yates, R. K. (1993) Networks of real-time processes. In: Best, E. (ed.) Proceedings of the 4th International Conference on Concurrency Theory (CONCUR). Springer-Verlag Lecture Notes in Computer Science 715 384–397.CrossRefGoogle Scholar
Zhu, Y.et al. (2010) Mathematical equations as executable models of mechanical systems. In: ICCPS '10: Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems, ACM 1–11.Google Scholar