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

Research on Liveness Property Translation for Safety-Critical System Modeling

作　　者：张棋 谢健[1] 尹小花 ZHANG Qi;XIE Jian;YIN Xiao-hua(Nanjing University of Aeronautics and Astronautics,College of Computer Science and Technology,Nanjing Jiangsu,211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106

出　　处：《计算技术与自动化》2018年第3期161-164,共4页Computing Technology and Automation

基　　金：国家自然科学基金资助项目(61772270);国家重点研发计划(2016YFB1000802)

摘　　要：现有的安全关键系统开发的方法一般是在系统开发后期使用测试的方法对系统需求进行验证,这种方法一方面需要耗费大量时间与人力,另一方面测试并不能保证系统中不存在错误。使用形式化的开发方法可以将软件需求添加到模型中,使用数学证明的方法来验证所要建立的系统是正确的,即在开发早期就能发现需求与系统设计间可能存在的问题,能够有效地减少后期发现错误所带来的损失。在现有需求工程方法KAOS方法转化到Event-B模型的方法基础上,对其中活性属性丢失问题进行研究,并给出了解决方法。The traditional verification method of safety-critical system usually happened in the late stage of system clevelopment.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-orientecl method to Event-B method, then we give a solution.

关 键 词：安全关键系统 KAOS EVENT-B 活性 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]