状态图到PTL形式规范的转化

摘要：

本文讨论从状态图到PTL形式规范的转化方法.状态图是描述系统行为的半形式化的图形工具,但缺少精确的形式语义,PTL(投影时序逻辑)是一种具有离散的时间模型的时序逻辑,把状态图转换到PTL后可以使其具有精确的形式语义并能使用形式化验证方法来证明状态图所描述的系统的一些重要性质是否得到满足,同时可把系统的形式描述转换为Tempura程序进行模拟,从而提高系统设计的可信性.

关键词： 投影时序逻辑 状态图 形式化方法

作者: 张鹏飞 段振华 田聪

作者单位: 西安电子科技大学计算机学院,陕西,西安,710071

会议类型: 国内会议

会议名称: 中国计算机学会软件工程专委会2006年年会

会议地点: 长沙

会议语种:中文

页码: 122-125

在线出版日期: 2006-11-01（万方平台首次上网日期，不代表论文的发表时间）