원문정보
보안공학연구지원센터(IJHIT)
International Journal of Hybrid Information Technology
Vol.6 No.6
2013.11
pp.203-216
피인용수 : 0건 (자료제공 : 네이버학술정보)
초록
영어
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.
목차
Abstract
1. Introduction
2. Preliminaries
2.1 Propositional Projection Temporal Logic
2.2 Normal Form of PPTL
2.3 Labeled Normal Form Graph
3. Symbolic Model Checking for PPTL
4. A Case Study
5. Related Work
6. Conclusion
7. ACKNOWLEDGEMENTS
References
1. Introduction
2. Preliminaries
2.1 Propositional Projection Temporal Logic
2.2 Normal Form of PPTL
2.3 Labeled Normal Form Graph
3. Symbolic Model Checking for PPTL
4. A Case Study
5. Related Work
6. Conclusion
7. ACKNOWLEDGEMENTS
References
키워드
저자정보
참고문헌
자료제공 : 네이버학술정보