片间综合化互连时间触发通信调度方法

未来先进的分布式综合化航空电子系统需要实现跨越计算体系结构的信息综合,对微小型智能器件间的综合化互连提出要求。通过构建一种具有开放式接口的芯片间综合化互连结构,提出一种相应的时间触发（TT）通信调度方法。首先建立片间综合化互连模型和时间触发流量传输模型,给出负载均衡的选径方法;随后依据传输路径中各级节点各流量的发送时间偏移量计算流量传输的等待时间可行值,利用遗传算法优化调整各芯片发送端口的调度表相位,更新各流量在发送端口的时间偏移量,缩短最坏情况下的最大等待时间,得到具有全局优化意义的时间触发调度表。与使用Yices等SMT形式化求解器的TT调度表生成方法相比,本方法不会出现长时间不停机而无法判定的问题,且不论对于对称或非对称结构,案例研究表明本方法的可调度规模至少增加30%。此外,以流量传输等待时间占周期的比例作为归一化的传输延迟度量,与既有的基于特征任务的调度方法相比,案例研究表明本方法得到的传输延迟最多仅为后者的2%。     

时间触发以太网拜占庭容错方法的形式化验证

对于时间触发以太网的拜占庭容错方法,已有的推理性论证表明网络的分布式时钟同步机制有利于容错过程中实现交互一致性。为对该容错方法的正确性进行严格验证,进一步采用模型检查的形式化分析手段,通过符号分析实验室(SAL)形式化工具,构建了网络节点模型,建立了时间触发体系结构下的拜占庭容错场景,设定了容错操作活性、一致性和有效性等属性的形式化定理。模型检查的结果表明:在三冗余独立路径条件下,该方法可以容忍一个拜占庭故障,且在存在指令/监视对(COM/MON pair)的条件下可以容忍2个高完整性配置节点的"不一致遗漏"故障。与推理论证手段相比,SAL模型检查为时间触发交换式网络在航空航天高安全关键等级系统中的容错配置提供了更规范的依据。