基于时间多栈下推网络的实时系统验证

• 作者: 古天龙 甘鹏程 赵岭忠 郭云川 钱俊彦
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: MPDN TMPDN 并发递归程序 时钟等价 可达性
• 年，卷（期）: 2016,（11）
• 所属期刊栏目: 软件技术
• 页码范围: 2253-2269
• 页数: 17页
• 分类号: TP311
• 字数: 16644字
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2016.02253

摘要

多栈下推网络（MPDN）是利用多个栈来描述并发递归程序线程之间交互的一种下推系统模型．为了描述基于线程之间交互的实时并发递归程序，首先将描述连续时间的时钟引入到 MPDN，提出了时间多栈下推网络（TMPDN），并给出了语法及其操作语义；其次利用基于时间关键点的时钟等价优化技术，缩减等价域状态空间；然后通过静态转换方法，获得所有的可达域状态格局，将连续时间的 TMPDN 模型转换成离散的 MPDN 模型．在此基础上，基于 on-the-fly 技术，采用动态转换方法，仅关心栈顶域状态转换，进一步缩减转换后的状态空间．同时证明了状态 qF 在 TMPDN 可达当且仅当其转换状态 q′F 在 MPDN 可达，并给出了模型转换算法；最后可采用现有模型检验工具验证转换后的 MPDN．

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子科技大学广西可信软件重点实验室	207	1546	18.0	30.0
2	钱俊彦	桂林电子科技大学广西可信软件重点实验室	86	238	9.0	10.0
3	赵岭忠	桂林电子科技大学广西可信软件重点实验室	64	229	8.0	11.0
4	郭云川	中国科学院信息工程研究所	21	48	3.0	6.0
5	甘鹏程	桂林电子科技大学广西可信软件重点实验室	1	1	1.0	1.0