一种设计通信顺序进程通道服务的方法

当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,在名称解析、序列化和反序列化方面存在单点故障和额外开销,设计者难以使用他们来构建大规模网络分布式应用。利用Kademlia网络实现的路由算法,对CSP模型中提出的通道进行重新抽象,并把它设计为由一组远程调用过程构成的网络服务,使其具有改良的可靠性和扩展性,为设计者在区块链网络中开发大规模、安全的分布式应用提供了现实意义。

基于进程迹的CSP模型验证框架

CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。

远距离无中继有线语音通讯系统硬件设计

本文主要讨论了远距离无中继有线通讯系统的硬件设计思想。本通讯系统采用AMBE10 0 0TMCODEC结合LSP10 2 7语音PCM信号处理芯片进行语音信号的处理 ;同时 ,采用FX90 9A和FX42 9A传输数字化后的语音信号 ;在整体上 ,采用AT89C5 2单片处理器负责接口。

基于Petri网的CSP并发系统验证技术研究

通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。

一种利用CSP转换UML活动图模型的方法

为了研究UML活动图模型中可中断活动区间、嵌套的层次活动图等高级构造子的形式化表示,依据进程代数理论,采用一种利用CSP转换UML活动图模型的方法。建立了UML活动图元模型捕获活动图语言的主要概念和属性并依据元模型的类图将建模语言的抽象语法形式化,并给出了以“活动”为中心的形式化表示机制。共享医疗业务流程管理为案列研究背景,对活动图模型高级构造子形式化验证,结果表明CSP代数理论不仅能够对活动图模型进行表示,而且能够对共享医院业务流程多层次、全方面地进行分析。

精炼二级计算机系统数据通讯作用与功能实现

通过对二炼钢区域二级计算机的网络系统构成、各主要工艺设备环节间的数据流程、数据传输、数据交换功能的说明 ,系统描述了CSP厂精炼二级计算机通讯机制、数据交换、实现功能及其作用 ;介绍了二级计算机通讯的工作原理 ,同时也展示了三级计算机系统的作用。

基于CSP的CTCS-1级列控系统RDC数据验证的研究

区域列控数据中心(RDC)作为CTCS-1级列控系统地面设备的核心部分,为车载设备提供线路数据、临时限速信息、进路信息等,因此,RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析,总结出数据应满足的约束条件,以轨道区段数据为例,基于实体数据应满足的域值条件以及数据之间的关系建立数据约束规则,将数据验证规则加入数据验证流程,利用通信顺序进程(CSP)形式化语言对数据验证流程进行建模,用模型检验工具ProB对CSP语义模型进行检验。验证结果正确,表明数据验证方法可行,为RDC静态数据自动化验证奠定了基础。

薄板CSP公辅水系统全面实现PLC控制

主要阐述了CSP区整个公辅系统实现PLC控制 ,通过ST - 4 0 0主站之间的工业以太网 ,以及S7- 4 0 0主站与从站ET - 2 0 0之间的profibus—DP网的连接 ,实现系统数据通讯。并通过工作站WINCC画面和安装在现场的各种先进自动化仪表对水系统各个泵组的压力、流量、温度进行动态控制和显示。完成各系统控制功能 ,实现了集中操作、集中监控 。

CSP派员参加全国认证认可标准化技术委员会第六次全体委员会会议

2009年4月16日，全国认证认可标准化技术委员会在京召开了第六次全体委员会会议。SAC／TC261全体委员、通讯成员，SAC／TC261秘书处人员，国家认监委，国家标准委领导和相关SAC／TC领导以及专家等参加了会议。CSP技术发展部部长周东培作为SAC／TC261通讯成员参加了会议。

CTCT-4级安全通信协议的形式化建模与验证

CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统,而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施,引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信,并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。

采用函数式语言的BPEL模型形式化验证方法

通信顺序进程(communicating sequential process,CSP)是一种经典的形式化方法,CSP_M是在CSP基础上提出的一种函数式语言。目前Web服务组合中BPEL(business process execution language)模型缺乏可执行的形式化编程语言,通过CSP_M提出了一种基于函数式语言的BPEL模型验证方法。首先给出了基于CSP_M的BPEL模型建模与验证框架;其次给出了CSP_M的进程代数定义;再次详细描述了BPEL语言到CSP以及CSP_M的映射方法;最后以一个在线购物系统为例,讨论了该方法的使用效果。实验表明该方法可以提高BPEL模型的可靠性。

Powerlink协议异步调度机制的建模与分析

针对通信协议进行形式化建模与分析,能够很大程度上提高工控协议的安全性。通过分析开源实时以太网Powerlink的同步、异步阶段的不同通信行为,以及在同步阶段的不同通信模式,提出一种利用CSP(Communication Sequential Process)语言对Powerlink协议进行形式化建模的方法。使用该方法能够描述Powerlink在数据链路层上不同节点之间的通信行为,以及描述在随机产生异步请求的情况下,异步阶段的异步请求调度行为。同时,该方法也准确模拟了协议运行过程中,错误处理机制对丢失帧情况的处理过程。最后利用软件PAT(Process Analysis Toolkit)验证了这些异步调度过程是否满足优先级顺序等性质,有助于对协议的运行机制进行深入分析。

协同业务过程的随机行为分析方法

参与组织随机行为是评价业务协同有效实施的一个关键因素。结合进程代数和马尔科夫链,提出了一种协同业务过程的随机行为分析方法。首先,使用有限状态自动机建模每个参与组织的业务过程,通过引入异步消息通信关系定义协同业务过程。其次,提出将参与组织业务过程转换成通信顺序进程(Communication Sequential Process,CSP)方法,进而将每个参与组织业务过程对应CSP进程并发组合得到协同业务过程对应的CSP进程,并根据CSP操作语义构建协同业务过程的状态迁移模型。最后,引入状态迁移模型正则化概念,从理论上证明正则化的状态迁移模型与一个齐次马尔科夫链相对应,进而根据平衡方程求得状态迁移系统中每个状态的稳定概率,以此为基础实现参与组织随机行为分析。通过对电设备采购过程建模与随机行为分析阐述该方法的可行性和有效性。