摘要: 对于复杂的并发系统的刻画和分析，形式化方法是一种常用和有效的方法。通过严格定义的语法和语义，形式化方法可以使得对系统的刻画和分析都基于严格的数学框架，更利于人们对复杂系统的本质特征的掌握。动作精化是在并发理论当中一种很重要的层次化设计和刻画方法。它允许将并发系统在不同层次上进行刻画，通过不断精化上层的抽象动作，改变系统的抽象层次，直到最底层的实现。目前，基于无时间指标的并发系统的动作精化理论已经研究得比较透彻了，在这种传统的动作精化理论中，系统模型采用的是无时间指标的事件结构，这是一种真并发的系统模型，动作精化作为一种操作算子来看待，并且动作的执行是不消耗时间的。然而，对于并发系统来说，时间指标是一个至关重要的因素，很多现实生活中的并发系统都跟时间密切相关，另外，紧急事件在实时并发系统中也是常见的现象，在已研究的动作精化理论当中紧急事件都仅仅只限于用来模拟超时事件，并且是不能被精化的，这对于很多现实系统来说是一个很大的限制。基于此，本文扩展了传统的动作精化理论，研究具有时间指标的并发系统的动作精化理论，在我们研究的并发系统中，时间指标是系统的一个重要参数，动作的执行也是需要消耗时间的，并且紧急事件也被扩充到可以是任何事件，而不仅仅是超时事件。在系统模型的结构表示上，本文扩充了传统的事件结构，使用一种带时间信息的捆绑式事件结构来模拟系统行为，在系统模型的语言刻画上，本文采用的是带时间的类LOTOS进程代数描述语言，对于动作精化，我们同样采用算子的观点，将动作精化定义为一个操作算子。本文的主要贡献是研究了这种更一般的并发系统的动作精化理论，证明了我们的动作精化具有通常期望的以下一些性质：（1）正确性。即精化后的系统行为可以由精化前的系统行为和用于替换原系统动作的子系统的行为组合推导出来；（2）同余性。在并发理论的研究中，等价关系是一个非常重要的概念，它用于比较和区分并发系统的行为，本文提出的动作精化操作在两种重要的等价关系下是同余的，这两种等价关系分别是线性时间的Pomest迹等价和分支时间的历史保持双模拟等价；（3）语法精化和语义精化的一致性。本文分别在语法和语义层次上对动作精化进行了定义，并证明了这两个层次的动作精化在前述两种等价关系下，关于一种基于完全偏序的指称语义是一致的。经过扩充，本文提出的动作精化理论更具有一般性和实用性。