许多分布式算法，包括TTP/C的中央算法，进行一系列的回合运算，可以很容易地描述为递推函数。接着，正确性证明通常或多或少涉及简单形式的推导。Rushby^[18]揭示了基于圆的描述是怎样和更密切地反映算法的时间触发执行的模型联系起来的。方法按两个步骤进行，并涉及由一组分布在两个层次上的抽象节点表示算法的执行。第一步，基于圆的描述转换成可以系统地完成的非定时同步系统模型^[19]。在此模型中，所有的节点都假定完全同步，并在锁定的步骤中操作。时间概念通过计数节点所采取的步骤进行抽象捕捉。对TTP/C而言，这些步骤大致对应协议调度表所定义的时槽。这个抽象来自于时钟同步机制。第二步包括提炼同步模型为定时同步模型，它可以通过一种独立于任何给定算法的通用的方式来实现。

一个指定分布式算法的标准方式就是状态转换系统。为了描述在分布式系统中一个节点执行的一个给定的算法，人们定义了一组节点开始状态，节点产生的那些信息给出了它的当前内部状态，以及在信息接收端它是如何从一个状态移动到下一个状态的。更形式化的，节点需要提供以下三种功能的解释：

•initstate（p），分配给每一个节点p的初始状态；

•msg（p，s），这是信息生成函数，它表示节点p在状态s发送的信息；

•trans（p，s，m），这是状态转换函数，它描述了节点p在状态s上接收信息m后的新状态。

接着，在t时刻分布式系统中的算法执行的快照由以下组成：所有节点的内部状态集合S_t、节点生成的信息集合M^s_t和节点接收到的信息集合M^r_t。描述这些集合如何随着时间的推移而发展的粒度是系统模型的特点。在不计时的同步模型中，时间以时槽粒度建模，并且算法的执行可以用以下三种函数来描述，其中Slot代表时槽编号，Node表示节点标识符：

•state^ss：Slot×Node→State，其中state^ss（t，p）给出节点p在时隙t开始时的内部状态；

•sent：Slot×Node→Message，其中sent（t，p）表示节点p在时隙t期间发送的信息；

•rcvd：Slot×Node→Message，其中rcvd（t，p）表示节点p在时隙t期间接收的信息。

同步系统模型中的一个节点的行为，可以通过把实体与信息生成函数msg以及状态转换函数trans联系起来捕获，这就构成了分布式算法。然而，算法必须区分一个节点的无故障和有故障行为。对于无故障节点，算法会认为它们在其初始状态开始，然后同步执行以下步骤^[20]：

（1）应用信息生成函数到当前状态，以确定要发送到其他节点的信息。将这个信息放在输出通道中：

（2）应用状态转换函数到当前状态和通过传入通道收到的信息中，以获得新的状态。删除通道中的所有信息。

对于基于TDMA的通信模式，比如在TTP/C中，信息生成函数会产生一些特殊的值，null表示对于所有节点，没有信息在时隙t调度发送节点。

故障节点的行为以及描述发送信息和接收信息的函数（即sent和rcvd）的关系，受分析研究中采用的算法的故障模型支配。例如，如果节点需要考虑任意的或Byzantine式节点故障，那么函数state和sent可以假定分别产生任何状态或信息，而不必服从信息生成函数或状态转换函数。例如，一个节点的故障-沉默行为，可以通过定义sent（t，p）、从时隙t起产生一些null来建模。

由于不定时的同步系统模型是从时序方面抽象而来，所以具体涉及时间的算法比如时钟同步，不在这个层面上表达。因此，人们还需要更详细的描述来建立节点的时序行为的模型。与不计时的同步层面的模型相比，“定时同步模型”额外引入了形式化节点的本地时钟的实体，状态更新和信息生成目前以一个更细粒度的方式在时钟的滴答声的层面上，而不是时槽的层面上描述。

和同步系统模型相比，用来描述时间触发系统的函数的数量增加一倍。除了描述一个节点内部状态的函数state外，函数message被引入用来表示在某一时刻一个节点可用的信息。此函数延伸了从同步系统模型中知道的信息接收的概念。尽管如此，函数rcvd表示在一个时隙期间信息到达节点；然而，在时间触发模型中，不得不考虑到该信息是否按时到达。如果按时到达，信息对应于rcvd，否则会产生空的信息。此外，函数send_time和arr_time分别表示节点发送和接收信息的时刻（实时）。

更形式化地，执行分布式算法的时间触发系统通过以下函数描述：

•state^tt：ClockTime×Node→State，其中当节点p时钟读取时间T时，state^tt（T，p）给出节点p的内部状态；

•message：ClockTime×Node→Message，其中当节点p在其逻辑时钟读取时钟T时message（T，p）给出节点p可以利用的信息；

•sent：Slot×Node→Message，其中sent（sl，p）表示节点p在时槽sl期间发送的信息；(www.daowen.com)

•rcvd：Slot×Node→Message，其中rcvd（sl，p）表示节点p在时槽sl期间接收的信息；

•send_time：Slot×Node→realtime，其中send_time（sl，p）表示节点p在时槽sl发送信息的实时时刻；

•arr_time：Slot×Node→realtime，其中arr_time（sl，p）表示节点p在时槽sl接收信息的实时时刻。

上述实体涉及的两个时间概念必须区分：实时和时钟时间^[16]。实时是一个抽象的概念，在系统中并不可以直接观察，而时钟时间是本地的节点通过其时钟可利用的时间概念。一个节点p的（逻辑）时钟LC_p把实时的时间t和时钟时间T联系起来，因此LC_p（t）表示节点p的时钟在实际时间t的读数。

就像在同步系统模型中一样，上面的实体都需要和实际建立研究中的分布式算法模型的那些内容联系起来。和同步世界不同，实体不仅要形式化一个节点怎么开始，而且要形式化它何时采取步骤。为此，引入函数schedule（sl），为每一个时槽sl产生一个节点启动时槽的时钟时刻。概念上，时槽可以分为节点发送和接收信息的“通信阶段”和一个节点更新自己的内部状态的“计算阶段”^[18]。这些概念用函数cmp_start（sl）来反映，该函数表示一个节点在时槽sl结束其通信阶段并开始其计算阶段时的偏移量。

使用这些函数，一个无故障节点的内部状态可以如下步骤来建模：

•第一时隙的开始时刻，p是在其初始状态：

State^tt[schedule（0），p]＝initstate（p）

•在时槽的通信过程中，一个节点的状态保持不变：

如果schedule（sl）≤T≤schedule（sl）＋cmp_start（sl），

则state^tt（T，p）＝state^tt[schedule（sl），p]。

•在节点的计算阶段，节点p根据其状态转换函数更新它的内部状态，状态转换函数在通信阶段结束时被施加到p的状态，在该时间对节点p可用的信息为：

State^tt[schedule（sl＋1），p]＝trans[p，state^tt（T，p），m]

其中

T＝schedule（sl）＋cmp_start（sl），且m＝message（T，p）。

为了表征message（T，p）的值，需要考虑节点p是否在最后一个通信阶段收到信息；如果是这样，则它对应于rcvd（sl，p），否则该信息为空。

如果schedule（sl）≤arr_time（sl，p）＜schedule（sl）＋cmp_start（sl），

则

message（T，p）＝rcvd（sl，p）。