● 摘要
综合模块化航空电子系统（IMA），目前已经在军用和民用领域得到了一定范围的应用，与传统的分布式航空电子系统相比，综合模块化航空电子系统具备多变性和可重用性的特点，硬件资源和软件资源，在IMA系统中可以实现共享。IMA系统中分区的设计不仅能够使新一代航空电子系统的重量和花费大大减少，同时也能够有效的提高航空电子系统的灵活性和重用性。功能重构作为IMA系统的最重要特点之一，就体现了IMA系统的灵活性。
为了对IMA系统中软件功能重构的正确性进行验证，本文提出了一种针对IMA软件功能重构的建模与验证方法。本文首先对IMA软件功能重构的相应文献进行了调研，给出了IMA软件功能重构所需的要素，通过分区模式转换、进程状态转换、通信、资源分配和时序五个角度，作为描述IMA软件功能重构的基本要素。随后，针对IMA软件功能重构执行过程中的特点，提出了IMA软件功能重构建模的方法，将重构过程拆分为构件、构件的状态、状态转移的条件和状态转移的行为完成建模。接下来，选取AADL语言作为建模语言，结合AADL语言的基本语法，配以ARINC 653附件和行为附件，完成AADL语言对IMA软件功能重构的建模。然后，提出了由AADL模型向时间自动机模型转换的规则，完成两种模型之间的转换。最后选用UPPAAL作为工具，对时间自动机模型的可达性、无死锁和实时性进行验证，从而完成对IMA软件功能重构的验证。
基于上述方法，本文选用了某IMA系统中软件功能重构案例作为实例，验证了方法的正确性。