基于MARTE的时序需求建模与分析验证技术研究

作     者：徐嘉 

作者单位：中国科学院大学(中国科学院国家空间科学中心) 

学位级别：硕士

导师姓名：周晴

授予年度：2022年

学科分类：08[工学] 0825[工学-航空宇航科学与技术] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：MARTE 嵌入式软件 时序分析 梯度下降算法 需求完整性验证 

摘      要：随着航天事业的迅速发展,嵌入式软件在航天整体系统设计、实现中的比重不断提高,繁重的任务需求进一步提升了航天嵌入式软件的规模及复杂度。时序是嵌入式软件的关键特性,时序正确决定了软件系统的稳定性。为了解决当前航天嵌入式软件时序需求复杂带来的时序需求定义不准确和需求分解不完整等问题,本文提出了一种基于MARTE模型的数据流时序模型,并在该模型的基础上设计了一种时序偏离检测分析算法和需求完整性验证算法,实现了一套时序需求分析验证系统,可以为软件设计师在需求分析阶段尽早开展软件时序分析验证工作。本文的具体工作如下:(1)由于航天嵌入式软件需求中包含了复杂的时序数据交互关系,传统的需求模型无法针对具有时序特性的数据流进行建模,因此,本文将传统数据流图和MARTE中的时序特性相融合,提出了一种基于MARTE模型的数据流时序模型。本模型将MARTE中时序模式融合入DFD的组件中,并在模型中增添数据优先级和事件触发的相关设计,重新构建元模型,使其满足航天嵌入式软件建模需求。(2)针对航天嵌入式软件需求时序需求复杂,需求人员很难发现定义的时序特性存在偏差的情况,本文提出了一种时序偏离检测分析算法,包含可达性分析、时序偏离概率计算、时序序列分析三个部分。软件系统中并不是所有的外部输入数据流通过系统后均可到达外部接口,为了进行后续时序偏离检测分析,首先需要进行可达性分析,找出所有可达外部输出且连接着数据汇点的数据流集合;时序偏离概率计算是依据软件需求通过模拟输入流的时序特性,计算匹配后输出流的时序特性,并将验证结果与期望时序特性进行比对,获得输出数据流的时序偏离概率。在上述的仿真模拟过程中,为了满足航天嵌入式软件中存在具有优先级数据的需求,在处理点模块中通过增添了优先队列和普通队列,来划分到达处理点的优先级和非优先级数据,并通过排队队列缓存输出流数据到达的时序信息,有利于后续的时序分析。时序序列分析采用基于梯度下降算法对上述得到的数据到达时序信息进行拟合,最终给出推荐的输出数据的时序特性,给需求分析人员作为时序改进的参考建议。(3)为了解决复杂需求在分解过程中易出现层级间信息不一致的问题,本文提出一种需求完整性验证算法。传统的模型一致性检查算法是针对数据流进行平衡性的检查,本算法在此基础上增添了节点的平衡性和正确性检查以及数据流的正确性检查,验证算法更全面。(4)设计并实现了面向航天嵌入式软件时序需求分析验证工具,实现以上算法,最终可以以XML文件形式导出含时间特性的数据流之间的依赖关系,可以为后续进一步开展形式化验证提供支持。将系统工具应用于真实的航天嵌入式软件需求中,通过时序偏离检测分析及需求完整性验证,表明本工具可有效帮助需求人员发现和改进时序偏离和需求分解不一致等问题。