题名 CTCT-4级安全通信协议的形式化建模与验证
被引量：7
1
作者
胡晓辉 陈慧丽 石广田 陈永
机构
兰州交通大学电子与信息工程学院 兰州交通大学艺术设计学院
出处
《计算机工程与应用》
CSCD
2014年第4期81-85,共5页
基金
国家自然科学基金(No.61163009)
文摘
CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统,而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施,引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信,并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。
关键词
GSM-R 安全协议 通讯顺序进程(csp ) 故障 偏差 精炼检测器(FDR)
Keywords
GSM-R security protocol communicating sequential process （csp ）Failures Divegences Refinement checker（FDR）
分类号
TP391.9
[自动化与计算机技术—计算机应用技术]
题名 采用函数式语言的BPEL模型形式化验证方法
被引量：5
2
作者
祝义 黄志球 周航
机构
南京航空航天大学计算机科学与技术学院 江苏师范大学计算机科学与技术学院
出处
《计算机科学与探索》
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
[自动化与计算机技术—计算机软件与理论]
题名 体系结构动态演化中的构件行为分析
被引量：3
3
作者
黄崇德 彭鑫 赵文耘
机构
复旦大学信息科学与工程学院软件工程实验室
出处
《计算机工程与应用》
CSCD
北大核心
2007年第10期87-92,共6页
基金
国家自然科学基金(the National Natural Science Foundation of China under Grant No.60473061) 国家高技术研究发展计划(863)(theNational High- Tech Research and Development Plan of China under Grant No.2005AA113120)
文摘
在体系结构演化的过程中,关闭运行时系统升级的代价增高和频繁改变的业务需求使得研究者考虑动态的软件升级机制.但在体系结构的动态升级过程中,由于构件风格、功能及交互方式等方面的差别,强制的构件升级会影响系统的稳定性和正确性。从构件行为的角度考虑,采用基于Wright的软件体系结构描述语言和通信顺序进程中对于进程的描述方法,描述构件行为并在构件替换之前分析原构件和新构件间的行为特性,在演化前确认构件的行为一致性,从而保证动态升级过程的正确性和合法性,以及提高系统演化的自适应性。
关键词
软件体系结构 动态升级 构件行为 csp WRIGHT
Keywords
software architecture dynamic update component behavior communicating sequential process （csp ） Wright
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 基于通信序列进程的UML序列图形式化方法
被引量：1
4
作者
邓建波 张立臣 邓惠敏 徐碧红
机构
广东工业大学计算机学院 吉首大学数学与计算机科学学院
出处
《计算机应用》
CSCD
北大核心
2010年第10期2727-2729,2734,共4页
基金
国家自然科学基金资助项目(90818008 60774095 60474072Z)
文摘
UML2.0序列图是一种描述对象之间动态协作和事件发展时间关系的视图,但是UML序列图缺乏精确的形式化语义,所以不利于对其所描述的系统进行形式化验证。为此,根据UML2.0语义文档及组合碎片包概念,基于通信序列进程(CSP)给出了UML序列图的基本元素和消息迹的形式化定义及生成规则,实现了UML序列图的形式化,为UML序列图在描述系统准确性和有效性方面提供了形式化的检验方法。最后通过ATM实例说明UML序列图这一过程的正确性。
关键词
UML2.0序列图 形式语义 组合碎片包 通信序列进程
Keywords
UML2. 0 sequence diagram formal semantics combined fragrnen（ packet communicating sequential process （csp ）
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
题名 一种利用CSP转换UML活动图模型的方法
5
作者
沈晓奕 杨德仁
机构
宁夏医科大学公共卫生与管理学院 宁夏医科大学理学院
出处
《计算机与数字工程》
2019年第7期1565-1570,共6页
基金
国家自然科学基金项目“可信工作流管理系统的关键技术及其标准化研究”(编号:61862001) 宁夏医科大学教学专项改革项目“全景式IT类课程‘四融一拓’教改设计与探索”(编号:NYJY1822) 宁夏医科大学研究生创新创业项目“共享医院业务过程模型仿真研究”(编号:YJSCXCY2018006)资助
文摘
为了研究UML活动图模型中可中断活动区间、嵌套的层次活动图等高级构造子的形式化表示,依据进程代数理论,采用一种利用CSP转换UML活动图模型的方法。建立了UML活动图元模型捕获活动图语言的主要概念和属性并依据元模型的类图将建模语言的抽象语法形式化,并给出了以“活动”为中心的形式化表示机制。共享医疗业务流程管理为案列研究背景,对活动图模型高级构造子形式化验证,结果表明CSP代数理论不仅能够对活动图模型进行表示,而且能够对共享医院业务流程多层次、全方面地进行分析。
关键词
UML活动图 元模型 形式化 通讯顺序进程(csp ) 进程代数 PETRI网 共享医院
Keywords
UML activity diagrams meta model formalizing communicating sequential process (csp ),process algebraPetri net shared hospital
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
题名 基于通信顺序进程的OWL-S语义分析与建模
被引量：2
6
作者
杨建书 吴尽昭 周瑾
机构
中国科学院成都计算机应用研究所
出处
《计算机应用》
CSCD
北大核心
2010年第8期2173-2176,2196,共5页
基金
国家973计划项目(2007CB310803) 国家863计划项目(2007AA01Z143) +2 种基金 国家自然科学基金资助项目(60873118 60973147) 北京交通大学科学研究基金资助项目(2007RC110)
文摘
为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。
关键词
OWL-S过程模型 自动化验证 通信顺序进程 形式化语义 建模
Keywords
Ontology Web Language for Services OWL-S process model automatic verification communicating sequential process csp formal semantics modeling
分类号
TP301.2
[自动化与计算机技术—计算机系统结构]
