时间相关移动并发系统是以并发性、移动性、时间相关性和异构性等为主要特征的计算系统。对于这类系统,特别是安全攸关的时间相关移动并发系统,如移动支付系统、移动通信系统、交通控制系统等,其失误和崩溃可能会造成重大损失,因此时间相关移动并发系统的正确性、安全性等质量属性受到人们的普遍重视。对时间相关移动并发系统采用以严格数学理论为支撑的形式化方法进行建模、验证与测试是行之有效的减少系统设计错误和保证系统质量的重要途径。进程代数,作为形式化方法的代表,是一种重要的用于对并发系统进行建模和验证的技术。由于所面向的领域和应用背景的不同,涌现出很多进程代数的分支和变种,其中演算就是用于建模移动性的重要的分支。近年来,由于新型网络技术和信息技术的不断发展,使得能够建模和验证移动系统的演算得到人们的广泛关注。但是,演算在对系统建模时并未考虑到动作执行所占用的时间以及系统在某个状态所持续的时间,故而,使得它不适于对时间相关系统进行建模、验证和测试。为了对时间相关移动并发系统进行建模和验证,本文研究了添加时间相关特性的扩展的演算。在此基础上,提出采用扩展演算为时间相关移动并发系统进行建模和推演的方法。进一步地,为了对扩展演算建模的系统进行自动验证,提出将扩展演算转换为建模、仿真验证语言MSVL的方法。此外,为了对扩展演算建模的系统进行测试,文章还给出了采用扩展演算的测试用例生成方法。所取得的研究成果主要有以下几个方面。(1)建立了带区间动作前缀的扩展演算p-π,定义了p-π的语法和操作语义,给出了p-π的代数性质和时间相关性质并对其进行了证明。在此基础上给出了p-π对时间相关行为的建模。此外,还通过实例对p-π的应用效果和相应性质所起的作用进行了分析和说明。(2)提出了采用扩展演算对时间相关移动并发系统进行建模和推演的方法。采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,基于上述迁移系统和执行路径完成对系统性质的推演。通过移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。(3)提出了从扩展演算p-π到MSVL的转换方法。为了完成转换,先在MSVL中对通道和通信原语进行了定义。基于该定义,给出了从p-π到MSVL的结构化转换规则,并对二者采用的通信机制间存在的一致性进行了证明。为了说明转换的合理性,文章还证明在p-π进程和MSVL的格局间存在互模拟关系。这样,通过转换,就可以借助MSVL建模仿真验证工具完成对p-π进程的验证。(4)提出了基于扩展演算的测试用例生成方法。采用p-π为时间相关并发系统建模并由p-π的操作规则构造出系统模型的时间相关标记迁移系统。基于时间相关标记迁移系统和用例规约生成测试用例,测试用例的生成满足执行动作覆盖准则、路径覆盖准则和时间约束覆盖准则,并给出了测试用例的选择策略。同时通过p-π的验证方法,还保证了所产生的测试用例的正确性。