一种形式化建模中活性属性转化方法研究

• 作者: 尹小花 张棋 谢健
• 来源期刊: 计算技术与自动化
• 关键词: 安全关键系统 KAOS Event-B 活性 模型检测
• 年，卷（期）: 2018,（3）
• 所属期刊栏目: 计算机软件及应用
• 页码范围: 161-164
• 页数: 4页
• 分类号: TP311
• 语种: 中文
• DOI: 10.16339/j.cnki.jsjsyzdh.201803031

摘要

现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证,这种方法一方面需要耗费大量时间与人力,另一方面测试并不能保证系统中不存在错误.使用形式化的开发方法可以将软件需求添加到模型中,使用数学证明的方法来验证所要建立的系统是正确的,即在开发早期就能发现需求与系统设计间可能存在的问题,能够有效地减少后期发现错误所带来的损失.在现有需求工程方法KAOS方法转化到Event-B模型的方法基础上,对其中活性属性丢失问题进行研究,并给出了解决方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张棋	南京航空航天大学计算机科学与技术学院	1	0	0.0	0.0
2	谢健	南京航空航天大学计算机科学与技术学院	5	15	3.0	3.0
3	尹小花	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0