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

摘要

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