计算机科学与探索 ›› 2015, Vol. 9 ›› Issue (4): 385-402.DOI: 10.3778/j.issn.1673-9418.1408014
胡 军1,2+,马金晶1,刘 雪1,程 桢1,石娇洁1,黄志球1
HU Jun1,2+, MA Jinjing1, LIU Xue1, CHENG Zhen1, SHI Jiaojie1, HUANG Zhiqiu1
摘要: 近年来,在以综合模块化航电系统(integrated modular avionics,IMA)为代表的一类安全关键应用中,确保系统重配置信息的正确性成为保证系统安全可靠运行的一个重要问题。提出了一种模型驱动架构下符合ARINC653规范的IMA系统配置信息的建模转换与验证方法。针对多个实时应用在IMA平台上以时间/空间多分区形式运行的系统特征,建立了从系统配置信息的核心元素(包括模块、分区、内存、进程、通信等)到MARTE模型元素的语义映射规则,设计了基于模型驱动架构的系统配置信息模型转换的方法,并给出了一种对模型转换构造得到的系统配置信息MARTE模型进行形式化验证的框架。最后,通过一个实例分析说明了此方法对验证重配置后系统配置信息的有效性。