近日，公司周建涛教授课题组的一项研究成果“A Verification Framework for Time-triggered Networks based on Timed Colored Petri Net”被计算机辅助设计领域顶级国际学术期刊《IEEE Transactions on Computer-Aided Design of Integrated Circuits And System(TCAD)》正式录用（DOI:  10.1109/TCAD.2024.3355708）。TCAD是集成电路与系统计算机辅助设计领域国际公认的最顶尖学术期刊，也是中国计算机学会（CCF）认定的A类期刊。该期刊主要关注包括模拟信号、数字信号和混合信号等在内的集成电路和计算机辅助设计领域最新的研究进展和技术，对原创性、算法方法以及理论研究等方面都有极高的要求，收录了所在领域的顶级研究成果。这是公司软件工程学科在TCAD上发表的首篇论文。

第四次工业革命正在推动传统产业向数字化、网络化、智能化快速转型，标准以太网使用best-effort(BE)策略来传输消息帧，缺乏对工业控制任务的时间关键性考虑。时间触发(Time-Triggered，TT)网络能够解决时间关键消息的通信问题，但是时间触发消息的传输时延形成更为复杂且更难以控制。论文提出一种基于时间着色Petri网（Timed Colored Petri Net, TCPN）的验证框架，能够为时间触发消息帧的传输提供一种形式化的仿真及可达性分析的集成方法。

图1基于TCPN的TT网络验证框架图

该验证框架使用TCPN对消息在TT网络集群（图1a）的传输行为建模。形式模型（Formal Model）包含三种行为模型，分别是消息帧模型（Frame Model）、消息发送模型（Message Sending Model）和链路模型（Link Model）。验证框架（图1 b）在形式模型上动态仿真（Dynamic Simulaiton）消息传输，直观地检测TT消息传输正确性；模型生成的状态空间（State Space）用于实现可达性分析（Reachability Analysis），例如边界属性、活性属性以及其他用户自定义的时间相关属性。该框架包含基于TCPN的自动建模方法，并且通过状态空间上的关键性属性验证实现了消息传输行为的全局评估，对时间触发网络消息传输问题以及形式化建模、仿真和可达分析方法领域问题的研究具有重要参考价值。 

论文通讯作者为公司周建涛教授，第一作者为学院在读博士研究生钟文杰。钟文杰自本科起即在公司就读，是公司自主培养的博士研究生。 

论文在线访问地址：https://ieeexplore.ieee.org/document/10404013