中文摘要：

实时系统的延迟界限可以被表达为时间自动机（timed automata）模型的有界活性（bounded liveness）。为了解决有界活性在线（on-line）测试对于分布式状态和并发行为的观测能力，使之具备硬件在回路（hardware in the loop）环境中实时性能指标的测试能力，本项目针对安全关键性或任务关键性分布交换式互连系统，研究基于测试自动机的分布式在线测试原理，提出适用于分布式系统的互操作性测试验证方法，提出适用于运行时间（run-time）并发时序的监视方法，制定并完善验证、测试和监视自动化的框架方案；预期在 时间自动机与性能分析联合建模、交互环境模拟与模型状态观测、形式化模型与工作状态模型的运行时间等价 等方面取得关键性技术突破和新进展，开拓分布交换式互连系统有界活性在线检测的应用基础，为飞机、舰船等尖端嵌入式平台内部的实时通信与控制的综合化提供性能保证支持。

结论摘要：

本项目的研究适用于硬件在回路（hardware in the loop）条件下分布交换式互连系统并发实时行为的测试和监视，即将交换式节点及其流量的时序特性表达为时间自动机（time automata，TA）模型的有界活性问题，采用硬件逻辑实现的在线测试装置进行验证。经过对测试自动机模型和在线测试原理、互操作行为的有界活性测试验证方法、运行时间并发时序监视方法，以及分布交换式互连系统的自动化验证测试和监视方案的研究工作，取得的主要研究成果包括 (1) 给出TA模型与实时演算（Real-time Calculus，RTC）模型相结合的分布交换式互连系统建模方法；根据上述混合模型，提出了采用硬件实现的测试自动机进行在线测试的原理，明确了通过对动态生成的状态空间进行可达性搜索，随着带有时间约束的状态路径变化，如果违例状态总是不可达，就能保证系统的有界活性。 (2) 在测试实验中，给出采用可编程硬件实现的RTC分析模型到TA模型的接口转换方法，可以实现由多条阶梯函数逼近的输入流量到达曲线约束，用于生成速率约束（rate constrained，RC）的虚拟链路流量，作为被测分布交换式节点的激励源。 (3) 针对在线测试的并发时序采集和模型状态观测问题，给出了TA模型的时钟变量与可编程硬件时钟的适配方法，给出了TA模型中的二元同步信道、广播同步信道和全局变量的硬件逻辑对应方法，用以保证网络组件事件交互行为观测的正确性。 (4) 对于具有混合关键性的分布交换式互连系统，考虑时间触发（time triggered，TT）流量和RC流量的综合，给出自动化验证、测试和监视的方案框架，即根据RTC的演算结果产生测试所需的事件序列，对硬件实现的TA模型实例进行测试驱动；根据综合化网络的同步和容错机制，对于TT流量定时的正确性、RC流量突发度控制的正确性，以及TT消息与RC消息之间时间孔隙调度的正确性进行在线监视。在研究工作中，实现了分布交换式节点等实验原型装置，发展了流量整形中间件、时延抖动测试等实验方法，初步构建了以硬件在回路实验为主，基于端系统的虚拟链路测试为辅的实验环境。上述研究成果可用于解决互连系统的安全/任务关键性保证问题；例如采用“通信/监视对”对时间偏移量进行在线监测，可以预先发现RC消息对TT消息窗口的影响，用于完善时间触发以太网（TTE）的故障监测机制。