基于模型检验的分级调度系统参数生成方法
韩朴杰1, 翟正军1, 陆艳洪1, 李运喜2     
1. 西北工业大学 计算机学院, 陕西 西安 710072;
2. 航空工业 西安航空计算技术研究所, 陕西 西安 710068
摘要: 针对综合模块化航空电子(IMA)分级调度系统中的分区参数优化问题,提出了一种基于模型检验的参数生成方法。该方法结合了传统符号模型检验和统计模型检验(SMC)技术,构建一个通用的时间自动机网络来描述分级调度系统的时间行为,在确保系统可调度性的前提下,采用分布式遗传算法搜索具有最优处理器利用率的参数。其中,系统的可调度性约束表述为符号模型检验中的安全性属性和统计模型检验中的假设检验2种形式。相比广泛应用的响应时间分析模型,该方法的形式化模型具有更强的表达能力,能更精确地描述复杂系统特征。而且统计模型检验的引入缓解了传统模型检验的"状态空间爆炸"问题。参数生成实验表明该方法能够定位参数空间中的全局最优解。
关键词: 综合模块化航电    分级调度    参数生成    时间自动机    统计模型检验    分布式遗传算法    

随着现代微处理器计算能力的快速增长,分级调度(hierarchical scheduling)架构越来越广泛地被应用于航空电子系统的设计与开发[1]。该架构能够将多种类型的应用有效地集成于单一计算平台,并在不同应用之间提供时间分区隔离。综合模块化航空电子(integrated modular avionics, IMA)便采用了分级调度架构,其ARINC-653[2]标准定义了2级调度器及严格的时间分区机制[3]。在构建IMA分级调度系统的过程中,一个重要的问题是如何为每个时间分区合理配置处理器资源,在保证系统可调度性的前提下,最大程度地利用系统计算能力[4]

在分级调度系统中,时间分区的资源配置问题可定义为如何生成分区资源模型[5]的最优参数。ARINC-653标准采用周期资源模型(p, b)描述分区资源需求,其中p表示分区周期(partition period),b表示每周期的运行时间预算(partition duration)[2]。基于该模型,IMA分级调度系统的处理器资源配置问题可表述为求解每个分区的参数pb,使系统不仅满足实时任务和分区的时间约束,还具有最优的处理器利用率(processor utilization)[6]

根据系统可调度性约束的建模方法,可将相关工作分为两部分。其中一部分研究采用传统的响应时间分析(response time analysis)方法[7],为实时任务和分区构造最坏情况(worst-case)下的响应时间解析表达式,从而导出系统可调度性约束的解析模型,在此基础上使用特定的数学优化方法如线性规划[1, 4, 8]、几何规划[9]和迭代搜索[10-12]等求解目标参数。此类工作往往具有较低的计算复杂度,但缺乏对复杂实时任务的表达能力,易产生过于保守的最坏情况假设,造成计算资源的浪费。为克服此不足,另一部分工作采用形式化模型描述系统行为,通过模型检验等技术来验证系统的可调度性。相比解析模型,这些工作中的形式化模型,例如数理逻辑[13]、时间Petri网[3, 14-15]、线性混成自动机[16]和时间自动机[17-20],具有更强的表达能力,能够精确建模诸如资源共享、任务依赖和分区间通信等复杂系统特性。然而,相关的验证算法有着较高的计算复杂度,特别是模型检验技术会随着系统并发组件数量的增长,遭遇“状态空间爆炸(state space explosion)”问题[21]。为此,这些工作大都采用组合化方法[3, 16, 19],即单独分析每个分区并逐层组合为全局的可调度性结论,但该方法难以应用于存在分区间通信的实际系统。此外,这部分工作大多数只能根据经验使用穷举测试来搜索可行解,缺乏有效的优化方法。

针对上述问题,本文提出一种基于模型检验的参数生成方法,用于求解分级调度系统处理器资源配置的最优参数组合。该方法采用时间自动化精确的建模系统;通过组合传统模型检验和统计模型检验(statistical model checking, SMC),缓解了“状态空间爆炸”问题;在确保可调度性的前提下,使用分布式遗传算法高效地探索解空间,避免了穷尽搜索。

1 问题描述

本文考虑一个双层分级调度系统, 其全局-本地2级调度器均采用抢占式固定优先级(preemptive fixed priority)调度算法对时间分区或实时任务分配资源。设该分级调度系统运行于一个单处理器平台, 并由时间分区集合{Pi|i=1, 2, …, n}组成。分区Pi定义为一个四元组(pi, bi, ri, Γi)。其中, pi表示分区周期, bi代表分区预算, 它们组成了分区的周期资源模型(pi, bi); ri表示该分区的优先级, 通常由系统设计人员根据应用安全性需求预先指定; Γi表示分区Pi所包含的实时任务集合{τji |j=1, 2, …, mi}。这里采用开放式可扩展的任务定义。考虑最简单的周期任务类型, 任务τji定义为元组(Tji, Eji, Dji, Rji), 其中Tji表示任务周期, Eji代表运行时间, Dji为截止时间, Rji为任务优先级。

分级调度系统的可调度性约束包含两部分:①对于每个分区Pi, 全局调度器需保证在每个分区周期pi内分配预算运行时间bi; ②在任意分区Pi中, 本地调度器需确保每个实时任务τji在最后期限Dji前获得所需的运行时长Eji

定义分级调度系统的处理器利用率为

(1)

式中包含每个分区Pi的周期资源模型的待解参数pibici表示该分区每个周期内上下文切换的最大次数, v表示分区上下文切换的时间开销。

基于上述系统定义, 参数选择问题即求解参数向量(pi, bi)n, 使之满足系统的可调度性约束, 同时具有最小的处理器利用率U

2 系统建模 2.1 UPPAAL和时间自动机

UPPAAL是一个用于时间自动机建模和验证的集成工具环境, 包含多个基于不同形式化理论的变种[22]。其中经典UPPAAL实现了对时间计算树逻辑(TCTL)表达式的符号模型检验。UPPAAL SMC则采用了统计模型检验技术, 通过随机生成并监视系统的仿真过程, 得出统计意义上的结论[23]

时间自动机是一种包含时钟变量扩展的有限状态机。与有限状态机的结构类似, 时间自动机由一系列位置(location)节点及联结它们的边(edge)构成。它使用稠密时间模型, 其中所有的时钟变量均解析为实数值并同步增长, 用于表示连续特性。此外, UPPAAL还定义了有界整数类型用于表达离散状态。系统在任意时刻的状态(state)是由模型所处的位置、时钟变量和离散变量的值共同定义。复杂系统可建模为多个并发的时间自动机, 在它们之间使用通道(channel)进行同步和交互, 其状态是多个自动机状态的组合[24]

2.2 模型框架

根据分级调度系统的结构, 设计了如图 1所示的层次化模型框架。自顶向下分别是全局调度器模型、分区模型、本地调度器模型和实时任务的模型集合。在相邻的层次之间, 仅通过少数的通道进行交互, 实现了模块化的建模。如图 1中箭头所示, 该通道集合代表了层次间的调度命令和请求。

图 1 模型框架的结构图

针对分级调度系统的参数生成问题, 创建一个全局调度器实例、n个分区实例及其对应的n个本地调度器实例; 同时为分区中的每个实时任务创建一个实例。由于采用了开放式可扩展的实时任务定义, 用户只需遵守与本地调度器之间的通道语义, 便可定义新的实时任务模型来创建任务实例。为便于引用分区和任务, 定义整数类型pid-t和tid-t分别表示分区编号和任务编号。下面举例介绍建模框架中的全局调度器模型。

2.3 全局调度器模型

全局调度器使用抢占式固定优先级调度算法, 为所有的分区分配时间资源。它声明了一个分区就绪队列, 按照分区优先级从高到低将所有等待分配资源的就绪分区的编号插入队列中。该队列拥有一系列操作函数:函数enque和deque分别用于插入分区编号和移除队首元素; 函数front返回队首分区编号; 函数pqLen返回队列长度。

图 2所示, 全局调度器在初始时刻处于位置Idle, 当接收到某一分区n在就绪时所发送的pready通道输出时, 则调用函数enque将该分区编号插入就绪队列, 并迁移至Committed类型位置Schedule。由于UPPAAL不允许在Committed类型位置(内部标记符号C)上有时间流逝[24], 调度器会立即离开Schedule位置, 通过psched通道调度就绪队列的队首分区运行, 在变量curPart中记录当前运行分区, 然后迁移至位置Occupied。

图 2 全局调度器模型

在Occupied位置, 当接收到新就绪分区的pready通道输入时, 则将该分区的编号n插入就绪队列, 并转移至Preempt位置。此刻会立即判断就绪队列的队首元素是否仍旧为当前运行分区, 如是则返回Occupied位置继续运行, 否则执行抢占操作, 即通过pstop通道停止当前运行分区, 使用reset函数重置curPart变量, 并返回Schedule位置重新调度新的队首分区。

当运行的分区获得所需资源后, 它会向全局调度器发送prelease请求以释放处理器。此时, 模型自Occupied位置迁移至Release位置, 并从就绪队列中移除当前分区。在Release位置时, 若就绪队列为空, 则返回位置Idle等待新的就绪请求; 否则转移至位置Schedule再次执行调度。

3 参数生成方法 3.1 参数生成流程

参数生成的总体流程如图 3所示。该流程需要调用一个搜索算法, 用于发现和定位可行的解向量。由于复杂系统模型的导数信息通常难以求解, 这里采用启发式搜索算法来探索参数空间。在输入系统模型和搜索算法模块后, 便可启动参数生成流程。其主要操作步骤如下。

图 3 参数生成流程图

首先, 初始化一个迭代次数变量j=0。

1)由搜索算法根据参数定义域和在搜索过程中所获得的知识执行搜索并生成一个目标参数向量(pi, bi)n的集合Ωj

2) 为Ωj中每个参数向量创建独立的系统模型, 将分区周期和预算分别写入模型。

3) 调用UPPAAL SMC测试每个模型的可调度性并评估其处理器利用率。

4) 若Ωj所对应的模型集合经过SMC测试和评估后满足用户设定的终止条件, 例如达到处理器利用率阈值或搜索迭代次数上限, 则执行5);否则令j=j+1, 转向1)。

5)对Ωj中所有通过可调度性测试的参数向量及其模型, 调用经典UPPAAL符号模型检验器, 确认其可调度性。

6) 若Ωj中存在满足可调度性约束的参数向量, 则输出这部分参数向量作为解集, 结束执行; 否则令j=0, 转向1)。

3.2 可调度性验证

在参数生成过程中, 采用了符号模型检验和统计模型检验组合的方式来验证系统模型的可调度性。如图 4所示, 可调度性验证分为2个步骤。首先, 对每个录入目标参数的系统模型, 执行UPPAAL SMC的假设检验测试, 判断是否在较高置信度下满足可调度性属性。然后, 对于通过SMC测试的模型, 调用经典UPPAAL执行TCTL安全性属性验证, 从而确认模型的可调度性。

图 4 可调度性验证的步骤

由于统计模型检验采用了基于仿真的采样测试, 其计算复杂度远低于符号模型检验, 不但避免了对模型状态空间的穷尽搜索, 而且能够较快地发现违反时间约束的状态路径[23], 从而在参数搜索过程中提前排除了这部分无效参数。然而统计模型检验采样测试的本质, 使其无法严格地保证可调度性, 故此后仍需符号模型检验确认可调度性成立。

为了支持可调度性验证, 在系统模型中定义一个布尔变量e, 并添加e的更新操作:一旦系统违反时间约束, 则立即设置e为真。

1) 在UPPAAL SMC的可调度性测试中, 系统的可调度性表述为如下的假设检验公式:

(2)

表示违反约束的概率小于θ。其中M是仿真过程的时间限制, θ是一个较小的概率值(通常取值小于0.001)。

由于该统计模型检验的目的是“证伪”, 即排除不可调度的参数, 在假设检验中应尽可能降低第二类错误即“取伪”的概率β。因此, 为了提升可调度性验证的效率, 在假设检验中设定第二类错误概率β小于第一类错误概率α。例如设置典型的显著性水平α=0.05, β=0.01。

2) 当执行UPPAAL符号模型检验时, 系统的可调度性表述为TCTL安全性属性:

(3)

表示模型状态空间中的所有路径始终令e为假成立, 故通过该步骤能够严格地保证可调度性。

3.3 处理器利用率的评估

针对每个通过可调度性测试的参数向量及其模型, 使用UPPAAL SMC的期望值公式来评估系统的处理器利用率U, 即

(4)

该公式求解处理器利用率U最大值的期望Ue, 其中M是仿真过程的时间限制, N是仿真执行的次数。

在UPPAAL SMC中定义处理器利用率为

式中, pid-t是分区编号的类型; 变量ci, v, bipi分别存储了分区i的上下文切换次数、切换开销、预算和周期; K是一个常数因子, 用于将结果表示成UPPAAL SMC所能接受的整型数据。

3.4 搜索算法的选择

在参数生成流程中, 步骤1所采用的启发式搜索算法决定了参数空间的探索方向, 能够在每一次迭代中生成更优的参数向量集合。这里基于生物进化的思想实现该算法。由于对每个参数向量及其模型的处理相互独立, 可利用并行化的方式来加速整个参数生成流程。

考虑以上因素, 采用如图 5所示的分布式遗传算法。步骤如下。

图 5 分布式遗传算法中的数据流

1) 初始化:按照设定的参数取值范围随机生成一个包含X个个体的种群Φ0, 种群中的每个个体是一个候选参数向量。

2) 划分:将输入的种群Φj, j≥0平均划分为m个子种群{Φjk |k=1, …, m}。分别对每个子种群Φjk, 执行3)~ 5)。

3) 交叉:使用交叉算子(crossover operator), 重组Φjk'中个体的参数值, 生成新个体的集合Φjk。所有子种群共生成X′个新个体。

4) 变异:调用变异算子(mutation operator), 改变Φjk′中的每个个体的参数值, 映射Φjk′为Ωjk

5) 输出:输出种群Ωj={Ωj1, Ωj2, …, Ωjm}中的各个子种群, 由3.1节所述流程中的步骤2)继续执行。

6) 合并:合并种群Ωj={Ωj1, Ωj2, …, Ωjm}的可调度性验证和处理器利用率评估的结果。

7) 适应度计算:根据可调度性验证和处理器利用率评估的结果, 计算种群Ωj中所有个体的适应度。

8) 选择:使用选择算子(selection operator)对种群Ωj执行选择操作, 筛选出一个包含X个个体且适应度更高的种群Φj+1, 转向2)。

适应度函数F:IN映射个体空间I至自然数, 用于评价个体的优劣, 更高的适应度代表更优的目标参数。其定义为

(6)

式中, K是3.3节中的常数因子, c是个体所对应可调度性的整型真值(即可调度为1, 不可调度为0), Ue是处理器利用率的期望值。

4 参数生成实验 4.1 实验方案

本文使用文献[11]中的2个实时任务集, 组成2个不同的分级调度系统, 分别开展参数生成实验。表 1给出了2组实验的实时任务集。表中分区的优先级与其分区编号相同。更小的优先级值代表更高的优先级。分区的上下文切换时间设为2个时间单位。

表 1 实时任务集
任务 分区 周期 运行时间 截止时间 任务优先级
Tsk11 1 50 5 50 1
Tsk21 1 125 7 125 2
Tsk31 1 300 6 300 3
Tsk12 2 50 5 50 1
Tsk22 2 125 7 125 2
Tsk32 2 300 6 300 3
Tsk13 3 160 8 100 1
Tsk23 3 240 12 200 2
Tsk33 3 320 16 300 3
Tsk43 3 480 24 400 4
Tsk14 4 160 8 100 1
Tsk24 4 240 12 200 2
Tsk34 4 320 16 300 3
Tsk44 4 480 24 400 4

1) 实验1:针对分区1和分区2所组成的分级调度系统执行参数生成操作。设置分区周期的取值范围为[5, 100], 精度为0.5个时间单位; 设定搜索算法的迭代次数上限为200, 种群容量X=64;配置UPPAAL的模型检验搜索顺序为“广度优先”, 假设检验的时间限制M=1.0×105, 概率上限θ=0.001, 期望值评估的仿真次数N=100, 因子K=10 000。

2) 实验2:针对分区3和分区4所组成的分级调度系统执行参数生成操作。设定分区周期的取值范围为[5, 200], 假设检验的时间限制M=2.0×105, 其他配置均与实验1相同。

在每个实验中, 使用表 2的4种算子组合逐一运行参数生成程序, 以确定适合该方法的算子配置。表中算子的详细定义可参考文献[25]。G1和G2采用了基于二进制值(binary valued)的交叉/变异算子。G3和G4采用了基于实值(real valued)的交叉/变异算子。

表 2 实验中的算子组合
序号 交叉算子 变异算子 选择算子
G1 均匀交叉 倒位变异 赌轮选择
G2 均匀交叉 倒位变异 锦标赛选择
G3 中间重组 高斯变异 锦标赛选择
G4 中间重组 高斯变异 截断选择

其中, 中间重组(intermediate recombination)算子的后代区域因子d=0.5, 高斯变异(gaussian mutation)算子的标准差σ=10, 锦标赛选择(tournament selection)算子的锦标赛容量S=2, 截断选择(truncation selection)算子的截断比例

4.2 结果分析

表 3表 4分别展示了实验1和实验2的参数生成结果。在2个实验中, 算子组合G3和G4所生成的目标参数向量与文献[11]中使用穷尽搜索方法所得的全局最优解相同, 达到了最小的处理器利用率值。相比之下, 算子组合G1和G2均未能定位最优参数, 所输出参数的处理器利用率明显大于G3和G4。而且, 从实验1到实验2, 随着搜索空间的增大, 算子组合G1和G2所生成的参数与G3和G4相比, 处理器利用率的差距会进一步地增大。可见, 中间重组算子和高斯变异算子的组合更适用于分级调度系统的参数生成操作, 能够有效定位具有较优处理器利用率的目标参数。

表 3 实验1的结果
序号 目标参数向量 处理器利用率/% 是否最优
G1 (51.5, 10.5, 52, 10.5) 48.3
G2 (52.5, 12, 54, 11.5) 51.66
G3 (50, 9.5, 50, 9.5) 46
G4 (50, 9.5, 50, 9.5) 46
表 4 实验2的结果
序号 目标参数向量 处理器利用率/% 是否最优
G1 (159.5, 53.5, 165, 64.5) 75.09
G2 (160.5, 48.5, 156.5, 69) 78.10
G3 (160, 34.5, 160, 34.5) 45.62
G4 (160, 34.5, 160, 34.5) 45.62

图 6显示了在实验过程中每一代种群的最优处理器利用率期望值Ue与迭代次数j的对应关系。从图中处理器利用率的演变过程可见, 两个实验中的算子组合G1和G2均在迭代次数j < 100时过早地收敛至某个局部最优解。这是因为基于二进制值的交叉/变异算子对本文问题解空间的搜索效率较低, 在进化过程中仅能随机地生成少数几个具有高适应度的新个体, 之后这些优势个体便很快地在种群中占据绝对的比重, 种群的多样性(diversity)迅速降低, 最终令种群丧失了进化能力, 从而使优化结果过早地收敛于随机的局部最优解。这种早熟收敛(premature convergence)现象[25]在实验2的搜索空间扩大后变得更为明显, 导致算子组合G1和G2难以充分优化系统的处理器利用率。

图 6 实验中处理器利用率的演变过程

相比之下,算子组合G3和G4所采用的基于实值的交叉/变异算子组合具有更好的搜索效率,能够持续产生更多的优势个体,最终达到了相同的全局最优解。这2个算子组合仅使用不同的选择算子,但仍导致图 6中的处理器利用率有着不同的演变过程:由于G3所采用的锦标赛选择算子比G4的截断选择算子具有更高的选择压力(selectivepressure),G3比G4总体上具有更快的收敛速度,但这也增大了G3早熟收敛的风险。因此,在实践中可组合使用2种选择算子开展参数生成任务,从而令搜索算法在选择压力和种群多样性之间取得平衡。

5 结论

为解决综合化航电分级调度系统的处理器资源配置问题,提出了一种基于模型检验的分区资源模型参数生成方法,它在确保系统可调度性的基础上,进一步优化了系统的处理器利用率。相比传统的解析模型,该方法所构建的时间自动机模型更精确地建模了ARINC-653分级调度系统的双层调度器结构及其行为。通过结合符号模型检验与统计模型检验,避免了对模型状态空间进行穷尽搜索,缓解了传统模型检验的“状态空间爆炸”问题。该方法所采用的分布式遗传算法能够在缺乏系统导数信息的情况下引导参数空间搜索,定位具有最优处理器利用率的参数;同时采用并行化的算法设计,加速了参数生成过程。本文的参数生成实验均在200次迭代之内发现了最优解。

下一步的研究主要包括任务模型集合的完善,复杂IMA系统的建模,以及针对复杂IMA系统的参数优化算法设计等。

参考文献
[1] BLIKSTAD M, KARLSSON E, LÖÖW T, et al. An Optimisation Approach for Pre-Runtime Scheduling of Tasks and Communication in an Integrated Modular Avionic System[J]. Optimization and Engineering, 2018, 19(4): 977-1004. DOI:10.1007/s11081-018-9385-6
[2] Airlines Electronic Engineering Committee. Avionics Application Software Standard Interface: Part 1-Required Services[S]. ARINC Specification 653 P1-4, 2015
[3] CARNEVALI L, PINZUTI A, VICARIO E. Compositional Verification for Hierarchical Scheduling of Real-Time Systems[J]. IEEE Trans on Software Engineering, 2013, 39(5): 638-657. DOI:10.1109/TSE.2012.54
[4] KIM J E, ABDELZAHER T, SHA L. Schedulability Bound for Integrated Modular Avionics Partitions[C]//Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2015: 37-42
[5] SHIN I, LEE I. Periodic Resource Model for Compositional Real-Time Guarantees[C]//Real-Time Systems Symposium, 2003: 2-13
[6] LIPARI G, BINI E. A Methodology for Designing Hierarchical Scheduling Systems[J]. Journal of Embedded Computing, 2005, 1(2): 257-269.
[7] ALMEIDA L, PEDREIRAS P. Scheduling within Temporal Partitions: Response-Time Analysis and Server Design[C]//Proceedings of the 4th ACM International Conference on Embedded Software, 2004: 95-103
[8] ZHANG L, GOSWAMI D, SCHNEIDER R, et al. Task-and Network-Level Schedule Co-Synthesis of Ethernet-Based Time-Triggered Systems[C]//19th Asia and South Pacific Design Automation Conference, 2014: 119-124
[9] YOON M K, KIM J E, BRADFORD R, et al. Holistic Design Parameter Optimization of Multiple Periodic Resources in Hierarchical Scheduling[C]//Proceedings of the Conference on Design, Automation and Test in Europe, 2013: 1313-1318
[10] DAVIS R, BURNS A. An Investigation into Server Parameter Selection for Hierarchical Fixed Priority Pre-Emptive Systems[C]//16th International Conference on Real-Time and Network Systems, 2008
[11] DEWAN F, FISHER N. Approximate Bandwidth Allocation for Fixed-Priority-Scheduled Periodic Resources[C]//Real-Time and Embedded Technology and Applications Symposium, 2010: 247-256
[12] DEWAN F, FISHER N. Fixed-Priority Schedulability of Arbitrary-Deadline Sporadic Tasks upon Periodic Resources[C]//IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, 2012: 358-367
[13] BEJI S, HAMADOU S, GHERBI A, et al. SMT-Based Cost Optimization Approach for the Integration of Avionic Functions in IMA and TT Ethernet Architectures[C]//Proceedings of the 2014 IEEE/ACM 18th International Symposium on Distributed Simulation and Real Time Applications, 2014: 165-174
[14] CARNEVALI L, LIPARI G, PINZUTI A, et al. A Formal Approach to Design and Verification of Two-Level Hierarchical Scheduling Systems[C]//International Conference on Reliable Software Technologies, 2011: 118-131
[15] CICIRELLI F, FURFARO A, NIGRO L, et al. Development of a Schedulability Analysis Framework Based on PTPN and UPPAAL with Stopwatches[C]//Proceedings of the 2012 IEEE/ACM 16th International Symposium on Distributed Simulation and Real Time Applications, 2012: 57-64
[16] SUN Y, LIPARI G, SOULAT R, et al. Component-Based Analysis of Hierarchical Scheduling Using Linear Hybrid Automata[C]//20th International Conference on Embedded and Real-Time Computing Systems and Applications, 2014: 1-10
[17] SBERG M, PETTERSSON P, NOLTE T. Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling[C]//23rd Euromicro Conference on Real-Time Systems, 2011: 172-181
[18] AHN S J, HWANG D Y, KANG M, et al. Hierarchical System Schedulability Analysis Framework Using UPPAAL[J]. IEICE Transactions on Information and Systems, 2016, 99(8): 2172-2176.
[19] HAN P, ZHAI Z, NIELSEN B, et al. A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems[C]//International Workshop on Methods and Tools for Rigorous System Design, 2018: 39-51
[20] BOUDJADAR A, KIM J H, LARSEN K G, et al. Compositional Schedulability Analysis of An Avionics System Using UPPAAL[C]//International Conference on Advanced Aspeots of Softuare Engineering, 2014: 140-147
[21] PELED D A. Software Reliability Methods[M]. New York: Springer Science & Business Media, 2013.
[22] UPPSALA University, AALBORG University. UPPAAL Home[EB/OL]. (2015-6-2)[2018-7-1]. http://www.uppaal.org/.
[23] DAVID A, LARSEN K G, LEGAY A, et al. UPPAAL SMC Tutorial[J]. International Journal on Software Tools for Technology Transfer, 2015, 17(4): 397-415. DOI:10.1007/s10009-014-0361-y
[24] DAVID G B A, LARSEN K G. A Tutorial on UPPAAL 4.0[J]. Department of Computer Science, 2006, 4(12): 200-236. DOI:10.1007/978-3-540-30080-9_7
[25] BÄCK T, FOGEL D B, MICHALEWICZ T. Evolutionary Computeation 1:Basic Algorithns and Operators[M]. New York: CRC Press, 2018.
Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking
HAN Pujie1, ZHAI Zhengjun1, LU Yanhong1, LI Yunxi2     
1. School of Computer Science and Engineering, Northwestern Polytechnical University, Xi'an 710072, China;
2. Xi'an Aeronautics Computing Technique Research Institute, AVIC, Xi'an 710068, China
Abstract: A parameter generation method based on model checking is proposed to tackle the parameter selection of hierarchical scheduling systems in Integrated Modular Avionics (IMA) by combining the classical symbolic model checking and the Statistical Model Checking(SMC). It builds a generic timed automata network to describe the temporal behavior of hierarchical systems. A distributed genetic algorithm is adopted to search the optimum partition parameters with respect to processor utilization while guaranteeing the schedulability of the system, which is formulated as safety properties of symbolic model checking and hypothesis testing of SMC. Comparing with the widely-used response time analysis, the formal model of this method is more expressive to cover complex features. The application of SMC alleviates the "state space explosion" of classical model checking. Finally, the parameter generation experiments show that the present method is able to find the global optimum solutions in the parameter space.
Keywords: integrated modular avionics    hierarchical scheduling    parameter generation    timed automata    statistical model checking    distributed genetic algorithm    
西北工业大学主办。
0

文章信息

韩朴杰, 翟正军, 陆艳洪, 李运喜
HAN Pujie, ZHAI Zhengjun, LU Yanhong, LI Yunxi
基于模型检验的分级调度系统参数生成方法
Parameter Generation for Hierarchical Scheduling Systems Based on Model Checking
西北工业大学学报, 2019, 37(6): 1302-1309.
Journal of Northwestern Polytechnical University, 2019, 37(6): 1302-1309.

文章历史

收稿日期: 2018-12-21

相关文章

工作空间