| 本文已被：浏览 1660次 下载 4004次 |
码上扫一扫！ |
|
|
| 基于SysML的机载软件分层精化建模与验证方法 |
|
肖思慧1,2, 刘琦1,2, 黄滟鸿1,2, 史建琦1,2, 郭欣1,2
|
|
1.华东师范大学 软件工程学院, 上海 200062;2.国家可信嵌入式软件工程技术研究中心(华东师范大学), 上海 200062
|
|
| 摘要: |
| 机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性. |
| 关键词: 机载软件 模型精化 模型转换 模型检验 |
| DOI：10.13328/j.cnki.jos.006602 |
| 分类号:TP311 |
| 基金项目:国家重点研发计划(2019YFB2102602) |
|
| Hierarchical Refined Modeling and Verification Method of Airborne Software Using SysML |
|
XIAO Si-Hui1,2, LIU Qi1,2, HUANG Yan-Hong1,2, SHI Jian-Qi1,2, GUO Xin1,2
|
|
1.Software Engineering Institute, East China Normal University, Shanghai 200062, China;2.National Trusted Embedded Software Engineering Technology Research Center (East China Normal University), Shanghai 200062, China
|
| Abstract: |
| Airborne software is widely used in aerospace, which dramatically improves the performance of airborne equipment. Nevertheless, with airborne software's increasing scale and function, it is challenging to develop airborne software. How to ensure the correctness and safety of airborne software has become a difficult problem to be solved. Model-based development can effectively improve development efficiency, and formal methods can effectively guarantee the correctness of software. To reduce the difficulty of development and ensure airborne software's correctness and safety, this study proposes a hierarchical refinement modeling and verification method of airborne software using the SysML state machine diagram subset. Firstly, the SysML state machine diagram is used to model the dynamic behavior of airborne software. According to the proposed refinement rules, the initial model is refined to obtain the refined design model step by step manually. Then, according to the dynamic characteristics of the software model, the SysML state machine model is automatically converted to a network of timed automata, and the formal TCTL properties are manually extracted from the software requirements for model checking. Secondly, to realize coding automation, the SysML model is automatically converted to Simulink, and Simulink Coder generates the source code. Finally, an automatic flight control software is developed and verified based on the proposed method, and the experimental results show the effectiveness of the method. |
| Key words: airborne software model refinement model transformation model checking |
