论文摘要
自顶向下逐步细化的层次化设计方法，是人们广泛接受的设计计算机硬件系统和软件系统的最主要方法之一，动作细化是系统层次化刻画方法的核心操作。具体应用到软件的模块设计中，有时需要比较系统在不同抽象层次上的描述，检验它们能否实现相应的功能，伴随系统描述抽象层次的改变，相应的原子级动作集也在改变。当系统不同抽象层次的动作集确定以后，另一种垂直模块化的方法就应运而生了，它不同于前面水平模块化的方法，垂直模块化的方法是先将复杂的系统描述成简单的、抽象的形式，然后一步一步细化成实际的、复杂的执行过程；这种描述，连同建立在描述之上的分析，可以一层一层的进行，这样每次只是专注于从上一个层次到这一个层次的相关细节。这个著名的方法就是通常被称为分层描述的方法。这种方法在顺序系统中的运用很成功，产生了“自上而下”的系统设计方法，“自上而下”的设计方法将宏观的功能模块一层一层的细化，直到最底级的执行代码，我们要探讨的动作细化，就是运用数学的方法来描述这一问题，为各种动作细化建立模型，探讨动作细化的操作语义和指称语义。本文系统阐述了动作细化理论的各个分支，具体包括：原子动作细化与非原子动作细化。原子动作细化是指：在动作细化以前，动作在相应的描述层次上是原子级的，原子动作经过细化变成一个进程后，原来动作执行的原子性继续保留。非原子细化，是一种更加自由的、松散的动作细化，这种观点的依据是动作的原子性只对于特定的描述层次，对于其他抽象描述层次上，动作间执行的关系根据特定的抽象层次，会发生相应的改变，即在某一个特定的描述层次上，所有的动作都是原子级的，细化到更具体的层次上，原来原子级的动作将可能细化成其他的非原子级的执行关系，这种动作细化后优化了进程的执行，但是对原来进程间的执行关系会造成某种程度上会破坏。不论是原子动作细化，还是非原子动作细化，在本质上都有两种解释方法：语法上的和语义上的。解释表现在语法上，主要是动作细化对于过程调用的拷贝式处理，比如顺序程序设计中嵌入主程序的动作调用。在语义的解释中，用来解释进程语句的的替换操作都定义在一个语义域中。t[a→u]的语义可以用这种操作来定义。例如，有时我们将语义的域构建在事件结构(Event Structure)上，而事件结构ε=[u]代表u的语义，可以被事件结构[t]中每个标签为a的事件d所替换。在事件结构域中动作细化的语义是保持的：包括进程间的冲突关系、顺序执行关系等等。当我们把动作细化当成对于语言的一个操作算子时，很自然的出现一个关键性问题：如何找到这个操作算子基于全等的等价关系。经典的进程代数提供了互模拟等价关系，这种等价关系就是基于交织语义的，交织语义在解释非并发进程间的等价关系是很有说服力的，但是复杂系统中包含大量的并发进程，交织语义对于并发进程间的等价关系的描述是不完全的，有些片面。本文对于等价关系的探讨，主要集中在真并发语义上。另一种以更加弱化的方法来处理动作细化问题的方法：就是不要将操作细化作为一个算子来对待，而是将动作细化看作是一种执行关系。在很长的一段时间内，人们将动作细化理论建立在这样一种认识上：就是当进程I相对于进程S更加便于直接执行，特别是针对选择算子时有更加明确的语义的时候，我们就将进程I当作是另一个进程S的一个执行。在探讨了经典动作细化的各种理论分支以后，很多研究人员意识到经典的动作细化缺乏数量上的约束，鉴于此，本文对动作细化理论中的原子动作细化理论进行了实时、随机和概率三个方面的扩展。对动作细化理论扩充的数量约束，每一种都有特定的现实背景和应用。实时的模型中，对进程执行的时间控制添加了超时算子，即一个进程如果在允许的时间内没有完成相应的动作，那么就会激活一个超时操作，原动作被禁止执行，系统开始执行一个新的动作(进程)。对于随机模型，我们将马尔可夫链引入进程代数中，这个模型的引入对于评价系统的性能带来和很大的方便，这种模型将概率和时间两个因素同时引入了动作细化理论，动作的执行有了自己的概率和执行时间，更加贴近于现实中的情况。概率事件在现实的生产生活中普遍存在和发生，因此，我们将概率模型也引入了动作细化理论。针对上面提到的每一种数量约束，我们首先给出相应的系统描述语言，其次给出语言上的操作语义，然后根据数量约束的需要，我们对事件结构扩充了实时、随机和概率三个数量约束，针对添加了数量约束的事件结构，我们给出了相应的指称语义，针对上面提到的数量约束，我们都证明了动作细化在语义上和语法上是重合的，对于历史保留互模拟和偏序多集迹两种等价关系都是保持的。