基于形式语言B的一种新的时态规约方案

• 作者: 张德运 肖健宇 董皓 陈海诠
• 来源期刊: 微电子学与计算机
• 关键词: 时态规约 形式化方法 实时系统 B方法 B函数
• 年，卷（期）: 2006,（2）
• 页码范围: 16-19
• 页数: 4页
• 分类号: TP311.1
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2006.02.006

摘要

提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证.该方案中,时间类型表示为B方法中系统内部支持的非负整数集合,所有依赖于时间的变量都表示成定义域为时间的全函数.该方案可以方便地表达"过去"、"现在"、"稳定"、"跳变"等时态概念.定义了时间类型、"现在"以及与时间有关的变量的宏操作等抽象机,这些抽象机已经通过B工具的一致性验证,可以在实时系统的B形式化规约中直接使用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	肖健宇	西安交通大学电子与信息工程学院	13	83	6.0	8.0
4	陈海诠	西安交通大学电子与信息工程学院	8	67	5.0	8.0
5	董皓	西安交通大学电子与信息工程学院	12	83	6.0	9.0