首页> 中文期刊> 《计算机技术与发展》 >基于NuSMV的SysML模型形式化验证

基于NuSMV的SysML模型形式化验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

cqvip:航空航天道路交通等高安全领域的系统开发需要保证高安全、高可靠,对于该类系统的合理建模以及模型验证则尤为重要。当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制开发时间和成本,并降低系统出现风险的可能性。但与此同时,需求与设计模型之间仍然存在着沟壑,设计模型是否很好地满足用户所提出的需求在完成系统设计后仍需验证。针对系统建模语言缺乏精确形式化语义难以进行模型验证的问题,文中给出一套从SysML设计模型到NuSMV模型转换的语义规则,实现了一个自动转换程序,将SysML模型文件转换成NuSMV输入文件,进而利用NuSMV实现SysML模型的验证。最后通过一个铁路控制系统的案例证明了该方法的有效性。

著录项

来源
《计算机技术与发展》 |2019年第10期|153-156|共4页
作者
邓刘梦; 葛晓瑜; 宛伟健;
展开▼
作者单位

南京航空航天大学计算机科学与技术学院江苏南京 211106;

展开▼
原文格式 PDF
正文语种 chi
中图分类程序设计、软件工程;
关键词
需求工程; 模型转换; 形式化验证; 模型驱动开发;

相似文献

中文文献
外文文献
专利

1. 基于模型检测工具NuSMV的功能测试用例生成方法 [J] . 何洋 ,洪玫 ,祁琳莹 . 计算机应用 . 2015,第0z2期
2. 一种基于NuSMV模型检测的服务组合编制方法 [J] . 孙杰 ,蒋静 ,郭晓华 . 青岛大学学报（自然科学版） . 2014,第003期
3. 基于NuSMV的AADL行为模型验证的探究 [J] . 刘博 ,李蜀瑜 . 计算机技术与发展 . 2012,第002期
4. 基于NuSMV的Web服务失配限界模型检测 [J] . 陈圣标 ,吴剑峰 ,张广泉 . 苏州大学学报（自然科学版） . 2011,第001期
5. 一种AltaRica3.0模型到NuSMV模型的转换方法 [J] . 陈朔 ,胡军 ,唐红英 . 计算机科学 . 2020,第012期
6. 基于NuSMV的AADL行为模型验证的探究 [C] . 刘博 ,李蜀瑜 . 2011嵌入式技术开发论坛 . 2011
7. 基于NuSMV的AUML模型形式化验证 [A] . 梁文福 . 2006

获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

客服微信
服务号