期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
8
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
一种设计通信顺序进程通道服务的方法
1
作者
赵扬
《上海电机学院学报》
2019年第4期245-248,共4页
当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,...
当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,在名称解析、序列化和反序列化方面存在单点故障和额外开销,设计者难以使用他们来构建大规模网络分布式应用。利用Kademlia网络实现的路由算法,对CSP模型中提出的通道进行重新抽象,并把它设计为由一组远程调用过程构成的网络服务,使其具有改良的可靠性和扩展性,为设计者在区块链网络中开发大规模、安全的分布式应用提供了现实意义。
展开更多
关键词
Kademlia覆盖网络
通信
顺序进程
(
csp
)
通道
进程
同步
通信
下载PDF
职称材料
基于进程迹的CSP模型验证框架
被引量:
3
2
作者
赵岭忠
翟仲毅
钱俊彦
《计算机科学》
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
职称材料
基于Petri网的CSP并发系统验证技术研究
被引量:
1
3
作者
刘彦青
赵岭忠
钱俊彦
《计算机科学》
CSCD
北大核心
2015年第10期244-250,291,共8页
通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于...
通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。
展开更多
关键词
通信
顺序进程
(
csp
)
并发系统
PETRI网
性质验证
安全性
下载PDF
职称材料
基于CSP的CTCS-1级列控系统RDC数据验证的研究
4
作者
卢铃冉
张勇
《铁路计算机应用》
2019年第7期52-58,共7页
区域列控数据中心(RDC)作为CTCS-1级列控系统地面设备的核心部分,为车载设备提供线路数据、临时限速信息、进路信息等,因此,RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析,总结出数据应满足的约束条件,以...
区域列控数据中心(RDC)作为CTCS-1级列控系统地面设备的核心部分,为车载设备提供线路数据、临时限速信息、进路信息等,因此,RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析,总结出数据应满足的约束条件,以轨道区段数据为例,基于实体数据应满足的域值条件以及数据之间的关系建立数据约束规则,将数据验证规则加入数据验证流程,利用通信顺序进程(CSP)形式化语言对数据验证流程进行建模,用模型检验工具ProB对CSP语义模型进行检验。验证结果正确,表明数据验证方法可行,为RDC静态数据自动化验证奠定了基础。
展开更多
关键词
CTCS-1
区域列控数据中心(RDC)
数据验证
通信
顺序进程
(
csp
)
下载PDF
职称材料
基于广义污点传播模型的操作系统访问控制
被引量:
7
5
作者
杨智
殷丽华
+3 位作者
段洣毅
吴金宇
金舒原
郭莉
《软件学报》
EI
CSCD
北大核心
2012年第6期1602-1619,共18页
动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized t...
动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized taint propagation model,简称GTPM),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累;还利用通信顺序进程(CSP)语言描述了模型的规格,以明确基于GTPM的操作系统的信息流控制行为的形式化语义;基于CSP的进程等价验证模型定义了可降密无干扰,并借助FDR工具证明形式化构建的抽象GTPM系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.
展开更多
关键词
污点传播
隐蔽
通道
通信
顺序进程
无干扰
最小权限
信息流控制
操作系统
下载PDF
职称材料
采用函数式语言的BPEL模型形式化验证方法
被引量:
5
6
作者
祝义
黄志球
周航
《计算机科学与探索》
CSCD
北大核心
2018年第2期185-196,共12页
通信顺序进程(communicating sequential process,CSP)是一种经典的形式化方法,CSP_M是在CSP基础上提出的一种函数式语言。目前Web服务组合中BPEL(business process execution language)模型缺乏可执行的形式化编程语言,通过CSP_M提出...
通信顺序进程(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模型的可靠性。
展开更多
关键词
函数式语言
通信
顺序进程
(
csp
)
业务流程执行语言(BPEL)
形式化验证
模型检测
下载PDF
职称材料
Powerlink协议异步调度机制的建模与分析
被引量:
2
7
作者
陈睿
庞海萍
+2 位作者
郝丽
厉达
杨栋
《计算机工程与应用》
CSCD
北大核心
2019年第17期259-265,共7页
针对通信协议进行形式化建模与分析,能够很大程度上提高工控协议的安全性。通过分析开源实时以太网Powerlink的同步、异步阶段的不同通信行为,以及在同步阶段的不同通信模式,提出一种利用CSP(Communication Sequential Process)语言对Po...
针对通信协议进行形式化建模与分析,能够很大程度上提高工控协议的安全性。通过分析开源实时以太网Powerlink的同步、异步阶段的不同通信行为,以及在同步阶段的不同通信模式,提出一种利用CSP(Communication Sequential Process)语言对Powerlink协议进行形式化建模的方法。使用该方法能够描述Powerlink在数据链路层上不同节点之间的通信行为,以及描述在随机产生异步请求的情况下,异步阶段的异步请求调度行为。同时,该方法也准确模拟了协议运行过程中,错误处理机制对丢失帧情况的处理过程。最后利用软件PAT(Process Analysis Toolkit)验证了这些异步调度过程是否满足优先级顺序等性质,有助于对协议的运行机制进行深入分析。
展开更多
关键词
POWERLINK
通信
顺序进程
(
csp
)
建模
验证
流程分析工具箱(PAT)
下载PDF
职称材料
协同业务过程的随机行为分析方法
8
作者
赵莹
潘华
+2 位作者
孙金艳
莫启
代飞
《计算机工程与应用》
CSCD
北大核心
2019年第3期245-251,265,共8页
参与组织随机行为是评价业务协同有效实施的一个关键因素。结合进程代数和马尔科夫链,提出了一种协同业务过程的随机行为分析方法。首先,使用有限状态自动机建模每个参与组织的业务过程,通过引入异步消息通信关系定义协同业务过程。其次...
参与组织随机行为是评价业务协同有效实施的一个关键因素。结合进程代数和马尔科夫链,提出了一种协同业务过程的随机行为分析方法。首先,使用有限状态自动机建模每个参与组织的业务过程,通过引入异步消息通信关系定义协同业务过程。其次,提出将参与组织业务过程转换成通信顺序进程(Communication Sequential Process,CSP)方法,进而将每个参与组织业务过程对应CSP进程并发组合得到协同业务过程对应的CSP进程,并根据CSP操作语义构建协同业务过程的状态迁移模型。最后,引入状态迁移模型正则化概念,从理论上证明正则化的状态迁移模型与一个齐次马尔科夫链相对应,进而根据平衡方程求得状态迁移系统中每个状态的稳定概率,以此为基础实现参与组织随机行为分析。通过对电设备采购过程建模与随机行为分析阐述该方法的可行性和有效性。
展开更多
关键词
协同业务过程
异步消息
通信
随机行为
通信
顺序进程
(
csp
)
马尔科夫链
下载PDF
职称材料
题名
一种设计通信顺序进程通道服务的方法
1
作者
赵扬
机构
中国证券登记结算有限责任公司上海分公司
出处
《上海电机学院学报》
2019年第4期245-248,共4页
文摘
当前金融机构正在寻求使用区块链技术重构关键性应用软件。通常,设计者引用通信顺序进程(CSP)库去构建这些软件,便可方便套用CSP模型去验证软件在并发通信过程中的安全性。然而,在现有的CSP库中,通道以面向对象方式被抽象、设计和实现,在名称解析、序列化和反序列化方面存在单点故障和额外开销,设计者难以使用他们来构建大规模网络分布式应用。利用Kademlia网络实现的路由算法,对CSP模型中提出的通道进行重新抽象,并把它设计为由一组远程调用过程构成的网络服务,使其具有改良的可靠性和扩展性,为设计者在区块链网络中开发大规模、安全的分布式应用提供了现实意义。
关键词
Kademlia覆盖网络
通信
顺序进程
(
csp
)
通道
进程
同步
通信
Keywords
Kademlia overlay network
communicating sequential processes(
csp
)channel
process synchronous communication
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于进程迹的CSP模型验证框架
被引量:
3
2
作者
赵岭忠
翟仲毅
钱俊彦
机构
桂林电子科技大学计算机科学与工程学院
出处
《计算机科学》
CSCD
北大核心
2013年第11期181-186,221,共7页
基金
国家自然科学基金(61262008
61063002)
+2 种基金
广西自然基金(2011GXNSFA018166
2011GXNSFA018164)
广西可信软件重点实验室基金(kx201113)资助
文摘
CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。
关键词
通信
顺序进程
(
csp
)
并发系统
迹模型
回答集编程(ASP)
Keywords
Communicating sequential processes, Concurrent system, Trace model, Answer set programming
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于Petri网的CSP并发系统验证技术研究
被引量:
1
3
作者
刘彦青
赵岭忠
钱俊彦
机构
桂林电子科技大学计算机科学与工程学院
出处
《计算机科学》
CSCD
北大核心
2015年第10期244-250,291,共8页
基金
国家自然科学基金(61262008
61100186)
+4 种基金
广西自然科学基金(2013GXNSFBA019267)
广西教育厅重点项目:高可信软件的安全性验证研究
广西高等学校高水平创新团队及卓越学者计划
广西可信软件重点实验室基金项目(kx201113)
桂林电子科技大学创新团队资助
文摘
通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。
关键词
通信
顺序进程
(
csp
)
并发系统
PETRI网
性质验证
安全性
Keywords
Communicating sequential processes (
csp
), Concurrent systems, Petri net, Property verification, Safety
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
基于CSP的CTCS-1级列控系统RDC数据验证的研究
4
作者
卢铃冉
张勇
机构
北京交通大学电子信息工程学院
出处
《铁路计算机应用》
2019年第7期52-58,共7页
基金
国家自然科学基金重点项目(6149700015)
中国铁路总公司科技研究开发计划(2015X002-A)
文摘
区域列控数据中心(RDC)作为CTCS-1级列控系统地面设备的核心部分,为车载设备提供线路数据、临时限速信息、进路信息等,因此,RDC数据的正确性对列车正常运行至关重要。通过对RDC所包含的静态数据进行分析,总结出数据应满足的约束条件,以轨道区段数据为例,基于实体数据应满足的域值条件以及数据之间的关系建立数据约束规则,将数据验证规则加入数据验证流程,利用通信顺序进程(CSP)形式化语言对数据验证流程进行建模,用模型检验工具ProB对CSP语义模型进行检验。验证结果正确,表明数据验证方法可行,为RDC静态数据自动化验证奠定了基础。
关键词
CTCS-1
区域列控数据中心(RDC)
数据验证
通信
顺序进程
(
csp
)
Keywords
CTCS-1
regional data center(RDC)
data validation
communication sequence process(
csp
)
分类号
U284.482 [交通运输工程—交通信息工程及控制]
TP39 [自动化与计算机技术—计算机应用技术]
下载PDF
职称材料
题名
基于广义污点传播模型的操作系统访问控制
被引量:
7
5
作者
杨智
殷丽华
段洣毅
吴金宇
金舒原
郭莉
机构
中国科学院计算技术研究所
解放军信息工程大学
中国科学院研究生院
信息内容安全技术国家工程实验室
出处
《软件学报》
EI
CSCD
北大核心
2012年第6期1602-1619,共18页
基金
国家自然科学基金(61070186)
国家高技术研究发展计划(863)(2009AA01Z438)
+1 种基金
国家重点基础研究发展计划(973)(2007CB311100
2011CB311801)
文摘
动态调整安全级是目前提高强制访问控制模型可用性的主要途径,它大致包括两类方法.其中,安全级范围方法对主体权限最小化的支持不够,而污点传播方法存在已知隐蔽通道.提出了保护操作系统保密性和完整性的广义污点传播模型(generalized taint propagation model,简称GTPM),它继承了污点传播在最小权限方面的特点,拓展了污点传播语义,以试图关闭已知隐蔽通道,引入了主体的降密和去污能力以应对污点积累;还利用通信顺序进程(CSP)语言描述了模型的规格,以明确基于GTPM的操作系统的信息流控制行为的形式化语义;基于CSP的进程等价验证模型定义了可降密无干扰,并借助FDR工具证明形式化构建的抽象GTPM系统具有可降密无干扰安全性质.最后,通过一个示例分析了模型的可用性提升.
关键词
污点传播
隐蔽
通道
通信
顺序进程
无干扰
最小权限
信息流控制
操作系统
Keywords
taint propagation
covert channel
csp
noninterference
least privilege
information flow control
operating system
分类号
TP316 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
采用函数式语言的BPEL模型形式化验证方法
被引量:
5
6
作者
祝义
黄志球
周航
机构
南京航空航天大学计算机科学与技术学院
江苏师范大学计算机科学与技术学院
出处
《计算机科学与探索》
CSCD
北大核心
2018年第2期185-196,共12页
基金
国家自然科学基金No.61502212
江苏省博士后基金No.1501055B~~
文摘
通信顺序进程(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模型的可靠性。
关键词
函数式语言
通信
顺序进程
(
csp
)
业务流程执行语言(BPEL)
形式化验证
模型检测
Keywords
functional programming language
communicating sequential process(
csp
)
business process execution language(BPEL)
formal verification
model checking
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
Powerlink协议异步调度机制的建模与分析
被引量:
2
7
作者
陈睿
庞海萍
郝丽
厉达
杨栋
机构
国网上海市电力公司电力科学研究院
华东师范大学国家可信嵌入式软件工程技术研究中心
上海赛璞乐电力科技有限公司
上海丰蕾信息科技有限公司
出处
《计算机工程与应用》
CSCD
北大核心
2019年第17期259-265,共7页
文摘
针对通信协议进行形式化建模与分析,能够很大程度上提高工控协议的安全性。通过分析开源实时以太网Powerlink的同步、异步阶段的不同通信行为,以及在同步阶段的不同通信模式,提出一种利用CSP(Communication Sequential Process)语言对Powerlink协议进行形式化建模的方法。使用该方法能够描述Powerlink在数据链路层上不同节点之间的通信行为,以及描述在随机产生异步请求的情况下,异步阶段的异步请求调度行为。同时,该方法也准确模拟了协议运行过程中,错误处理机制对丢失帧情况的处理过程。最后利用软件PAT(Process Analysis Toolkit)验证了这些异步调度过程是否满足优先级顺序等性质,有助于对协议的运行机制进行深入分析。
关键词
POWERLINK
通信
顺序进程
(
csp
)
建模
验证
流程分析工具箱(PAT)
Keywords
Powerlink
Communication Sequential Process(
csp
)
modeling
verification
Process Analysis Toolkit(PAT)
分类号
TP393.04 [自动化与计算机技术—计算机应用技术]
下载PDF
职称材料
题名
协同业务过程的随机行为分析方法
8
作者
赵莹
潘华
孙金艳
莫启
代飞
机构
云南电力调度控制中心
云南云电同方科技有限公司
云南大学软件学院
西南林业大学大数据与智能工程学院
出处
《计算机工程与应用》
CSCD
北大核心
2019年第3期245-251,265,共8页
基金
国家自然科学基金(No.61462095
No.61702442)
云南省自然科学基金(No.2016FB102)
文摘
参与组织随机行为是评价业务协同有效实施的一个关键因素。结合进程代数和马尔科夫链,提出了一种协同业务过程的随机行为分析方法。首先,使用有限状态自动机建模每个参与组织的业务过程,通过引入异步消息通信关系定义协同业务过程。其次,提出将参与组织业务过程转换成通信顺序进程(Communication Sequential Process,CSP)方法,进而将每个参与组织业务过程对应CSP进程并发组合得到协同业务过程对应的CSP进程,并根据CSP操作语义构建协同业务过程的状态迁移模型。最后,引入状态迁移模型正则化概念,从理论上证明正则化的状态迁移模型与一个齐次马尔科夫链相对应,进而根据平衡方程求得状态迁移系统中每个状态的稳定概率,以此为基础实现参与组织随机行为分析。通过对电设备采购过程建模与随机行为分析阐述该方法的可行性和有效性。
关键词
协同业务过程
异步消息
通信
随机行为
通信
顺序进程
(
csp
)
马尔科夫链
Keywords
collaborative business process
asynchronous message communication
random behavior
Communication Sequential Process(
csp
)
Markov chain
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
一种设计通信顺序进程通道服务的方法
赵扬
《上海电机学院学报》
2019
0
下载PDF
职称材料
2
基于进程迹的CSP模型验证框架
赵岭忠
翟仲毅
钱俊彦
《计算机科学》
CSCD
北大核心
2013
3
下载PDF
职称材料
3
基于Petri网的CSP并发系统验证技术研究
刘彦青
赵岭忠
钱俊彦
《计算机科学》
CSCD
北大核心
2015
1
下载PDF
职称材料
4
基于CSP的CTCS-1级列控系统RDC数据验证的研究
卢铃冉
张勇
《铁路计算机应用》
2019
0
下载PDF
职称材料
5
基于广义污点传播模型的操作系统访问控制
杨智
殷丽华
段洣毅
吴金宇
金舒原
郭莉
《软件学报》
EI
CSCD
北大核心
2012
7
下载PDF
职称材料
6
采用函数式语言的BPEL模型形式化验证方法
祝义
黄志球
周航
《计算机科学与探索》
CSCD
北大核心
2018
5
下载PDF
职称材料
7
Powerlink协议异步调度机制的建模与分析
陈睿
庞海萍
郝丽
厉达
杨栋
《计算机工程与应用》
CSCD
北大核心
2019
2
下载PDF
职称材料
8
协同业务过程的随机行为分析方法
赵莹
潘华
孙金艳
莫启
代飞
《计算机工程与应用》
CSCD
北大核心
2019
0
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部