Timed automata for metric interval temporal logic formulae in prototype verification system

Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.

基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。

COMPLEXITY ANALYSIS OF TIME SERIES GENERATED BY ELEMENTARY CELLULAR AUTOMATA

Using the tools of distinct excluded blocks, computational search and symbolic dynamics, the classification problem of all 256 elementary cellular automata is discussed from the point of view of time series generated by them,and examples in each class are provided to explain the methods used.

Steady state speed distribution analysis for a combined cellular automaton traffic model

Cellular Automaton （CA） based traffic flow models have been extensively studied due to their effectiveness and simplicity in recent years. This paper develops a discrete time Markov chain （DTMC） analytical framework for a Nagel-Schreckenberg and Fukui Ishibashi combined CA model （W^2H traffic flow model） from microscopic point of view to capture the macroscopic steady state speed distributions. The inter-vehicle spacing Maxkov chain and the steady state speed Markov chain are proved to be irreducible and ergodic. The theoretical speed probability distributions depending on the traffic density and stochastic delay probability are in good accordance with numerical simulations. The derived fundamental diagram of the average speed from theoretical speed distributions is equivalent to the results in the previous work.

基于TAS-TIS结构和前馈路径的两级CTLE的设计

在高速接口电路中,接收机通常采用连续时间线性均衡器(Continuous-Time Linear Equalizer,CTLE)消除符号间干扰(Inter-Symbol Interference,ISI)对信号传输的影响。为提高CTLE电路的高频增益和减少芯片面积,基于UMC(United Microelectronics Corporation)28 nm工艺,设计了一款最大速率为50 Gbps的CTLE电路,其主体电路由跨导级联跨阻抗(Trans-Admittance Trans-impedance,TAS-TIS)结构和前馈路径的两级CTLE电路构成。在传统CTLE的基础上,使用有源电感做负载,以反相器为基础构建跨阻放大器和在输入管增加前馈通路等方式,有效地扩展了电路的工作频率。仿真结果显示,均衡后40 Gbps PAM4(4-Level Pulse Amplitude Modulation)信号、50 Gbps PAM4信号和28 Gbps NRZ(Non Return Zero Code)信号的眼图眼宽分别达到了0.68,0.5,0.92个码元间隔(UI),可满足后级电路对于输入信号的要求,对提升整体传输数据速率具有重要的意义。

Simulated and experimental investigation on discontinuous dynamic recrystallization of a near-α TA15 titanium alloy during isothermal hot compression in βsingle-phase field

A cellular automaton（CA） modeling of discontinuous dynamic recrystallization（DDRX） of a near-α Ti-6Al-2Zr-1Mo-1V（TA15） isothermally compressed in the β single phase field was presented.In the CA model,nucleation of the β-DDRX and the growth of recrystallized grains（re-grains） were considered and visibly simulated by the CA model.The driving force of re-grain growth was provided by dislocation density accumulating around the grain boundaries.To verify the CA model,the predicted flow stress by the CA model was compared with the experimental data.The comparison showed that the average relative errors were10.2%,10.1%and 6%,respectively,at 1.0,0.1 and 0.01 s^-1 of 1020 ℃,and were 10.2%,11.35%and 7.5%,respectively,at 1.0,0.1and 0.01 s^-1 of 1050 ℃.The CA model was further applied to predicting the average growth rate,average re-grain size and recrystallization kinetics.The simulated results showed that the average growth rate increases with the increasing strain rate or temperature,while the re-grain size increases with the decreasing strain rate;the volume fraction of recrystallization decreases with the increasing strain rate or decreasing temperature.

一种基于二级队列调度的时间敏感网络帧抢占机制

作为工业以太网、无人驾驶、航空电子等网络应用场景的核心技术之一,基于以太网的时间敏感网络(Time Sensitive Network,TSN)能够提供低时延、低抖动的确定性传输服务,一直以来广为业界关注。TSN流量调度是解决帧传输的确定性和有界时延问题的关键技术,其中帧抢占技术通过对不同实时性要求的数据进行划分且允许高优先级实时数据打断低优先级非实时数据的传输,来保证TSN网络中高优先级实时数据的超低时延。然而,帧抢占机制设置“保护带”以隔离高低优先级两类数据的传输,导致在保护带内网络链路空闲。本文针对保护带引起的链路带宽损耗问题,对帧抢占机制进行改进,提出一种基于二级队列调度(Two-Level Queue Scheduling,TLQS)的帧抢占机制。该机制通过设置两组队列,将经过基于门控的时间感知整形机制(Time-Aware Shaper,TAS)调度的非实时数据进行分流、存储与仲裁调度,并利用保护带闲置带宽进行传输选择。仿真结果表明,相较于使用标准帧抢占机制,基于TLQS的帧抢占机制在降低抢占产生的额外开销的基础上,能够有效提升网络带宽利用率。

Tenax TA对甲苯吸附脱附性能的研究

以甲苯为研究对象,通过动态吸附实验研究Tenax TA的吸附性能,考察进口浓度、流量和湿度对吸附性能的影响;通过热再生法研究Tenax TA的脱附性能,考察温度和再生次数对脱附性能的影响。结果表明,Tenax TA的抗湿性能和再生性能突出,相对湿度90%的吸附能力为干燥时的85%以上,再生200次后再生效率在95%以上。实验结果表明,Tenax TA可用于高湿度且对再生性能要求高的特殊环境中有机物的去除。

紫外脉冲激光烧蚀沉积Ta_2O_5薄膜过程的研究

对３５５ｎｍ激光烧蚀沉积Ｔａ２Ｏ５薄膜的过程进行了研究。由时间分辨四极质谱测得烧蚀Ｔａ２Ｏ５产生的正离子有Ｔａ＋、Ｏ＋、ＴａＯ＋和ＴａＯ＋２，中性粒子有Ｏ、Ｔａ、ＴａＯ和ＴａＩＯ２，并测定了它们的飞行时间（ＴＯＦ）谱。在不同压强的Ｏ２气氛下，由测得的时间分辨发光光谱表明，烧蚀产物在向基片飞行过程在发生了氧化反应。对沉积薄膜的组成分析表明，钽及其氧化物在基片上存在进一步氧化过程。

1998～2000年TA(CSAO)的保持与UTC(CSAO)的控制

中国科学院陕西天文台 (CSAO)用 6台新的HP50 71A商品小铯钟保持的时间尺度已有三年多了。在此期间 ,我们做了系统重算、TA(CSAO)算法改进、GPS坐标修正等一系列工作 ,使得TAI -TA(CSAO)的稳定度逐年提高 ,进入世界先进水平 ,同时陕台的UTC(CSAO)控制水平也达到了国际电联建议标准 ,与国际协调时UTC的差控制在± 1 0 0ns以内 。

Qualitative analysis for state/event fault trees using formal model checking

A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.

RFID Complex Event Processing: Applications in Real-Time Locating System

Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS.

The Approximation of Bosonic System by Fermion in Quantum Cellular Automaton

In one-dimensional multiparticle Quantum Cellular Automaton (QCA), the approximation of the bosonic system by fermion (boson-fermion correspondence) can be derived in a rather simple and intriguing way, where the principle to impose zero-derivative boundary conditions of one-particle QCA is also analogously used in particle-exchange boundary conditions. As a clear cut demonstration of this approximation, we calculate the ground state of few-particle systems in a box using imaginary time evolution simulation in 2nd quantization form as well as in 1st quantization form. Moreover in this 2nd quantized form of QCA calculation, we use Time Evolving Block Decimation (TEBD) algorithm. We present this demonstration to emphasize that the TEBD is most natu-rally regarded as an approximation method to the 2nd quantized form of QCA.

Solution of the Time Dependent Schrodinger Equation and the Advection Equation via Quantum Walk with Variable Parameters

We propose a solution method of Time Dependent Schr?dinger Equation (TDSE) and the advection equation by quantum walk/quantum cellular automaton with spatially or temporally variable parameters. Using numerical method, we establish the quantitative relation between the quantum walk with the space dependent parameters and the “Time Dependent Schr?dinger Equation with a space dependent imaginary diffusion coefficient” or “the advection equation with space dependent velocity fields”. Using the 4-point-averaging manipulation in the solution of advection equation by quantum walk, we find that only one component can be extracted out of two components of left-moving and right-moving solutions. In general it is not so easy to solve an advection equation without numerical diffusion, but this method provides perfectly diffusion free solution by virtue of its unitarity. Moreover our findings provide a clue to find more general space dependent formalisms such as solution method of TDSE with space dependent resolution by quantum walk.

考虑车队速度反馈机制的高速公路事故区交通流仿真研究

针对高速公路事故瓶颈处拥堵严重的问题,提出利用自动驾驶车队进行速度控制,以缓解交通拥堵,提升安全性.首先,基于车联网(Vehicle-to-Everything,V2X)技术中的基本安全信息(Basic Safety Message,BSM)数据,设计高速公路事故瓶颈处网联自动驾驶车速度反馈机制.其次,构建考虑车队速度反馈机制的元胞自动机模型,引入考虑通行优势的多车道换道模型,以更加真实地刻画车辆在事故区的换道行为.最后,基于提出模型,对低、中、高3类交通量等级和封锁车道、区段限速两类事故场景的人类车和自动驾驶车混合流交通分别进行模拟仿真.研究结果表明:速度反馈机制可以提升约7%~43%的预碰撞时间,并且有效缩小事故影响范围,使车辆更加平稳、安全地通过事故瓶颈区域.

基于深度学习的电力系统暂态功角与暂态电压稳定裕度一体化评估

随着面向高比例可再生能源新型电力系统的转型,系统运行特性日趋复杂。暂态功角稳定(transientangle stability,TAS)与暂态电压稳定(transient voltage stability,TVS)问题相互耦合且频发,为系统安全稳定评估带来严峻挑战。研究首先采用变步长二分法通过调用PSASP从时间维度上构建了暂态电压与暂态功角的稳定边界。研究了不同故障位置、感应电动机占比、负荷率对稳定边界的影响并依托边界确定主导失稳模式。其次提出一种基于注意力机制与一维卷积神经网络融合的电力系统功角稳定及电压稳定裕度评估的新方法。该方法直接面向测量数据,将节点稳态与暂态运行的电压幅值、有功功率、无功功率数据作为输入特征,节省了数据处理时间。通过一维卷积神经网络构建输入特征与极限切除时间的映射,利用注意力机制进一步提高了模型预测效果。通过新英格兰IEEE39节点系统进行分析验证,结果表明该方法可以实现暂态安全裕度的快速评估且具有较高的预测精度。

基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具,可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而,AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果,尤其是对于资源动态分配的实时系统。为解决结果不精确的问题,可结合基于系统有穷状态空间遍历的模型检验方法。首先,将实时系统AADL模型转换为时间自动机(TA)模型,以TA为理论体系进行模型检验。其次,基于反应链的需求分类定义端到端延迟需求表达模式。最后,给出对应需求模式的观察者模型,与系统模型并行组合,优化模型验证的时空资源消耗。

CATALAN NUMBERS, DYCK LANGUAGE AND TIME SERIES OF ELEMENTARY CELLULAR AUTOMATON OF RULE 56

A new approach to study the evolution complexity of cellular automata is proposed and explained thoroughly by an example of elementary cellular automaton of rule 56. Using the tools of distinct excluded blocks, computational search and symbolic dynamics, the mathematical structure underlying the time series generated from the elementary cellular automaton of rule 56 is analyzed and its complexity is determined, in which the Dyck language and Catalan numbers emerge naturally.

一种基于时间自动机的安全智能合约生成方法

区块链是一种去中心化的计算范式,在诸多领域具有良好的应用前景。智能合约是区块链应用的关键,然而,智能合约的安全问题时有发生,有些甚至造成重大的经济损失。为了避免智能合约在设计开发阶段出现由逻辑不严谨或错误逻辑所造成的安全漏洞,提出一种基于时间自动机模型的安全智能合约生成方法。相较于直接编写合约代码,该方法通过将证明为正确的模型转换为可执行的智能合约代码,有效解决在智能合约开发设计阶段所存在的安全性问题。利用UPPAAL工具将人类可理解的文本合约建模为时间自动机并通过模型验证来确保模型的安全性和可靠性。通过对智能合约的正式定义建立时间自动机与智能合约的映射规则,根据相应的映射规则,时间自动机被转换为模块化的Solidity智能合约代码。设计一个具体的商品预售活动案例进行分析,结果表明,通过所提方法生成的商品预售合约的Solidity代码可成功编译并部署在以太坊测试网络中。

辅助等电位联结设计探讨

通过TN接地系统的接地故障电流、接地故障电压、故障电压传导等分析,阐述间接接触防护自动切断电源的条件以及设置辅助等电位联结的必要性和有效性,得出辅助等电位联对接地故障电流大小影响,并强调设了辅助等电位联结后,还应校验间接接触保护电器的动作特征能否满足要求。