Ptolemy II is an open-source modeling and simulation tool supporting the design of the concurrent, real-time and embedded systems, particularly those involving heterogeneous mixtures of models of computation. In this paper, we present a bounded model checking (BMC) and k-induction based formal verification approach to Ptolemy II, especially its synchronous reactive (SR) models which are commonly used to design systems with complicated control logic. Compared to the verification of common finite-state based systems, the challenges include fixed-point semantics associated with tick execution, simultaneous actor reaction to an input signal, and instantaneous communication between actors through sending messages via ports, etc. In addition to tackle these challenges, we also present a BMC encoding approach to most common non-FSMActor actors in SR, which can be used as a library for similar work such as Lingua France. We have implemented a prototype (named as Ptolemy-Z3) and integrated it into the Ptolemy II tool. Experimental results show that Ptolemy-Z3 outperforms the existing tool Ptolemy-NuSMV significantly in both capability and efficiency.