论文部分内容阅读
两阶段提交协议是最简单且最常用的原子提交协议，该协议使分布式事务的提交具有原子性和持久性。在本文中，我们使用π演算对两阶段提交协议进行描述，并对其正确性进行了证明，进一步体现了π演算对于描述进程通信及并行性的独特优势。
使用π-演算验证两阶段提交协议
【摘 要】
：
两阶段提交协议是最简单且最常用的原子提交协议，该协议使分布式事务的提交具有原子性和持久性。在本文中，我们使用π演算对两阶段提交协议进行描述，并对其正确性进行了证明，进一
【机 构】
：
国防科技大学计算机学院,北京航空航天大学计算机学院
【出 处】
：
计算机科学
【发表日期】
：
2006年11期
其他文献
面向对象形式规格说明语言Obiect-Z与进程代数CSP相结合是当今的一个热点，它既可以表示复杂的模块化数据与算法，又可以表示系统的行为，但求精与验证对它们结合后的规格说明需要
NoteExpress是一种具有文献检索、文献整理、引文标注、在文末自动按特定格式生成参考文献列表等强大功能、并且完全支持中文的软件。它可嵌入MSWord环境使用，还可以直接通过
针对嵌入式实时系统复杂动态交互行为和严格实时的领域特征,提出了一种软件需求规约语言RTRSM*.该语言以扩充的层次并发有穷状态机HCA为核心,以支持合成的模板为基本组成单元
