基于Event-B的一种联锁逻辑的形式化建模研究

• 作者: 唐晨 沈啸 陈邦兴
• 来源期刊: 信息技术
• 学科: 工学
• 关键词: 联锁逻辑 形式化建模 Event-B
• 年，卷（期）: 2013,（2）
• 所属期刊栏目: 基金项目
• 页码范围: 7-10,14
• 页数: 5页
• 分类号: TP311.52
• 字数: 3816字
• 语种: 中文

摘要

铁路车站信号联锁逻辑的形式化描述无论对计算机联锁软件的研发,还是对联锁软件的第三方测试都是非常重要的.基于Event-B方法,利用自动机模型和形式化语言对车站的一种信号联锁逻辑进行建模研究,并通过逐步精化的方法扩展联锁功能,依赖不变式技术形式化地保证了该模型的安全性.所建模型通过Rodin平台的验证,结果表明它们是安全的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈邦兴	同济大学电子与信息工程学院	25	186	8.0	13.0
2	沈啸	同济大学电子与信息工程学院	1	2	1.0	1.0
3	唐晨	同济大学电子与信息工程学院	3	3	1.0	1.0