A formal representation of discrete event models in Ptolemy II

Within the embedded software design process, formal methods including formal specifications and formal verifications can be used to check designs, with the goal of ensuring the requirements of embedded software, such as reliability and concurrency. This paper presents a means to formally describe the discrete event models of Ptolemy II that is a modeling and simulation environment for embedded software. The proposed formal specification distinguishes between model structure and behavior and can construct complex models through hierarchical compositions of sub-model. The specification may be used as a basis for formal verifications of the models.