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

• 作者: 张鹏飞 段振华 田聪
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 投影时序逻辑 状态图 形式化方法
• 年，卷（期）: 2006,（z2）
• 页码范围: 122-125
• 页数: 4页
• 分类号: TP3
• 字数: 3405字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2006.z2.036

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张鹏飞	西安电子科技大学计算机学院	27	107	6.0	9.0
2	段振华	西安电子科技大学计算机学院	47	363	10.0	16.0
3	田聪	西安电子科技大学计算机学院	8	41	4.0	6.0