论文部分内容阅读
Mobile Ambient演算是一种描述进程和设备移动的形式化方法,但其移动进程的实时性目前尚未有合适的形式化表达。通过对Mobile Ambient演算进行实时扩充,提出了一种离散时间域的时间Mobile Ambient演算(DTMA),并为DTMA演算定义了模态逻辑。基于DTMA演算及其模态逻辑的子集给出了模型验证算法,提出了一种对BPEL4WS程序的形式化建模方法,实现了业务流程的活动可达性的模型验证。