基于Event-B的一种联锁逻辑的形式化建模研究

铁路车站信号联锁逻辑的形式化描述无论对计算机联锁软件的研发,还是对联锁软件的第三方测试都是非常重要的。基于Event-B方法,利用自动机模型和形式化语言对车站的一种信号联锁逻辑进行建模研究,并通过逐步精化的方法扩展联锁功能,依赖不变式技术形式化地保证了该模型的安全性。所建模型通过Rodin平台的验证,结果表明它们是安全的。     

基于CPN模型的不可否认协议分析

通过对不可否认协议的语义进行分析,建立有色Petri网（Coloured Petri Net,CPN）中基本元素与安全协议中元素的对应关系,对CPN Tools提供的建模语言（CPN ML）在规范协议描述、简化协议建模及自动检测方面进行扩展,提出了一种基于CPN模型的不可否认协议分析方法,该方法利用CPN tools的状态空间查询功能和自建的查询函数库来对不可否认协议进行分析和验证,该工具具有通用性强、时效性强和交互性好等诸多优点,并通过实例说明了这种方法的有效性。     

基于着色Petri网的交换式局域网仿真

利用CPN—Tools建模辅助工具建立了基于着色Petri网的交换式局域网模型,通过模型的仿真运行得出了网络流量和网络延时之间的关系,模型的构件组成为交换机、工作站、服务器。     

广州地铁五号线ARS功能

一、概述ARS是ATS实现列车自动控制的核心功能。信号系统给信号机设置自动属性,当列车到达接近区段,系统根据列车的车次号信息自动生成进路排列的联锁命令,并将这些联锁命令发送到联锁系统,完成进路排列的自动触发功能。如图1所示,由人工操作设置S1信号机为ARS属性,当列车运行至触发区段时,系统将根据列车的目的地     

时速300公里高铁RBC-CBI信息分析

我国已全面进入高铁时代,时速300公里高铁在可达性、交通距离和时间成本方面有巨大优势。无线闭塞中心RBC与车站联锁系统CBI之间的数据信息对整个系统具有重要意义,将会给CTCS-3级列车控制系统的稳定运行产生很大影响。文章通过分析时速300公里高铁无线闭塞中心RBC与车站联锁系统CBI之间的信息数据交换,提出对RBC与车站联锁系统CBI之间数据交换信息的一些看法。     

GSM网络高铁列车异常场景识别和优化措施

高铁专网和外网在铁路沿线一般不做邻区关系,只有当列车到达车站时,高铁专网和外网才会建立邻区关系。当高铁列车在铁路沿线出现异常停车时,必然会导致很高的话务需求。文章通过对高铁列车上用户行为特征的分析,开发出一套实时监控机制,可实时监控高铁小区话务异常变化情况,自动判断异常停车事件,并实施,临时快速优化措施,分担高铁小区的话务,也可以自动判断列车是否已经恢复正常行驶,取消临时优化措施。     

城市三维空间模型快速构建方法研究

对城市三维空间模型建立方法的研究现状进行总结,提出城市三维空间模型的快速重建方案:采用一次性生成约束TIN构建地形模型,利用数字影像提取建筑物模型,通过CSG体素生长法对建筑物实施建模。在模型的建立过程中,首次将3种方法综合使用,实现了城市三维空间模型快速显示。     

基于CPN Tools研究综述

仿真工具CPN Tools是一款优秀的Petri网仿真工具,是仿真和分析着色petri网建立的模型。CPN Tools不仅支持基础着色Petri网建立模型,也支持带有时间和分层的着色petri网建立模型。CPN Tools支持CPN ML编程语言,颜色集,时间,层次化建模等,大大增加了它的描述能力和应用范围。同时,CPN Tools提供丰富的模型分析工具,如监视器,状态空间分析等,增强了它的模型分析能力和模型验证能力。     

基于OpenFlight API的建筑物场景自动建模及红外仿真

针对建筑物场景红外仿真真实性差、对国外软件依赖性强的现状,提出了一种新的适用于大规模建筑物场景自动建模及红外仿真的方法。该方法利用Google Earth提供的高分辨率航片中的阴影和地形信息,结合OpenFlight API自动建立建筑物场景三维模型,解决了数字高程数据、楼层数据缺失条件下的建模难题;通过对航片中不同城市地物的分割建立材质标号图像,利用理论分析的方法建立了建筑物场景中不同地物的红外辐射特征方程,离线生成了零视距红外纹理,并增加大气以及探测器作用效果,提高了红外场景的描述细节和真实性。     

基于AADL和SCADE的模型驱动软件设计

模型驱动开发逐渐应用于嵌入式系统的软件设计,在软件设计阶段重点关注的是软件的架构模型和详细功能模型。用于嵌入式系统软件建模的语言和工具很多,其中结构分析与设计语言(AADL)模型可以构建嵌入式软件的架构,高安全性应用开发环境(SCADE)模型可以描述嵌入式软件的逻辑功能,将两者统一使用可以满足嵌入式软件概要设计和详细设计的建模需求。针对某飞行器控制系统,本文分别使用AADL和SCADE对飞行器控制系统软件架构和功能进行建模,利用KCG工具从SCADE模型自动生成C代码,通过手工代码和自动生成代码的集成完成控制系统部分软件设计。实际应用表明,采用AADL和SCADE相结合的建模方法适用于模型驱动开发在嵌入式软件设计中应用。     

联锁道岔电子控制模块的设计

文中重点研究和分析了道岔电子控制技术，并在此基础上引入了道岔控制执行模块，其可以确保行车安全。继电联锁、计算机联锁等联锁方式，通常都由继电器来实现逻辑控制。文中在传统道岔控制技术的基础上，对现代铁路道岔控制系统的控制技术进行了研究，并对其中的关键技术进行了分析和说明。     

An Attack Modeling Based on Colored Petri Net

1 Attack Modeling A typical attack contains the following elements: 1) Objects attacked. These objects belong to the victims or can be regarded as public resource, such as networking bandwidth. 2) Attacker. These objects contain the hacker’s information, attacking tools and other states of attacker. 3) Attack processes. The stages of an attack and attack processes are used to depict the attacking action. 4) Control actions. These actions can be classified into response actions and defensiv…     

Modeling multi-traffic admission control in OFDMA system using Colored Petri Net

Call Admission Control (CAC) is one of the key traffic management mechanisms that must be deployed in order to meet the strict requirements for dependability imposed on the services provided by modern wireless networks. In this paper, we develop an executable top-down hierarchical Colored Petri Net (CPN) model for multi-traffic CAC in Orthogonal Frequency Division Multiple Access (OFDMA) system. By theoretic analysis and CPN simulation, it is demonstrated that the CPN model is isomorphic to Markov Chain (MC) assuming that each data stream follows Poisson distribution and the corresponding arrival time interval is an exponential random variable, and it breaks through MC??s explicit limitation, which includes MC??s memoryless property and proneness to state space explosion in evaluating CAC process. Moreover, we present four CAC schemes based on CPN model taking into account call-level and packet-level Quality of Service (QoS). The simulation results show that CPN offers significant advantages over MC in modeling CAC strategies and evaluating their performance with less computational complexity in addition to its flexibility and adaptability to different scenarios.     

面向算力网络的IP承载网关键技术及网络部署策略研究

随着云计算、边缘计算和智能终端的快速发展,算力资源呈现出泛在部署趋势,算力网络能够通过灵活的承载网络对泛在异构的算力资源进行调度,有效提升了算力资源利用率。文中结合当前算力网络发展现状,对算力网络的概念定义以及标准体系进行了总结,随后对SDN,SRv6等算力网络关键承载技术进行了阐述,并讨论了其在算力网络中的典型部署策略,最后对算力网络面临的挑战与后续研究方向进行了展望。     

自适应OFDMA系统无线资源管理的CPN建模与仿真

基于自适应OFDMA系统,对多业务系统中基于总发射功率最小化的无线资源管理问题进行研究,并使用着色Petri网(CPN,coloured Petri nets)以及CPN分析工具CPN Tools对其进行建模。采用Monitor监控器对模型进行仿真分析,并将仿真结果与随机Petri网(SPN,stochastic Petri nets)模型以及基于吞吐量最大化的CPN模型进行比较,验证了该系统模型的正确性和优越性。     

性能管理在驻地网中的应用

本文首先阐述性能管理的基本内容，然后分析性能管理在驻地网环境中的特性，最后提出了驻地网性能管理的应用模型，并具体介绍了该模型中每个模块采用的技术。     

Catalyst‐Free,Fast, and Tunable Synthesis for Robust Covalent Polymer Network Semiconducting Thin Films

Covalent polymer networks (CPNs) are of great technological interest due to their robustness and tunability; however, they are rarely applied as semiconductors in optoelectronic devices due to poor material processability. Herein, a simple, rapid, and powerful approach is reported to prepare CPN thin films based on an in situ thermal azide–alkyne cycloaddition (TAAC) in the absence of catalyst or solvent. The method is demonstrated with perylenediimide and triazine‐based monomers, and affords smooth and homogenous CPN films through solution processing and heat treatment (10 min). Moreover, the site‐specific TAAC realizes semiconducting CPNs without undesired impurities or byproducts, and tunable optoelectronic properties are achieved by varying the reaction temperature, which affects the intermolecular self‐assembly. The obtained CPN films exhibit exceptional solvent resistance and good n‐type semiconducting behavior, which together afford application in a series of multilayer solution‐processed organic photovoltaics, where the presence of CPN films significantly improves the solar energy conversion efficiency to over 8% (7% in control devices) when the CPN is used in a planar‐mixed heterojunction device architecture.     

The customer premises network for ATM: Architecture and standardization issues

This paper discusses the architecture of ATM-based customer premises networks (CPN), which can easily be tailored to the needs of a broad range of residential and (small) business customers. A first part analyses the functions of the classical CCITT reference model, and regroups them into building blocks for a new model. This model features a high degree of modularity, and interfaces with low-level functionality. The building blocks for this CPN are the network termination, connection subnets and switching subnets. Following this, some issues related to the user-network interface standardization are addressed, as this interface has potential to be a candidate for application in the whole CPN. Owing to publication schedules, the author did not have the opportunity to take into account the recent decisions taken by CCITT concerning ATM standards.     

反射式需求工程过程演化建模

用反射机制为软件系统需求工程过程演化建模,将需求工程过程的开发活动作为反射系统的基层,实现软件系统的功能需求,将软件系统的非功能需求作为反射系统的元层,对需求工程过程的开发活动进行调节、控制,并将非功能需求的性质反射到功能需求.定义了有色Petri网及其范畴,并用有色Petri网范畴描述软件系统非功能需求性质的模拟、保持和反射机制;用有色Petri网建立反射式需求工程过程演化形式化模型,模拟了软件系统需求工程过程中功能需求和非功能需求的迭代、增量、演化,为软件系统需求工程过程演化建模提出了一种新的方法.