论文部分内容阅读
在综合模块化航空电子系统(integrated modular avionics,IMA)中,采用严格的空间和时间分区管理(partitioning)保证同一个模块上运行的不同应用可以共享处理资源。根据系统硬件资源和应用的要求,定义分区的多类型约束条件,使得分区到在各个模块上的分配和时分访问调度成为复杂的组合优化问题。通过将分区分配的预处理与满足性模理论(satisfiability modulo theories,SMT)求解调度表的方法相互结合,可以减少断言式和分区调度时刻变量的数量,提高求解效率;其中,预处理过程采用最大独立团算法,随后将剩余的分区约束条件转换成SMT工具可识别的逻辑表达式,形式化求解得到各个分区的调度时刻。通过规模不同的算例,验证了该方法可行性,并说明预处理过程对于快速判断满足性要求和缩短求解时间的好处。
In integrated modular avionics (IMA), strict space and time partitioning is used to ensure that different applications running on the same module can share processing resources. According to the system hardware resources and application requirements, the definition of multi-type partition constraints, making the partition to each module in the allocation and time-based access scheduling becomes a complex combinatorial optimization problem. By combining partition pre-processing and satisfiability modulo theories (SMT) to solve the schedule, the number of predicate-type and partition-scheduling time variables can be reduced and the solution efficiency can be improved. The preprocessing process uses the largest Independent group algorithm, then the remaining partition constraints into SMT tools can identify the logical expression, the formal solution to each partition scheduling time. Through the examples with different scales, the feasibility of this method is verified and the benefits of the preprocessing process for quickly assessing the satisfaction and shortening the solution time are illustrated.