软件学报

作者：肖思慧，刘琦，黄滟鸿，史建琦，郭欣

单位：肖思慧，华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 20006211,刘琦，华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 20006202,黄滟鸿，华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 20006203,史建琦，华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 20006204,郭欣，华东师范大学 软件工程学院, 上海 200062;国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 20006205

关键词：机载软件;模型精化;模型转换;模型检验

基金：国家重点研发计划(2019YFB2102602)

机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期