期刊文献+
共找到4篇文章
< 1 >
每页显示 20 50 100
基于Pi-Calculus的跨组织工作流建模方法
1
作者 潘晓华 冯志林 +2 位作者 尹建伟 郑正平 董金祥 《计算机应用研究》 CSCD 北大核心 2006年第1期63-65,76,共4页
针对跨组织协同环境下的业务流程建模技术的不足,提出了一个新的用于跨组织业务流程的形式化建模方法。首先根据工作流管理联盟(W fMC)的有关工作流过程定义接口规范,利用Pi-Calculus技术对跨组织业务流程结构进行了形式化定义。此外,利... 针对跨组织协同环境下的业务流程建模技术的不足,提出了一个新的用于跨组织业务流程的形式化建模方法。首先根据工作流管理联盟(W fMC)的有关工作流过程定义接口规范,利用Pi-Calculus技术对跨组织业务流程结构进行了形式化定义。此外,利用Pi-Calculus特有机制对并发流程及其之间的通信进行描述。提出的方法可以有效用于不同业务流程间的协同工作,并且适合于对分布式协同环境下的工作流进行建模。 展开更多
关键词 工作流建模 picalculus 跨组织流程
下载PDF
Formal Analysis of Trusted Platform Module Commands for Compromising User Key 被引量:2
2
作者 Qin Yu Zhao Shijun Zhang Qianying 《China Communications》 SCIE CSCD 2012年第10期91-102,共12页
The Trusted Platform Module (TPM) is a dedicated hardware chip designed to provide a higher level of security for computing platform. All TPM functionalities are implemented in TPM corntrends to achieve specific sec... The Trusted Platform Module (TPM) is a dedicated hardware chip designed to provide a higher level of security for computing platform. All TPM functionalities are implemented in TPM corntrends to achieve specific security goals. We attempt to analyze the security properties of these commands, especially the key management API. Our study utilizes applied pi calculus to forrmlize the commands and determine how their security properties affect TPM key rmnagement. The attacker is assumed to call TPM comrmnds without bounds and without knowing the TPM root key, expecting to obtain or replace the user key. The analysis goal in our study is to guarantee the corre- sponding property of API execution and the integrity of API data. We analyze the security properties of TPM commands with a process reduction method, identify the key-handle hijack attack on a TPM newly created key, and propose reasonable solutions to solve the problem. Then, we conduct an experiment involving a key-handle attack, which suc- cessfully replaces a user key with an attacker's key using lmlicious TPM software. This paper discloses the weakness of the relationship between the key handle and the key object. After the TPM software stack is compromised, the attacker can hunch a keyhandle attack to obtain the user key and even break into the whole storage tree of user keys. 展开更多
关键词 trusted computing TPM TPM command applied pi calculus Api analysis
下载PDF
Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows 被引量:2
3
作者 曹军威 张帆 +2 位作者 许可 刘连臣 吴澄 《Journal of Computer Science & Technology》 SCIE EI CSCD 2011年第6期1017-1030,共14页
With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to en... With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis (RRA) approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification. 展开更多
关键词 grid computing workflow management formal verification state pi calculus
原文传递
Formal verification technique for grid service chain model and its application 被引量:2
4
作者 XU Ke WANG YueXuan WU Cheng 《Science in China(Series F)》 2007年第1期1-20,共20页
Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on sta... Ensuring the correctness and reliability of large-scale resource sharing and complex job processing Is an Important task for grid applications. From a formal method perspective, a grid service chain model based on state PI calculus Is proposed In this work as the theoretical foundation for the service composition and collaboration in grid. Following the Idea of the Web Service Resource Framework (WSRF), state PI calculus enables the life-cycle management of system states by associating the actions in the original PI calculus with system states. Moreover, model checking technique is exploltad for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effectiveness of the proposed work. 展开更多
关键词 GRID grid service chain formal method model checking state pi calculus
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部