综合模块化航空电子多约束分区调度方法

摘要

在综合模块化航空电子系统(integrated modular avionics,IMA)中,采用严格的空间和时间分区管理(partitioning)保证同一个模块上运行的不同应用可以共享处理资源。根据系统硬件资源和应用的要求,定义分区的多类型约束条件,使得分区到在各个模块上的分配和时分访问调度成为复杂的组合优化问题。通过将分区分配的预处理与满足性模理论(satisfiability modulo theories,SMT)求解调度表的方法相互结合,可以减少断言式和分区调度时刻变量的数量,提高求解效率;其中,预处理过程采用最大独立团算法,随后将剩余的分区约束条件转换成SMT工具可识别的逻辑表达式,形式化求解得到各个分区的调度时刻。通过规模不同的算例,验证了该方法可行性,并说明预处理过程对于快速判断满足性要求和缩短求解时间的好处。