![](https://csdnimg.cn/release/download_crawler_static/88749925/bg4.jpg)
S. Nakajima/Electronic Notes in Theoretical Computer Science 151
(
2006
)
89
2.3
相关工作
Web
服务流程的形式化验证的最早工作可以追溯到
S. Narayanan
和
S.A.
Mcllraith
使用
Petri-net
进行自动分析
[13]
。然而,他们不研究与
Web
服务
标准相关的语言。
针对标准技术的第一个提案是
WSFL
和
XLANG
在
2001
年
5
月宣布的。
和
S. Nakajima
提到了一个使用模型检查技术来分析
WSFL
的基本思想
[9][10]
。尽管
WSFL
已经过时,但处理并发的基本技术(包括
DPE
)仍然
适用于
Windows
。使用
SPIN
模型检查器的详细技术见
[11].
本文采用同样
的技术来处理面向对象的数据处理过程,并研究了用模型检查器来分析
面向对象的应用程序所需要的技术。抽象技术是必不可少的。
目前,对可重构数据库的形式化分析大多采用基于进程代数的形式化
方法。
H. Foster
等人使用
FSP
和
LTSA
模型检查器来建模和分析可移植程
序
[3]
。
M.
科什金娜和
F. van Breugel在他们的工作中使用了CCS和并发控制(CWB-NC)
[7]
。
G. Salaun
等人还使用
CWB-NC
进行行为分析
[14]
。对于
DPE
,
F.van Breugel和M.Koshkina [1]给出了一个有趣的分析,即执行结果可
能会因是否引入DPE而不同,从而留下无意的
副作用
。最后,X。Fu
等人通过使用抽象技术以及行为规范来处理数据方面的问题,并使用
SPIN
模型检查器
[6]
。然而,抽象技术并不总是可靠的。
3
行为规范
3.1
行为规范
3.1.1
基本工艺描述
基本的计算元素是表示原子操作的活动。
EJB
提供了三种活动来与外部
Web
服务提供者交换信息:调用、接收和应答。
invoke
活动表示通过特
定的合作伙伴链接调用
Web
服务提供者的原子操作,并等待结果。
<invoke
partnerLink=“assessor”portType=“riskAssessmentPT”operation=“check”i
nputVariable=“request”outputVariable=“risk”>
除了通信原语活动之外,
为访问变量分配
Activity
。 它还开展其他活动,