典型文献
基于SysML的机载软件分层精化建模与验证方法
文献摘要：
机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.
文献关键词：
机载软件;模型精化;模型转换;模型检验
中图分类号：
作者姓名：
肖思慧;刘琦;黄滟鸿;史建琦;郭欣
作者机构：
华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 200062
文献出处：
引用格式：
[1]肖思慧;刘琦;黄滟鸿;史建琦;郭欣-.基于SysML的机载软件分层精化建模与验证方法)[J].软件学报,2022(08):2851-2874
A类：
TCTL
B类：
SysML,机载软件,验证方法,航空航天,航天领域,机载设备,软件规模,发带,基于模型,开发效率,形式化方法,发难,状态机,子集,动态行为,初始模型,逐层,设计模型,自动转换,时间自动机,软件需求,模型检验,Simulink,Coder,源代码,飞行控制,控制软件,模型精化,模型转换
AB值：
0.359927
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
