Abstract.
Interface automata [deH01] have been introduced as an interface theory [deH01a] capable of functioning as a behavioral type system. Behavioral type systems describe dynamic properties of components and their compositions. Like traditional (data) type systems, behavioral type systems can be used to check compatibility of components. In this paper, we use interface automata to devise a behavioral type system for Ptolemy II, leveraging the contravariant and optimistic properties of interface automata to achieve behavioral subtyping and polymorphism. Ptolemy II is a software framework supporting concurrent component composition according to diverse models of computation. In this paper, we focus on representing the communication protocols used in component communication within the behavioral type system. In building this type system, we identify two key limitations in interface automata formalisms; we overcome these limitations with two extensions, transient states and projection automata. In addition to static type checking, we also propose to extend the use of interface automata to the on-line reflection of component states and to run-time type checking, which enable dynamic component creation, morphing application structure, and admission control. We discuss the trade-offs in the design of behavioral type systems.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Corresponding author
Additional information
Received September 2002
Accepted in revised form November 2003 by M. Broy, G. Lüttgen and M. Mendler
Rights and permissions
About this article
Cite this article
Lee, E., Xiong, Y. A behavioral type system and its application in Ptolemy II. Formal Aspects of Computing 16, 210–237 (2004). https://doi.org/10.1007/s00165-004-0043-8
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-004-0043-8