| 一种形式化建模中活性属性转化方法研究 |
 点此下载全文 |
| 引用本文：张 棋，谢 健，尹小花.一种形式化建模中活性属性转化方法研究[J].计算技术与自动化,2018,(3):161-164 |
| 摘要点击次数: 1190 |
| 全文下载次数: 0 |
|
|
| 中文摘要:现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证，这种方法一方面需要耗费大量时间与人力，另一方面测试并不能保证系统中不存在错误。使用形式化的开发方法可以将软件需求添加到模型中，使用数学证明的方法来验证所要建立的系统是正确的，即在开发早期就能发现需求与系统设计间可能存在的问题，能够有效地减少后期发现错误所带来的损失。在现有需求工程方法KAOS方法转化到Event-B模型的方法基础上，对其中活性属性丢失问题进行研究，并给出了解决方法。 |
| 中文关键词:安全关键系统 KAOS Event-B 活性 模型检测 |
| |
| Research on Liveness Property Translation for Safety-Critical System Modeling |
|
|
| Abstract:The traditional verification method of safety-critical system usually happened in the late stage of system development.On one hand，test stage requires a lot of time and effort，moreover，traditional test technique does not guarantee that there is no error in the system.On the other hand，formal development methods use mathematic language to describe requirements，and then use various model checking methods to prove that the model which contains properties of requirements is correct.So we can find design error in early development stage，and this can reduce the losses caused by late errors.In this paper，we discuss the deletion of liveness property in several translation method from goal-oriented method to Event-B method，then we give a solution. |
| keywords:safety-critical system KAOS Event-B liveness model checking |
| 查看全文 查看/发表评论 下载pdf阅读器 |
次