随着计算机技术的深入发展和计算机软件在生产生活中的广泛应用,软件的正确性验证成了人们关心的重要问题。而模型检查作为一种软件正确性验证的方法,受到工业界广泛认同。它通过对系统的建模和对性质的逻辑公式化描述,实现了对软件系统的自动化验证。　　 针对工作流系统移动性、离散型、时效性和长时间事务的特性,本文提出了一个π演算的带时间和中断的扩展:πit演算。通过πit演算,我们可以更好的对工作流系统进行建模。在给出πit演算语法和语义的同时,我们还给出了一套πit演算的行为类型系统。结合行为类型系统和浅层逻辑系统,我们就可以使用模型检查的方法对工作流系统的性质进行验证。　　 本文还针对两种不同的规范--侧重网络服务的BPEL/BPEL4People和侧重实时性系统的MARTE顺序图--分别进行了基于πit演算的建模,展现了πit演算的描述能力,并给出了BPEL,BPEL4People和MARTE顺序图的形式化语义。　　 本文的主要工作表现在以下几个方面:　　 (1)提出了时序可中断演算πit,在传统π演算的基础上增加了对时间和中断事件的描述能力。　　 (2)给出了πit演算的行为类型系统,结合浅层逻辑,提供了对πit演算进程性质的描述和验证方法。　　 (3)使用πit演算对BPEL和BPEL4People进行建模,给出了其形式化语义。　　 (4)分别用πit演算和浅层逻辑公式对MARTE顺序图的主要元素和非功能性时间约束进行建模和描述,给出了MARTE顺序图的形式化语义。我们在πit演算中引入了离散的时间单元前缀ε,通过ε前缀,我们可以在描述时间的同时保持与传统π演算转换规则的一致性。同时,通过引入计时器算子Timer和中断算子Task,我们实现了通过时间和通道两种手段来中断当前进程,转而执行另一个进程的方法。这使得πit演算可以更好建模超时事件和长时间运行的事务。最后,通过对BPEL/BPEL4People主要活动和MARTE顺序图的建模,我们给出了它们清晰的语义,并提供了检验其性质的方法。