Verification of Embedded Real-Time Systems Using Symbolic Model Checking: A Case Study
Tao Pang, Zhenhua Duan, Xiaofang Liu · International Journal of Hybrid Information Technology · 2013
This paper presents a case study for symbolic model checking (SMC) with Propositional Projection Temporal Logic (PPTL).First, PPTL is briefly introduced.Then an outline of symbolic model checking algorithm for PPTL proposed in [21] is presented.As a case study, a single-track railroad crossing control system (STRCCS) is employed to illustrate how SMC for PPTL can be utilized in the specification and verification of embedded real-time systems.