支持活性属性保持的安全关键系统建模方法

发布时间：2020-05-21 16:57

【摘要】：使用传统的开发方法对安全关键系统进行开发时,早期系统设计阶段的错误往往到开发后期的测试阶段才能检测出来,重新对系统结构进行错误修改会造成大量的时间和人力耗费。并且由于测试并不能保证系统中不存在错误,无法满足安全关键系统对安全性和可靠性的要求。与之对应的是,形式化开发方法使用精确的数学语言根据系统需求进行描述,消除自然语言带来的二义性,同时,形式化方法根据系统需求进行建模后,使用数学证明的方式来验证模型的正确性,能够在开发早期发现需求与设计上存在的错误,避免了后期的测试所带来的时间和成本消耗。然而,由于形式化方法在使用时需要将自然语言描述的需求文本转换成精确的形式化规约,对开发人员的专业知识背景要求很高。因此一般需要使用需求工程中的需求分析方法将系统需求进行分解,转换成半形式化的中间语言,减轻前期获取需求规约的困难。本文使用SysML/KAOS方法在前期对需求进行处理,将文本需求转换成使用特定标记语言表示的目标(goal)中,然后根据目标模型中的精化分解关系将复杂需求进行分解,建立需求的层次结构。同时,建立从SysML/KAOS方法到形式化建模语言Event-B的关系映射,将目标模型中的目标和需求精化关系转换到Event-B的模型元素中,然后通过Event-B中的验证机制对转换的正确性和一致性进行验证。本文的主要研究工作如下:(1)将SysML/KAOS模型中表示功能需求的实现目标(Achieve goal)和表示安全需求的维持目标(Maintain goal)转换到Event-B模型中的对应元素;(2)将目标模型中的三种需求精化模式对应转换到Event-B的模型精化关系中,同时给出了转换一致性和正确性证明;(3)对于转换中存在的活性属性丢失问题进行讨论,给出了目标模型中活性属性在Event-B建模过程中的表达方式,然后针模型中已经添加的活性属性可能在精化过程中丢失的问题进行研究,给出的精化中活性属性保持的方法和相关证明。
【图文】：

图 3.14 Event-B 中模型 M2精化后的事件使用 ProB 工具对模型 M2进行验证与模拟的结果如图 3.15，可以看到，在该工具验证下的不变式和事件的正确性能够完整的保持

持活性属性保持的安全关键系统建模方oor_open = Fift_move =TLift_moveDoor_openDoor_openLift_moveColse_doorLift_stopLift_start图 5.6 模型 M1 的状态变迁图了表示安全性属性的不变式@inv1，则中的事件生成证明义务，，然后通过证明结果如下：
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP311.5

【参考文献】

相关期刊论文 前6条

1 李婉璐;;软件工程中的形式化方法研究综述[J];数字技术与应用;2015年10期

2 杨启亮;邢建春;王平;;安全关键系统及其软件方法[J];计算机应用与软件;2011年02期

3 祝义;黄志球;曹子宁;周航;刘亚萍;;一种基于形式化规约生成软件体系结构模型的方法[J];软件学报;2010年11期

4 杨仕平;熊光泽;桑楠;;安全关键系统高可信保障技术的研究[J];计算机科学;2003年05期

5 王继成,高珍;软件需求分析的研究[J];计算机工程与设计;2002年08期

6 黎忠文,熊光泽;形式化方法与安全关键系统[J];计算机应用;2000年09期

相关博士学位论文 前1条

1 苏雯;基于Event-B的混合系统形式化：理论与实践[D];华东师范大学;2013年

相关硕士学位论文 前4条

1 叶水琴;基于目标模型的横切关注点识别方法研究[D];武汉工程大学;2015年

2 彭小玲;软件非功能需求层次模型研究[D];中南大学;2011年

3 李平;面向目标建模的MDA模型转换研究与实现[D];哈尔滨工程大学;2011年

4 汪光明;FKAOS方法中Agent实体优化的研究和应用[D];合肥工业大学;2008年

本文编号：2674615