基于细胞膜演算的Web服务事务处理形式化描述与验证.pdf

第29卷第7期 计 算 机 学 报 v01．29No．7 20弱年?嚣 OFCOMPUT嚣RS 2006 C瓣lNES嚣JoU歉NAL july 基于细胞膜演算的Web服务事务处理 形式化描述与验证 戚正伟 尤晋元 (上海交通穴学诤篓税科学专工程系上海2∞030) 攘要采廷缨魃貘演算英诲势擀了当蘩鹱：较主滚瓣web鞭务孛藏予事务协调蛰议WS—A零，钤对WS—AT携议 采用简单的状态转换表和转换图，无法描述协调者和多个参与者的复杂协调满动，采用细胞膜演算给出了其形式 化接述，殿予规范协调者和参与者的活动，势分析了该协议的活性和安全性，毒棼到了38187个状态．模溅检验的实 验结果表鞠，该协议满足稳定性、一致性和非平凡性，而不满怒菲阻塞性．迸丽，分析出注册和协调协议混在一熬是 其不满足jB阻塞性的原因． 关键词 细胞膜演算；事务处理；形式化方法 审黧法分类号TP3ll The a珏dVeri髓ca耋io鼗of Forl糕啦SpeeiⅨea重ion Tra建s凌etio珏p1．oeessi珏g inWebSerVicesMembrane by Calculus QI YOUJi卅Yuan Zheng—Wei 200030) (Dg艇一雠#挖}。，Comp甜f。rSfl#牲钟n删≠王法gi箨乎#疵瑶g，S施ng矗8i歹玩#￡D嚣g魄f钟i移，s矗∞g矗蘸 It to Abstractis asuitableformalnlethodto and transac— irnportantadopt specifyverifycomplex tionsinWebservices．Theauthorshave afofmal calledMenlbraneCalculusto developedmethod describetheabstractmodelin transactions．This extendsMembraneCalculus running long paper to t|le atomictransactioncofnmit Duetot圭le State anaiyzepractical protocol习矿S—AT． silnple TransitionTableand cannotdescribethe activitiesbetween Chart，WS—AT complexcoordination thecoof蠢inatorandseveral Calc毪lusis thebe— participants。≥渡efnbraneuse鑫to量ormallyspeeify