数字系统投影时序逻辑描述及验证  

PTL Specification and Verification of Digital System

作　　者：张鹏飞[1] 叶永升[2] 

机构地区：[1]淮北师范大学计算机科学与技术学院,安徽淮北235000 [2]淮北师范大学数学科学学院,安徽淮北235000

出　　处：《淮北师范大学学报（自然科学版）》2013年第4期61-66,共6页Journal of Huaibei Normal University：Natural Sciences

基　　金：淮北市科技局基金项目(20120309)

摘　　要：投影时序逻辑是一种具有离散时间模型的时序逻辑,其部分子集又是一种程序设计语言,可处理顺序和并发计算.文章讨论应用投影时序逻辑对数字系统进行形式描述和验证的方法,该方法可在数字系统的不同层级设计过程中,使用投影时序逻辑对其系统行为和性质进行形式化的描述及验证,从而提高系统设计的可信性.PTL （Projection Temporal Logic） is a kind of temporal logic which can handle both sequential and parallel computa- tion. A formal approach of specification and verification of digital system using PTL is proposed in this paper. With this ap- proach, PTL and its executable subset （MSVL） are used for formal specification and verification in different level design of a digital system.

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

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