| 基于行为时序逻辑TLA的时钟系统分析与检测 |
| |
| 引用本文： | 吴勇,李祥.基于行为时序逻辑TLA的时钟系统分析与检测[J].电力学报,2011,26(4):310-312,321. |
| |
| 作者姓名： | 吴勇 李祥 |
| |
| 作者单位： | 1. 山西大学工程学院,太原,030013
2. 贵州大学计算机软件与理论研究所,贵阳,550025 |
| |
| 摘 要： | 对基于行为时序逻辑TLA的模型检测技术进行了研究,指明了TLA的语义和语法并对行为时序逻辑中的公平性问题进行了定义.用基于TLA的系统描述语言TLA+对时钟系统进行描述并用其模型检测工具TLC对其进行了验证.
|
| 关 键 词： | 计算机应用 模型检测 时钟系统 行为时序逻辑 TLC |
Analysis and Detection of the Clock System Based on TLA |
| |
| WU Yong,LI Xiang.Analysis and Detection of the Clock System Based on TLA[J].Journal of Electric Power,2011,26(4):310-312,321. |
| |
| Authors: | WU Yong LI Xiang |
| |
| Affiliation: | 1.Engineering College of Shanxi University,Taiyuan 030013,China; 2.Guizhou Institute of Computer Software and Theory,Guizhou University,Guiyang 550025,China) |
| |
| Abstract: | The author researches the Model checking based on Temporal Logic of Actions, specifies the Syntax and Semantics of Temporal Logic of Actions,defines the fairness of TLA,depicts a clock System with TLA+ which based on the TLA and Verifies it with TLC. |
| |
| Keywords: | model checking clock system TLA TLC |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
