期刊名称:International Journal of Hybrid Information Technology
印刷版ISSN:1738-9968
出版年度:2013
卷号:6
期号:6
出版社:SERSC
摘要:This paper presents a case study for symbolic model checking (SMC) with PropositionalProjection Temporal Logic (PPTL). First, PPTL is brie.y introduced. Then an outline ofsymbolic 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 SMCfor PPTL can be utilized in the specification and verification of embedded real-time systems
关键词:Propositional Projection Temporal Logic; Symbolic Model Checking; Veri-;fication; Embedded Real-Time Systems