| 基于时态逻辑的抽象对象规约方法 |
| |
| 引用本文： | 宋悦 郝克刚. 基于时态逻辑的抽象对象规约方法[J]. 西北大学学报(自然科学版), 1999, 29(6): 499-502 |
| |
| 作者姓名： | 宋悦 郝克刚 |
| |
| 作者单位： | 西北大学计算机科学系!陕西西安710069 |
| |
| 基金项目： | 国家“863”计划资助项目!863－306－2T02－04－01 |
| |
| 摘 要： | 提出了一种基于时态逻辑的抽象对象语义描述方法，采用这种方法，可以在说明对象的同时对其行为加以时态限制，从而在语义层次上规约了并行对象系统的行为。在此方法上，还可以进一步对系统进行形式化的验证。
|
| 关 键 词： | 时态逻辑 计算树逻辑 反应系统 形式化方法 规约 |
Using temporal logic to specify abstract object |
| |
| SONG Yue, HAO Ke-gang, GE Wei. Using temporal logic to specify abstract object[J]. Journal of Northwest University(Natural Science Edition), 1999, 29(6): 499-502 |
| |
| Authors: | SONG Yue HAO Ke-gang GE Wei |
| |
| Abstract: | An abstract spcification method of concurrent object family was presented. Temporal logic CTL was used as the base of language to specify dynamic behavior of object and synchronic between them. Using this method, object data and its behavior can be specified in one object model. Furthermore,object semantic can be checked formally and automally with this method. |
| |
| Keywords: | temporal logic CTL reactive system formal method specification |
| 本文献已被 CNKI 维普 等数据库收录！ |
