南京航空航天大学计算机科学与技术学院 程　桢



基于MARTE的IMA系统时间资源可调度配置验证

南京航空航天大学计算机科学与技术学院 程桢

【摘要】目前综合模块化航空电子系统（IMA）在资源配置方面有非常高的安全可靠性需求，其中时间资源的可调度性配置验证也显得至关重要。本文在AFDX网络架构下提出了一种IMA系统时间相关概念的MARTE建模和时间资源可调度配置的正确性验证方法。建立了IMA系统通信虚拟链路、AFDX终端、分区以及进程等相关元素到MARTE模型元素的建模规则，并设计了基于可调度分析工具MAST的时间资源可调度配置验证框架，最后利用相关实例进行仿真和分析得到验证结果。

【关键词】综合航电系统；模型驱动工程；MARTE；系统资源配置

随着航空领域系统日益复杂的发展趋势，综合模块化航空电子系统（Integrated Modular Avionics, IMA）[1]已广泛应用于机载航空电子系统。资源共享是IMA系统典型的特征，如何确保IMA系统开发过程中时间资源配置的安全性显得至关重要，也成为近年来航空电子系统工程领域的一个重要挑战。文献[2]主要基于单个IMA系统对资源的配置文件信息进行建模转换与验证，没有考虑实际情况中的AFDX网络，文献[3]给出了如何在任务时间需求函数的基础上去计算系统所消耗的时间,并得出了系统可调度性的判定定理。文献[4]详细介绍了本文所利用的MARTE建模语言。本文从时间资源验证角度，提出了一种AFDX网络架构下IMA系统的建模方法以及时间资源验证框架，基于模型驱动的方法对时间资源的可调度性进行了正确性验证。……