基于线性时序逻辑的实时系统模型检查

• 作者: 唐稚松 李广元
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 实时系统 时间自动机 线性时序逻辑 模型检查 性质验证
• 年，卷（期）: 2002,（2）
• 页码范围: 193-202
• 页数: 10页
• 分类号: TP301
• 字数: 10593字
• 语种: 中文

摘要

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	唐稚松		7	188	6.0	7.0
2	李广元		3	81	3.0	3.0