基于行为时序逻辑TLA的时钟系统分析与检测

• 作者: 吴勇 李祥
• 来源期刊: 电力学报
• 学科: 工学
• 关键词: 计算机应用 模型检测 时钟系统 行为时序逻辑 TLC
• 年，卷（期）: 2011,（4）
• 所属期刊栏目: 自动化
• 页码范围: 310-312,321
• 分类号: TP393.08
• 字数: 2817字
• 语种: 中文
• DOI: 10.3969/j.issn.1005-6548.2011.04.009

摘要

对基于行为时序逻辑TLA的模型检测技术进行了研究,指明了TLA的语义和语法并对行为时序逻辑中的公平性问题进行了定义.用基于TLA的系统描述语言TLA+对时钟系统进行描述并用其模型检测工具TLC对其进行了验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
2	吴勇	山西大学工程学院	5	3	1.0	1.0