Formal Verification of Hierarchical Ptolemy II Synchronous-Reactive Models with Bounded Model Checking

Ptolemy II is an open-source modeling and simulation tool for concurrent, real-time and embedded systems, particularly those involving hierarchical heterogeneity. Synchronous-reactive (SR) model of computation which has been implemented in Ptolemy II is commonly used to design safety-critical systems with complicated control logic. Formally verifying the correctness of hierarchical SR models is of great importance and also challenging due to the formalization of a series of specific features including, e.g., instantaneous communication between actors across the level of hierarchy, the combination of SR's fixed-point semantic with hierarchical structure, and multiple clocks proceeding at different rates in multiclock SR models. In this paper, we tackle such challenges and propose a bounded model checking (BMC) approach to typical actors commonly used in hierarchical SR models. In addition, we implement the proposed BMC approach to hierarchical SR models in a prototype tool called Ptolemy-Z3, which has been integrated into the Ptolemy II environment. Experimental results show that Ptolemy-Z3 outperforms significantly Ptolemy-NuSMV (a verification tool provided by the Ptolemy II environment) in the verification capability of hierarchical SR models.