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

作     者：张鹏飞 段振华 田聪 ZHANG Peng-fei;DUAN Zhen-hua;TIAN Cong

作者机构：西安电子科技大学计算机学院陕西西安710071 西安电子科技大学计算机学院陕西西安710071 西安电子科技大学计算机学院陕西西安710071 

基　　金：国家自然科学基金资助项目(60373103,60433010) 教育部博士点基金资助项目(20030701015) 

出 版 物：《计算机工程与科学》 (Computer Engineering & Science)

年 卷 期：2006年第28卷第Z2期

页      码：122-125页

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

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

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1007-130X.2006.z2.036

馆 藏 号：203102317...