补偿通信顺序进程的扩展及失败发散语义
ＣＮ４３—１２５８／ＴＰＩＳＳＮ１００７—１３０Ｘ
计算机工程与科学
ＣＯＭＰＵＴＥＲＥＮＧＩＮＥＥＲＩＮＧ＆ＳＣＩＥＮＣＥ
２０１０年第３２卷第３期
Ｖ０１．３２，Ｎｏ．３，２０１０
Ｉｌ—Ｉ一１…＿Ｉ一＿…Ｉ－●ｌ●Ｉ＿－●ｌ●ｌｌＩ●●ＩＩ＿●－ｌ●ＩＩ●ｌｌＩ－ｌ－ｌ－ｌ●Ｉｌ●ｌ●文章编号：１００７～１３０Ｘ（２０１０）０３—００８９—０７
补偿通信顺序进程的扩展及失败发散语义。
ＡｎＥｘｔｅｎｄｅｄｃＣＳＰｗｉｔｈ
ＦａｉｌｕｒｅＤｉｖｅｒｇｅｎｃｅＳｅｍａｎｔｉｃｓ
陈振邦，王戟。齐治昌
ＣＩｔＥＮｚｉｇ－ｂａｎｇ，ＷＡＮＧＪｉ。ＱＩＺｈｉ－ｃｌｍｌｇ
（国防科学技术大学计算机学院。湖南长沙４１００７３）
（ＳｃｈｏｏｌｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ－ＮａｔｉｏｎａｌＵｎｉｖｅｒｓｉｔｙｏｆＤｅｆｅｎｓｅＴｅｃｈｎｏｌｏｇｙ，Ｃｈａｎｇｓｈａ４１００７３。Ｃｈｉｎａ）摘要：补偿通信顺序进程（ｃ（靴）是通信顺序进程用于长事务建模的扩展，可用来描述服务计算中的编制程序，比如ＷＳ－ＢＰＥＬ程序。目前，ｃＣＳＰ只有操作语义和基于迹的指称语义，对死锁和发散行为的推理支持不够。本文扩展了ｃＣＳＰ，引入新的组合操作子，给出扩展ｃＣｓＰ的失败发散语义；并根据该语义，给出新引入组合操作子的重要代数规则，用于语义的理解和佐证。最后，给出一个案例描述用于展示扩展ｃＣＳＰ。
Ａｂｓｔｒａｃｔ：ＣｏｍｐｅｎｓａｔｉｎｇＣＳＰ（ｃＣＳＰ）ｉｓａｎｅｘｔｅｎｓｉｏｎｔＯＣＳＰｆｏｒｍｏｄｅｌｉｎｇｌｏｎｇ－ｒｕｎｎｉｎｇｔｒａｎｓａｃｔｉｏｎｓ．ＩｔｃａｎｂｅｕｓｅｄｔＯｓｐｅｃｉｆｙｔｈｅｐｒｏｇｒａｍｓｗｒｉｔｔｅｎｉｎｏｒｃｈｅｓｔｒａｔｉｏｎｌａｎｇｕａｇｅｓ，ｓｕｃｈａｓＷＳ－ＢＰＥＩ．ｃＣＳＰｈａｓｏｎｌｙａｎｏｐｅｒａｔｉｏｎａｌｓｅｍａｎｔｉｃｓａｎｄａｔｒａｃｅｓｅｍａｎｔｉｃｓｔｈａｔａｒｅｎｏｔｅｘｐｒｅｓｓｉｖｅｅｎｏｕｇｈｆｏｒｒｅａｓｏｎｉｎｇａｂｏｕｔｄｅａｄｌｏｃｋａｎｄｄｉｖｅｒｇｅｎｃｅ．ＷｅｅｘｔｅｎｄｃＣＳＰｗｉｔｈｍｏｒｅｏｐ—ｅｒａｔｏｒｓａｎｄｄｅｆｉｎｅｆｏｒｉｔａｆａｉｌｕｒｅ－ｄｉｖｅｒｇｅｎｃｅ
ｓｅｍａｎｔｉｃｓ．ＴｈｅｓｉｇｎｉｆｉｃａｎｔａｌｇｅｂｒａｉｃｌａｗｓａｒｅｐｒｅｓｅｎｔｅｄｆｏｒｔｈｅｎｅｗｏｐｅｒａｔｏｒｓｗｉｔｈｒｅｓｐｅｃｔｔＯｔｈｅｎｅｗｓｅｍａｎｔｉｃｓｆｏｒｉｔｓｊｕｓｔｉｆｉｃａｔｉｏｎａｓｗｅｌｌａｓｆｏｒｕｎｄｅｒｓｔａｎｄｉｎｇ．Ｉｎａｄｄｉｔｉｏｎ，ｆｌｃａｓｅｓｔｕｄｙｉｓｇｉｖｅｎｔＯｄｅｍ－ｏｎｓｔｒａｔｅｔｈｅｅｘｔｅｎｄｅｄｃＣｓＰ．
关键词：补偿通信顺序进程；指称语义；失败发散语义；代数规则
Ｋｅｙｗｏｎｂ：ｃｏｍｐｅｎｓａｔｉｎｇＣＳＰ；ｄｅｎｏｔａｔｉｏｎａｌｓｅｍａｎｔｉｃｓ；ｆａｉｌｕｒｅ－ｄｉｖｅｒｇｅｎｃｅｓｅｍａｎｔｉｃｓ；ａｌｇｅｂｒａｉｃｌａｗ
ｄｏｉ：１０．３９６９／ｊ．ｉｓｓｎ．１００７—１３０Ｘ２０１０．０３．０２６
中图分类号：ＴＰ３１１文献标识码：Ａ
１引言
随着面向服务计算研究的发展，长事务（Ｌｏｎｇ－ＲｕｎｎｉｎｇＴｒａｎｓａｃｔｉｏｎ，简称Ｉ。ＲＴ）模型引起了广泛的关注［１］。在面向服务的系统中，一个任务通常需要广泛分布的不同计算实体通过通信来协作完成。服务计算中的事务一般会持续较长时间，其中包括和不同的服务提供组织的交互。传统的原子事务模型的条件对于这种情况过于严格，比如原子事务模型中的资源隔离［１］。长事务能够通过补偿机制来应对这种问题，使系统在错误发生后恢复到相对一致的状态，从而保证了事务的原子性。
目前，工业界出现的服务组合语言，比如ｗＳＢＰＥＩ』引、ｘＩ。ＡＮｄ３１，都可以描述服务组合过程中的长事务。同时，也有一些形式化的语言，可用于长事务的描述和推理，比如ＳｔＡＣｔ“、Ｓａｇａｓ［５］和ｃＣＳｌｘ６１。这些形式化的语言不仅可以用于工业语言的形式语义的解释，而且还可以帮助开发人员理解长事务模型的主要特征。此外，基于这些形式语言的形式化技术和工具还可以用于长事务的分析和验证。
补偿通信顺序进程（ＣｏｍｐｅｎｓａｔｉｎｇＣＳＰ，简称《ＳＰ）是通信顺序进程（ＣｏｍｍｕｎｉｃａｔｉｏｎＳｅｑｕｅｎｔｉａｌＰｒｏｃｅｓｓ，简称ＣＳＰ）［７３的扩展，用于长事务模型的描述和验证。－ｃＣＳＰ中的错误恢复机制与经典长事务模型Ｓａｇａｓ［８］中的后向恢复一致。ｃＣＳＰ中的进程有两种类型：标准进程和可补偿进程。标准进程是对（Ⅻ子集的扩充，加入了异常处理和事务块；可补偿进程用于描述长事务。文献Ｅ６］中给出了ｃＣＳＰ基于迹的指称语义，文献［９］中给出了ｃＣＳＰ的操作语义，两种语义的一致性在文献［１０］中给出了证明。然而，
?收稿日期：２００９－０１—０６；修订日期：２００９—０３—１２
基金项目：国家９７３计划资助项目（２００５ＣＢ３２１８０２）；自然科学基金资助项目（９０６１２００９，６０８０３０４２）
作者简介：陈振邦（１９８１一），男，湖北黄陂人，博士生，研究方向为软件体系结构、面向服务的软件工程和软件验证；王戟，博士，教授，博士生导师，研究方向为形式化方法、高可信软件工程；齐治昌．教授，博士生导师，研究方向为软件工程。
通讯地址：４１００７３湖南省长沙市国防科学技术大学计算机学院博士生队２００４级；Ｔｅｌ：１３５７４８６６８３２；Ｅ－ｍａｉｌ：ｚｂｅｈｅｎ＠ｎｕｄｔ．ｅｄｕ．饥Ａｄｄｒｅ髂：Ｇｒａｄｅ２００４．ＤｏｃｔｏｒａｌＢｒｉｇａｄｅ，ＳＣｈｏｏｌｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅ。ＮａｔｉｏｎａｌＵｎｉｖｅｒｓｉｔｙｏｆＤｅｌｅｎｓｅＴｅｃｈｎｏｌｏｇｙ。Ｃｈａｎｇｓｈａ。Ｈｕｎａｒｌ４１００７３，Ｐ．ＲＣｈｉｎａ
８９万方数据