投影时序逻辑在系统建模中的应用  

Application of projection temporal logic in system modeling

作　　者：舒新峰[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,陕西西安710071

出　　处：《西北大学学报（自然科学版）》2010年第3期410-414,共5页Journal of Northwest University（Natural Science Edition）

基　　金：国家自然科学基金资助项目(60873018);国家自然科学基金重点基金资助项目(60433010)

摘　　要：目的为了解决形式化验证时需要分别使用不同工具进行系统建模和性质描述的问题。方法利用投影时序逻辑PTL(projection temporal logic)在同一逻辑框架内完成待验证系统的建模和性质的描述。结果对PTL投影操作符的特点和用途进行了详细分析,并结合实例展示了PTL系统建模的使用。结论 PTL具备强大的表达能力,可广泛的应用于各类软硬件系统的验证。Aim To solve the problem that two different tools are needed in system modeling and properties description respectively when doing formal verifications. Methods PTL is employed to describe the properties as well as the implication of the system to be verified within a same logical framework. Results The properties and purpose of projection operators of PTL are analyzed in detail; further,an example is given to illustrate how PTL woks in system modeling. Conclusion PTL has a powerful expressiveness and can be widely used in formal verifications for various software and hardware systems.

关 键 词：投影时序逻辑 系统建模 形式化验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]