Real-time embedded systems are increasingly applied in safety-critical areas, so guaranteeing the correctness of such systems by means of formal methods becomes particularly important. In this paper, we propose an optimized bounded model checking (BMC)-based formal verification approach for the verification of safety for synchronous-reactive (SR) models, which are often used to design systems with complicated control logic, especially the real-time embedded control systems. This method is based on the tackling of a series of challenging problems including the management of the logical clock, encoding of the contained ports, representation of the data types of ports, descriptions of behaviors of various components in a considered model, and formal consideration of the fixed-point semantics. We have implemented this proposed method in the prototype Ptolemy-Z3, and integrated this tool into the Ptolemy II environment. In addition, the experimental evaluation on 22 SR models has shown that our method performs better than the existing automatic verification method in Ptolemy II.

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 the relationship between the “tick in SR models and the step in BMC method, simultaneous actor reaction to an input signal and instantaneous communication between actors through sending messages via ports, and fixed-point semantics associated with tick execution, etc. In addition to tackle these challenges, we also present a BMC encoding approach to most common NonFSMActors in SR, which can be used as a library for similar work such as Lingua Franca. 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 formal conversion and verification capability of different types of SR models.

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.