期刊文献+
共找到89篇文章
< 1 2 5 >
每页显示 20 50 100
通信顺序进程的扩充及其在协议形式化技术中的应用 被引量:4
1
作者 顾翔 赵保华 屈玉贵 《通信学报》 EI CSCD 北大核心 2004年第2期43-50,共8页
讨论了为进行协议形式化描述而进行的CSP扩充问题。向CSP中引入了可终止进程的概念,并给出了可终止进程的判定方法;针对CSP只能进行同步通信描述的缺陷,提出了用CSP来描述异步通信的手段;最后给出了AB协议的CSP描述,并在此基础上初步讨... 讨论了为进行协议形式化描述而进行的CSP扩充问题。向CSP中引入了可终止进程的概念,并给出了可终止进程的判定方法;针对CSP只能进行同步通信描述的缺陷,提出了用CSP来描述异步通信的手段;最后给出了AB协议的CSP描述,并在此基础上初步讨论了协议规范的正确性及测试用例的生成。 展开更多
关键词 协议工程 通信顺序进程 形式化描述技术 协议测试
在线阅读 下载PDF
基于通信顺序进程的并发DEDS的规范和证实 被引量:1
2
作者 徐林 吴智铭 +1 位作者 杨根科 孟凡英 《上海交通大学学报》 EI CAS CSCD 北大核心 2002年第8期1177-1180,共4页
在实时通信顺序进程 ( TCSP)的基础上对离散事件动态系统 ( DEDS)进行建模、规范和证实 .介绍了 TCSP中与 DEDS相关的一些研究成果 ,根据离散事件的特点作了符号语义上的改进 ,就两个具体的例子——自动导引小车 ( AGV)和火车道口系统... 在实时通信顺序进程 ( TCSP)的基础上对离散事件动态系统 ( DEDS)进行建模、规范和证实 .介绍了 TCSP中与 DEDS相关的一些研究成果 ,根据离散事件的特点作了符号语义上的改进 ,就两个具体的例子——自动导引小车 ( AGV)和火车道口系统建立了 TCSP模型 ,给出了它们需要满足的特性 。 展开更多
关键词 并发DEDS 实时通信顺序进程 refusal模型 离散事件动态系统 自动导引小车 火车道口系统
在线阅读 下载PDF
基于通信顺序进程方法的RSSP-Ⅱ通信协议安全性分析 被引量:2
3
作者 陆德彪 和晟姣 王剑 《信息网络安全》 2016年第7期7-14,共8页
近年来,工业控制系统网络安全问题逐渐显现。铁路信号系统作为工业控制系统的一种特殊应用,除了保证系统设备可靠、功能完整之外,承载信息传输的网络安全问题也是迫切需要关注和解决的问题。文章分析了关乎铁路信号系统安全的RSSP-Ⅱ通... 近年来,工业控制系统网络安全问题逐渐显现。铁路信号系统作为工业控制系统的一种特殊应用,除了保证系统设备可靠、功能完整之外,承载信息传输的网络安全问题也是迫切需要关注和解决的问题。文章分析了关乎铁路信号系统安全的RSSP-Ⅱ通信协议,引入了形式化建模中的通信顺序进程方法,对通信协议的密钥服务流程和对等实体认证过程这两个关键内容进行了相应的建模研究工作。文章采用模型检测工具Casper-FDR对协议安全属性中的保密性、认证性进行了验证,分析了对应的验证结果。实验结果表明,访问状态数、转换状态数、状态转换时间参数均正常,反例个数为0,验证了RSSP-Ⅱ 在密钥服务和对等实体认证过程的安全性。 展开更多
关键词 RSSP-II 通信协议 安全性分析 通信顺序进程方法
在线阅读 下载PDF
基于通信顺序进程与B方法的CBTC计算机联锁系统的形式化建模与验证 被引量:9
4
作者 王鲲 《中国铁道科学》 EI CAS CSCD 北大核心 2018年第3期101-109,共9页
针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实... 针对CBTC联锁系统的复杂性,提出一种基于通信顺序进程(CSP)与B方法集成的形式化方法,即在通信顺序进程的通信事件与B方法抽象机的操作之间建立起一对一的映射关系,实现通信事件通过控制抽象机的操作、进而影响抽象机状态的目标,从而实现通信顺序进程和B方法之间的同步。以1个实际站场为例,采用B方法对具有复杂状态空间的CBTC联锁系统的逻辑状态运算建立抽象机,采用通信顺序进程对CBTC联锁系统与外部系统的并发交互行为建立进程,并通过映射关系使CBTC联锁系统的抽象机与外部交互行为进程同步,由此建立基于通信顺序进程与B方法的CBTC联锁系统的形式化模型。采用ProB工具对建立的CBTC联锁系统模型的安全性、无死锁性进行验证。发现并修改模型中的不一致、不完全、歧义等错误,从而验证了CBTC联锁系统的安全性和无死锁性,保证了系统的最终实现。 展开更多
关键词 城市轨道交通 CBTC 计算机联锁系统 形式化方法 通信顺序进程 B方法
在线阅读 下载PDF
补偿通信顺序进程的扩展及失败发散语义
5
作者 陈振邦 王戟 齐治昌 《计算机工程与科学》 CSCD 北大核心 2010年第3期89-95,110,共8页
补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩... 补偿通信顺序进程(cCSP)是通信顺序进程用于长事务建模的扩展,可用来描述服务计算中的编制程序,比如WS-BPEL程序。目前,cCSP只有操作语义和基于迹的指称语义,对死锁和发散行为的推理支持不够。本文扩展了cCSP,引入新的组合操作子,给出扩展cCSP的失败发散语义;并根据该语义,给出新引入组合操作子的重要代数规则,用于语义的理解和佐证。最后,给出一个案例描述用于展示扩展cCSP。 展开更多
关键词 补偿通信顺序进程 指称语义 失败发散语义 代数规则
在线阅读 下载PDF
基于通信顺序进程的网络故障管理形式化描述
6
作者 包铁 刘淑芬 《吉林大学学报(工学版)》 EI CAS CSCD 北大核心 2007年第1期117-120,共4页
针对网络故障的复杂性和多样性,对网络故障管理的形式化描述进行了研究。基于霍尔的“通信顺序进程”和相关的网络形式化的理论研究结果,提出了一种网络故障管理的形式化方法。该方法通过添加新的概念和定义扩充了“通信顺序进程”,为... 针对网络故障的复杂性和多样性,对网络故障管理的形式化描述进行了研究。基于霍尔的“通信顺序进程”和相关的网络形式化的理论研究结果,提出了一种网络故障管理的形式化方法。该方法通过添加新的概念和定义扩充了“通信顺序进程”,为描述复杂的故障信息提供数据类型支持,同时建立故障模型对网络故障采集和网络故障分析进行了精确的形式化描述,为故障管理系统的设计正确性和可验证性提供了可靠的数学依据。 展开更多
关键词 计算机系统结构 形式化描述 通信顺序进程 故障管理
在线阅读 下载PDF
基于通信顺序进程的OWL-S语义分析与建模 被引量:2
7
作者 杨建书 吴尽昭 周瑾 《计算机应用》 CSCD 北大核心 2010年第8期2173-2176,2196,共5页
为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语... 为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。 展开更多
关键词 OWL-S过程模型 自动化验证 通信顺序进程 形式化语义 建模
在线阅读 下载PDF
使用“通信顺序进程”机制的神经网络仿真 被引量:1
8
作者 孙亚军 曹磊 虞厥邦 《小型微型计算机系统》 CSCD 北大核心 1996年第4期35-39,共5页
本文引入了“通信顺序进程”的概念,同时介绍了一种实现环境──RISC结构的Tranputer处理器及Occam并行化编程语言,并阐述了用“通信顺序进程”机制来仿真人工神经网络的方法。
关键词 神经网络 仿真 通信顺序进程
在线阅读 下载PDF
基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法 被引量:2
9
作者 吕继东 李开成 +1 位作者 唐涛 袁磊 《中国铁道科学》 EI CAS CSCD 北大核心 2012年第5期91-97,共7页
针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具... 针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。 展开更多
关键词 高速铁路列控系统 混合通信顺序进程 混合自动机 行车许可场景
在线阅读 下载PDF
基于通信顺序进程的计算机网络通信协议形式化描述 被引量:6
10
作者 孙踊 杨宏戟 《北京大学学报(自然科学版)》 CAS CSCD 北大核心 1997年第1期110-122,共13页
描述和设计计算机网络通信协议时,使用抽象的同步通信机制最为方便。但在实际中,使用异步通信机制将不可避免。基于霍尔的“通信顺序进程”和其他对通信协议描述与设计的理论研究结果,本文提出一个形式化方法。
关键词 通信顺序进程 计算机网络 协议 通信 形式化描述
在线阅读 下载PDF
使用“通信顺序进程”机制的神经网络仿真
11
作者 孙亚军 曹磊 虞厥邦 《计算机应用与软件》 CSCD 1998年第5期32-37,共6页
本文引入了“通信顺序进程”的概念,同时介绍了一种实现环境——RISC结构的Tansputer处理器及Occam并行化编程语言,并阐述了用“通信顺序进程”机制来仿真人工神经网络的方法。
关键词 神经网络 仿真 通信顺序进程
在线阅读 下载PDF
通信顺序进程的证明规则
12
作者 宋国新 喻萌 《计算机学报》 EI CSCD 北大核心 1990年第5期374-381,共8页
本文把Brookes验证平行程序的思想应用于Hoare的通信顺序进程(CSP),提出了一组证明规则,以验证CSP程序的部分正确性。
关键词 通信顺序进程 证明规则
在线阅读 下载PDF
基于通信顺序进程的Android程序复杂信息流分析方法
13
作者 袁占慧 杨智 +2 位作者 张红旗 金舒原 杜学绘 《网络与信息安全学报》 2021年第5期156-168,共13页
Android隐私泄露问题日益严重,信息流分析是发现隐私泄露的一种主要方法。传统信息流分析方法以单一可达性分析为主,难以分析复杂信息流。提出一种基于通信顺序进程的信息流分析方法,建立应用程序行为的形式化模型,从而全面刻画程序信... Android隐私泄露问题日益严重,信息流分析是发现隐私泄露的一种主要方法。传统信息流分析方法以单一可达性分析为主,难以分析复杂信息流。提出一种基于通信顺序进程的信息流分析方法,建立应用程序行为的形式化模型,从而全面刻画程序信息流行为。基于进程迹等价分析方法能够自动化验证信息流关联、信息流约束等复杂信息流问题,进而判断是否存在敏感信息泄露。实验表明,所提方法能够达到90.99%的准确率。 展开更多
关键词 安卓 信息流分析 隐私防护 形式化分析 通信顺序进程
在线阅读 下载PDF
基于通信顺序进程的计算机网络通信协议形式化描述 被引量:1
14
作者 刘芳 《信息系统工程》 2016年第2期124-124,共1页
在当前的社会中,随着计算机技术、网络技术的不断发展,在人们的日常生活当中,对计算机网络的使用要求越来越高。在这样的情况之下,对于计算机网络通信协议的形式化描述越来越重要。在这一过程中,将通信顺序进程引入到可终止进程当中,同... 在当前的社会中,随着计算机技术、网络技术的不断发展,在人们的日常生活当中,对计算机网络的使用要求越来越高。在这样的情况之下,对于计算机网络通信协议的形式化描述越来越重要。在这一过程中,将通信顺序进程引入到可终止进程当中,同时给出了相应的判定方法。由于过去通信顺序进程只能对同步通信进行描述,因而提出了基于通信顺序进程的异步通信描述方法,最后结合AB协议,进行了基于通信顺序进程的描述。 展开更多
关键词 通信顺序进程 计算机网络通信协议 形式化描述
在线阅读 下载PDF
一种设计通信顺序进程通道服务的方法
15
作者 赵扬 《上海电机学院学报》 2019年第4期245-248,共4页
当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,... 当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,在名称解析、序列化和反序列化方面存在单点故障和额外开销,设计者难以使用他们来构建大规模网络分布式应用。利用Kademlia网络实现的路由算法,对CSP模型中提出的通道进行重新抽象,并把它设计为由一组远程调用过程构成的网络服务,使其具有改良的可靠性和扩展性,为设计者在区块链网络中开发大规模、安全的分布式应用提供了现实意义。 展开更多
关键词 Kademlia覆盖网络 通信顺序进程(csp)通道 进程同步通信
在线阅读 下载PDF
基于进程迹的CSP模型验证框架 被引量:3
16
作者 赵岭忠 翟仲毅 钱俊彦 《计算机科学》 CSCD 北大核心 2013年第11期181-186,221,共7页
CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框... CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。 展开更多
关键词 通信顺序进程(csp) 并发系统 迹模型 回答集编程(ASP)
在线阅读 下载PDF
基于CSP的进程行为取证方法研究
17
作者 孙国梓 俞超 陈丹伟 《南京邮电大学学报(自然科学版)》 2009年第6期48-53,共6页
针对取证过程中所获取的进程异常行为,提出进程行为事件重建犯罪过程的方法。该方法使用CSP(通信顺序进程)理论来形式化描述具有威胁乃至破坏性的进程操作及进程间的通信,根据系统保存的进程行为记录建立进程通信状态模型,使用基于路径... 针对取证过程中所获取的进程异常行为,提出进程行为事件重建犯罪过程的方法。该方法使用CSP(通信顺序进程)理论来形式化描述具有威胁乃至破坏性的进程操作及进程间的通信,根据系统保存的进程行为记录建立进程通信状态模型,使用基于路径搜索的进程行为解释算法分析模型内所有可能的进程通信序列,形成进程通信行为规则,在排除不符合规则的通信序列的基础上,找到能够形成合理证据链的通信序列。通过案例分析进行了证据的形式化及CSP建模,给出了进程行为的具体分析解释和原型系统,验证该方法的可行性和有效性。 展开更多
关键词 计算机取证 csp 进程行为 通信序列
在线阅读 下载PDF
CSP轧机机架网络通信故障原因分析及解决措施
18
作者 周杰 邓槟杰 吴苓 《自动化应用》 2014年第8期35-36,共2页
针对CSP轧机机架网络通信故障的问题进行分析,并提出相应的设备改造和模块技术优化措施,以减少故障发生的次数,保证生产稳定。
关键词 csp 网络通信 设备改造 优化 生产稳定
在线阅读 下载PDF
马钢CSP轧机过程自动化系统改造通信管理设计
19
作者 顾仲熙 《金属世界》 2016年第3期35-38,共4页
在钢铁企业里,二级控制系统作为整条热轧生产线自动化控制的大脑中枢,起着十分重要的作用。随着马钢CSP产品大纲的变化以及产品质量要求的提高,二级系统的控制模型已越来越不能满足实际生产的需要,因此于2014年启动二级改造计划。文章... 在钢铁企业里,二级控制系统作为整条热轧生产线自动化控制的大脑中枢,起着十分重要的作用。随着马钢CSP产品大纲的变化以及产品质量要求的提高,二级系统的控制模型已越来越不能满足实际生产的需要,因此于2014年启动二级改造计划。文章详细介绍了改造后的通信连接配置、网关服务器配置和电文系统设计。通过现场的测试和调试,过程自动化系统改造完全实现了和西门子一级系统之间的通信功能。 展开更多
关键词 自动化系统 csp 大脑中枢 热轧生产线 服务器配置 控制模型 二级控制 钢铁企业 通信管理 质量要求
在线阅读 下载PDF
CTCT-4级安全通信协议的形式化建模与验证 被引量:7
20
作者 胡晓辉 陈慧丽 +1 位作者 石广田 陈永 《计算机工程与应用》 CSCD 2014年第4期81-85,共5页
CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统,而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施,引用一种改进的NSSK安全协议来保障车... CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统,而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施,引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信,并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。 展开更多
关键词 GSM-R 安全协议 通讯顺序进程(csp) 故障 偏差 精炼检测器(FDR)
在线阅读 下载PDF
上一页 1 2 5 下一页 到第
使用帮助 返回顶部