时间感知系统优化的逐步精化方法-理论计算机科学电子笔记187（2007）91-106

理论计算机科学电子笔记187（2007）91-106www.elsevier.com/locate/entcs时间感知系统优化Tomi Westerlund1芬兰图尔库计算机科学中心芬兰图尔库大学信息技术系Juha Plosila2芬兰图尔库大学信息技术系摘要我们提出了一个正式的，时间意识的系统细化。所提出的时向精化方法是传统作用系统精化演算的直接扩展这种适应为逐步改进用时间刺激的动作系统形式主义建模的系统提供了一个有根据的数学基础在将一个抽象的系统细化为一个更具体的系统时，设计者必须表明，功能和时间属性的条件都得到了满足。关键词：定时动作系统，细化，时间1介绍使用基于仿真的方法对实现相对于初始规范的正确性进行了验证，如果两个模型之间存在不必要的不匹配，则需要新的设计周期。这是耗时的，并且是设计系统的容易出错的方法为了克服繁琐的设计周期，逐步精化的形式化方法是一种很有前途的方法。它们提供了工具，可以将高级系统规范转换为具有严格数学基础的可实现模型。行动系统形式主义[2]，此后称为常规行动系统，是一种可以在整个设计项目中使用的形式化方法。使用精化演算框架确保转换的正确性1电子邮件：tomi. utu.fi2 电子邮件：juha. utu.fi1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.08.04692T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91n图1.通过几个细化步骤的硬件系统开发示例[4]的文件。Conventional Action Systems是Back和Kurki-Suonio [1]提出的一种基于状态的形式化描述语言。 它是基于一个扩展版本的由Dijkstra引入的一种受保护的命令语言[5]。它用于反应式系统的规范和正确性保持开发。 它首先是为软件系统设计量身定制的，但随后也成功地应用于硬件系统设计，包括同步[9]和异步[8]。本研究的范围是扩展精化演算框架，以便能够开发时间香料动作系统，称为时间动作系统[11]。也就是说，我们提出了一种时间感知的精化方法，通过这种方法，可以使用标准的精化演算将抽象系统规范的功能属性转换为更具体的，并保留其时间特性（图1中以图形方式显示了一个示例精化）。我们研究的最终目标是为SoC/NoC（片上系统/片上网络）系统提供一个建模框架，在该框架中，在一种形式主义中，系统可以从规范建模到可实现的模型。发展一个系统的模型S从一个高层次的系统模型S开始，其功能和时间特性在一个规范中给出系统之间的细化关系模型的定义是为了保持总的正确性：如果S ± SJ和pSq，那么pSJq也成立。经过几个连续的细化步骤：S ± SJ±···±Sn，我们得到一个可实现的规范。通过传递性，我们有S ±Sn和pSnq[4]。因此，我们以逐步的方式开发了原始规范的实现。基于精化的开发方法是为几种不同的专用语言引入的，其中一些语言在经过几个精化步骤后不能保证具体模型的正确性，而另一些语言则允许逐步开发方法，即一系列精化。我们将简要讨论属于后一组的三种不同的细化方法。在[13]中介绍了一种将高级Timed MSC模型细化为设计规范的方法他们的细化方法类似于我们的跟踪细化，因为环境不应该然而，在我们的方法中，我们不考虑时间约束的细化，因为在我们的目标环境中，VLSI系统，系统约束由规范给出，因此不允许放松。然而，允许对时间限制进行细化，以满足新的、细化的定时动作系统。在[7]中提出了实时并发系统的动作的改进他们采取了一种方法，EA′一个2的1EAnBCDDCBAnE一A′T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）9193诉讼的持续时间与原诉讼的持续时间相同，而我们没有对诉讼作出任何特定的限制，因为这些限制确保了时间行为，此外，我们还试图尽量减少与时间有关的额外举证责任。另一个实时精化演算在[6]用于逐步开发独立于机器的实时程序。本研究的范围是软件开发。据我们所知，他们的方法不适用于SoC/NoC系统设计，这是我们的研究兴趣，也不可能用他们的方法进行静态时序分析2定时动作系统在这一节中，我们简要概述了构成我们的时间形式主义的正式基础的常规行动，之后我们继续对时间行动系统进行相当详细的回顾2.1常规行动一个动作A被定义为（例如）：A：：=abort（堕胎、不终止妊娠）| skip（空语句）| {p}（assert语句）| [p]（假设陈述）| x：= xJ.R（非确定性分配）| x：= e（（多重）分配）| p→ A（守护行动）| A1A2（非确定性选择）|A1; A2（顺序组成）| 做一件 好事（迭代合成）|[ var x：= x 0 ; A ]|（带有局部变量的块）|(block with local variables)其中A和Ai，i= 1， 2，是动作;x是变量或变量列表;x是变量x的某些值;e是表达式或表达式列表;p和R是谓词（布尔条件）。 在动作A中分配的变量称为A的写变量，用wA表示。其他变量在动作A中，被称为A的读变量，用rA表示。写变量和读变量共同构成了A的等式vA：vA=^wArA。2.1.1动作语义一个动作A关于一个前提P和一个后条件P的完全正确性条件Q表示dPAQ，并由d定义：PAQ=^Pwp（A，Q），其中wp（A，Q）表示动作A建立后置条件Q的最弱前置条件。例如，我们定义：wp（abort，Q）=false，wp（skip，Q）=Q，wp（（A0A1），Q）=wp（A0，Q）<$wp（A1，Q），wp（{P}，Q）=P<$Q，wp（[P]，Q）=P<$Q，wp（（A0;A1），Q）=wp（A0，wp（A1，Q）），wp（P→A，Q）=P<$wp（A，Q）并且wp（doAod，Q）=（<$k.k≥0<$H（k）），其中H（0）=Q<$<$gA，k= 0并且H（k）=（gA<$wp（A，H（k−1）<$H（0），k >0。也就是说，动作的迭代合成的最弱前提条件要求在A的k次重复之后，终止，也就是说，在后置条件Q成立的状态下，A如果k= 0，则A被禁用，并且迭代的行为与跳过动作相同。94T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91^^^上面的布尔条件gA是动作A的保护，定义为：gA=<$wp（A，wf alse）。也就是说，gA在状态中为真，在状态中A没有奇迹般的行为。在一个被保护动作A=p→B的情况下，我们有gA=p<$gB。一个动作A被称为在它的保护为真的状态下被启用。否则A为禁用.如果wp（A，false）=false（即，保护gA不变地为真：gA=true），则称动作A总是被启用。 此外，如果wp（A，true）=true成立，则称动作A总是终止的。动作A的主体sA由dy定义：sA=^AgA→abort。2.1.2符号一个行动的量化合成被定义为：[·1≤i≤n：A i]，它被定义为：A1·... ·An，其中项目符号·表示任何复合运算符，n是动作的数量此外，动作Ai内的替换操作，由A[eJ/e]表示，其中e指代诸如原始动作Ai的变量和谓词的元素，并且eJ表示新的元素，其替换Ai中的e。同样的符号也适用于动作系统。优先级（prioritised，“优先”）组合[ 10 ]是一种组合，其中启用的动作的执行顺序是优先级的。我们有：AB= Ag A→B，其中最高优先级属于组合中最左边的动作;因此，总是选择最左边的启用动作来执行。例2.1作为常规操作的一个例子，让我们有两个变量x和y相乘，结果被写入变量prod。执行所述功能的常规动作定义为：M：prod：=其中M是为动作给出的标签。2.2定时动作系统让我们开始介绍定时动作系统，首先展示它的形式，然后介绍它的元素和计算模型。定时动作系统A具有以下形式：sysA （g;）：：|[ 约束条件Cj：（B）;延迟dA i;var l;行为 Ai<$dAi）：（aAi）;initg，l：g0，l0;exec做定时动作A的合成[iod]|在上面的系统中，我们可以识别三个主要部分：接口，声明和迭代。接口部分声明了那些在动作系统边界之外可见的变量g如果一个定时动作系统没有任何接口变量，它是一个封闭的动作系统，否则它是一个开放的动作系统。在声明部分，引入了所有局部变量l，对局部和全局变量执行操作的动作定义，其中aAi是由前面给出的语法生成的任何类型的定义的原子动作，Ai是其标签，dAi是确定其延迟的谓词谓词被连接到延迟括号（）之间的定时动作。此外，定义其严格遵守是强制性的条件的约束Cj是T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）9195dmind′DMax时间一A.stA.ftΔ（A）=A.ft−A.st图2.非确定性延迟谓词dAnd的说明。在声明部分介绍。最后，在迭代部分之前，定时动作系统的do-od循环是全局和局部变量的初始化。do-od循环定义了系统的反应行为。它描述了在声明部分中定义的动作的组成，也就是说，它定义了系统的反应行为和功能。我们选择时间域是稠密和连续的T=R≥0，因为它一个连续时间系统运行的自然模型。 时间的推移通过推迟写入变量的更新来建模。计算开始的时间在初始化中设置，但它并不重要，因为只有定时动作的相对顺序才重要。接下来，让我们介绍延迟谓词，然后详细介绍定时动作及其形式2.2.1延迟模型如上所述，定时动作的延迟，比如A，由位于声明部分中的延迟子句中给出的预测dA确定。 在本节中，我们将介绍两个最常用的延迟谓词：确定性dAn 和非确定性dAn 和延迟谓词。对于这两个谓词，我们分别使用以下缩写A<$d）和A<$dmin，dmax）它们的定义如下：dAd=^dJ=d（确定性）dAnd=^dmin≤dJ≤dmax（n（bounded，non-deterministic））其中dJ是T类型的变量，d、dmin和dmax是T类型的数值。在前一个谓词中，延迟dJ获得值d。在后一个谓词中，值是在给定区间之间非确定性地选择的，见图2。也就是说，延迟的确切值事先并不知道。它是在评估组件时给出的。2.3定时动作传统动作系统的计算不需要时间，反应是瞬间的，因此在任何可能的意义上都是原子的。原子性意味着只有操作的前状态和后状态是可观察的，并且当它们被选择执行时，它们不能被外部对应物中断。这是由于其软件定制的背景。在对SoC/NoC系统建模时，知道动作所消耗的时间是很重要的，因为操作速度是由这些动作的延迟因此，在时间动作系统中，我们认为每个计算都需要时间。这种方法也是由动作的原子性以及在每次执行之后可以观察到系统状态的事实所证明的。96T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91^^行动应该注意的是，定时动作的复杂度不受限制，因此操作时间也不受限制定时动作A<$dA）定义为：A<$dA）=^（Af<$Ak）<$As<$Pt（时间）（1）其中我们可以识别由优先级划分的三个操作段：开始、结束和时间。开始段包含开始动作As，其执行启动定时动作的操作， 以及操作 终止于由终结动作Af和终结动作Ak组成的结束段。将被执行的一个依赖于定时动作的启用。也就是说，如果一个定时动作被其他定时动作禁用，当它被认为是一个预定的定时动作时，kill动作会释放它以供将来计算。它可以防止定时操作死锁。通过执行时间传播动作Pt，在执行开始动作之后的时间段中使时间提前。一个定时动作，其操作已执行，但其写变量尚未更新，称为计划定时动作。 的时间段 定时动作被认为是由谓词dA确定的调度动作。2.3.1定时动作详情接下来我们将详细介绍定时动作组件。此后，将介绍定时动作和时间传播动作的组成。定时动作组件的定义如下：As=<$bAgA→stateA：=（wA，gt，gt+dJ.dA）;A[stateA.wA/wA];bA：=T;（定时动作（开始））（二）Af=bAgA（gt=stateA.ft）→bA：=F;wA：=stateA.wA;（timed action（finish））（3）Ak=^bAgA→bA：=F;（ timedaction （ kill ） ）（四）其中布尔变量bA将操作序列化为操作和写入部分;gA是定时动作的保护;stateA存储动作的新状态它的类型是：typestate：record（wA;st，ft：T），其中wA是A的写变量，st是开始时间，ft是结束时间。开始时间设置为全局时间gt，结束时间通过将延迟值添加到全局时间来获得观察stateA.ft实际上存储写入变量被调度为由Aw更新的时间，假设它在延迟期间保持启用，即，在所提到的时间段内禁用删除动作Ak定时动作Ai的组成为：定时动作的合成Ai=^（定时动作组成）[1≤i≤n：（Af，i<$Ak，i）]（完成预定定时动作的操作）T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）9197^[进度时间其中n是动作的数量观察到时间传播动作Pt在定时动作之间共享。它将全局时间设置为最接近的计划完成时间。其定义如下：P t=^[n1≤i≤n：min[i]→gt：=stat eAi. 时间过程其中，保护min[i]被给出为：min[i]=（stateAi.f t> gt）（保护min）（ft>gt恒速器eAi. ft≤stat eAj。（ft）它探讨了预定定时动作的finish timesstateAi.f t的值。如果定时动作Ai的完成时间状态Ai. ft大于gt（定时动作是预定定时动作的要求）并且没有其他预定定时动作的完成时间状态A j . ft小于它，则它评估为真换句话说，它选择最小的预定完成时间大于全局时间gt，然后成为Pt中的新全局时间。2.3.2定时动作的最弱前提条件最弱的前提条件定义了一个动作相对于其前置条件和后置条件的完全正确性定时动作的最弱前提条件根据其在执行期间的启用情况分为两部分：（a）定时动作在其整个操作期间启用，允许在指定延迟之后更新写入变量，以及（b）定时动作在执行期间被禁用，防止写入变量的更新并启用定时动作以供进一步执行。也就是说，它的行为与skip动作相同。因此，定时动作的最弱前提条件是：wp （ （ A<$dA ） ） ，Q ） = wp （ A ， Q [ （ gt + dJ.dA ） /gt] ） <$ （ <$gA<$Q ）（wpof a timed action）其中后一部分是跳过动作的最弱前提条件：wp（skip，Q）。2.4系统行为建模假设我们有两个时间动作系统A和E，它们的局部变量和动作是不同的，后者是前者的环境。考虑这些系统的并行组合，用AE表示。并行组合被定义为另一个动作系统，其不同的全局和局部标识符（变量和动作）由组件系统的标识符组成，其执行子句具有以下公式：do[1≤i≤n：Ai][1≤j≤m：Ej]od，其中Ai和Ej分别是系统A和Ej这些行为是不允许的有相同的标签。组成系统通过它们共享的接口变量进行通信.平行合成的定义在系统中反向使用。98T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91i=1我图3.一个具有确认状态的定时动作系统的计算模型。一种派生，将系统描述分解为更小的独立系统或内部子系统的组合。在对系统A及其环境E的行为进行建模时，假设总是有一个启用的定时动作。换句W〇rds，S_SgA）（mi=1gE）。计算模型（图3）。定时动作系统的计算是通过将其变量（局部和全局）初始化为预定值开始的。在迭代部分（exec部分）中，基于开始动作As，i的组成和启用顺序地选择要执行的动作。在执行所有启用的开始动作之后，在时间传播动作Pt中，全局时间gt被设置为最接近的预定完成时间。然后，执行那些延迟被消耗的预定定时动作中的finishA f，i或kill A k，i动作。这只要存在启用的（1）或计划的（2）定时动作，就会重复。然而，如果没有这样的定时动作，则定时动作系统被认为是临时延迟的。当环境通过接口变量启用操作时，计算恢复执行。开始状态和结束状态周围的虚线框表示第1.1节中讨论的设计约束的验证。3.2.例2.2在例2.1中，我们引入了一个动作M。 让我们把这个动作放入下面的定时动作系统Mult中。系统Mult在更新输入变量并启用和禁用使用布尔变量en进行计算，最后读取计算结果。我们拥有：sysMult（x，y，prod：data;en：bool;）：：|[actionsM <$d min，d max）：（en → prod：= xy）;initen，x，y，prod：=F， 0， 0， 0;[执行模块 ]|验证进度时间（Af，i<$Ak，i）<$As，i<$Pt完成定时动作的操作（Af，i<$Ak，i）<$As，i<$Pt[错误]验证[true]开始歌剧-定时动作（二）[true]（一）ki=1gAiKi=1 gas，i[错误]（Af，i<$Ak，i）<$As，i<$Pt等待环境暂时的延迟在操作T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）9199^I=k其中，非确定性延迟定义了乘法的最小dmin和最大dmax运算时间。在本例中，所选延迟类型用于表示数据相关延迟，即其值取决于操作数的值的延迟。不知道例如乘法算法或生产技术的延迟值是保守的延迟值。然而，在本文中，我们不放大的算法，也没有生产技术。3时间性为了证明迹细化的正确性（在下一节中介绍），我们引入了计算定时动作合成的延迟的规则，此外，还引入了约束，利用这些约束，不仅在逻辑上而且在时间上都可以限制定时动作的操作。3.1延迟定时动作及其组合的延迟计算规则定义如下：Δ（A）=dJ.dA=A.f t−A.st（动作延迟）（5）Δ（A;A）= Δ（A）+ Δ（A）（顺序延迟）（6）1 2 ^1 2Δ（p→A）=Δ（[p];A）=Δ（[p]）+Δ（A）（差分）（7）Δ（A1ΔA2）=^{Δ（A1），Δ（A2）}（交替地）（8）Δ（A1ΔA2）=^{Δ（A1），Δ（A2）}（交替地）（9）（|[varx：=x0;A]|）=Δ（A）（b lockdelay）（10）Δ（doAod）=^0Δ（A）（它是相对的）（11）其中（5）定义了定时动作延迟。延迟也是使用定时动作的开始和结束时间来定义的;（6）对顺序执行的定时动作的延迟进行求和;（7）定义受保护的定时动作的延迟它由两个部分组成，基于保护动作的定义：保护的评估和操作时间;（8）和（9）给出了一组延迟，每个延迟都反映了另一个延迟路径。为了提取最佳或最差情况的传播延迟，可以分别使用Min或Max函数在关键时序路径分析中，可以利用Max函数来观察从输入到输出的最慢路径;（10）定义了一个定时动作块的延迟;最后，在（11）中定义了迭代合成的延迟它等于在k次迭代中执行的那些定时动作的延迟之和。这个定义是由前面给出的迭代合成的最弱前提所证明的。它指出，在k次选择后，do-od循环将正确终止。使用上述延迟计算规则，我们能够定义设计中系统的静态延迟。 在静态延迟分析中，无需仿真就可以计算出系统的期望定时信息。静态延迟分析返回一组延迟，每个延迟对应一个可能的计算路径，即两个定时动作之间不允许循环的路径。从所获得的集合，100T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91^时间TDF(a) 时间关系以开始。(b) 一个定时动作A满足（T）和不满足（F）一个截止日期。图4. 以时间关系和截止日期开始的图形表示例如，可以计算系统的最坏情况延迟，函数或使用Min函数的最佳情况延迟3.2约束约束是一个表达式，根据它所涉及的定时动作必须操作。因此，违反约束，布尔条件，表示无用的，不可预测的计算。如上所述，约束是布尔条件，例如，关于定时动作的相对或可测量属性。相对约束从时间的角度定义了定时动作如何相互作用，例如，相对约束以（图4（a））开始，要求定时动作的开始时间相等：A1满足A2= A1.st= A2.st。 在文本中，我们使用符号“”来表示约束。对于给定的例子，我们有：{A1满足A2}。另一方面，可测量约束检查定时动作的操作时间，例如，可测量约束期限[12]定义了一个时间点，在这个时间点上，所涉及的定时动作的操作必须完成它们的操作。例如，定时动作A的最后期限是：Δ {Δ（A）≤D}。图4（b）表示正确执行（A. ft=d1）和F.中的阴影区域图4（b）表示定时动作A的假计算区域，也就是说，在该区域中，我们具有d2> D。我们使用符号Q来表示最后期限约束。对于给定的例子，我们有：Q{A，D}。约束的可接受性在所示的任一虚线框中确认在图3中，取决于经验证的属性。约束在约束子句中的定时动作系统的声明部分中引入。 约束是根据验证点中的观测点进行验证的。例如，约束的观察点是第一个引用的定时动作发生时的时间点。在约束中开始或结束其操作。对于上面定义的截止日期，观察点是开始时间A.st。 另一方面，由约束中最后引用的定时动作定义。对于截止日期，验证点为A.f t。为了给一个约束一个特殊的状态，它可以被定义为一个断言语句。在这种情况下，如果它保持（Btrue），则它的行为就像一个skip语句，否则它的行为就像abort（Bfalse）。换句话说，如果满足约束条件，作为空语句操作，根本不改变状态。另一方面，如果一个约束没有被满足，它是一个永不终止的语句，因此不会建立任何导致系统异常终止的后置条件。的1时间A2Q（A，D）d1d2一T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）911014细化传统的行动系统是在精化演算框架内以逐步的方式设计的[4]。 精化演算在精化过程中保持动作的正确性。 在本节中，我们将集中讨论如何将有理有据的精化演算框架应用于定时动作。如前一节所述，计时符号是非计时模型的一个明显扩展。因此，我们采用传统作用量的精化演算，并将其推广到时域。一个（原子）动作A被称为被动作C（正确地）精化，记为A≤C，如果下列性质成立：你好。（wp（A，Q） wp（C，Q））（约定动作的细化条件）这相当于条件马格德堡，Q. （（P A Q）<$（P C Q））（全正确性）这意味着具体动作C保持抽象动作A的所有完全正确性。4.1常规操作的数据细化在数据精化中，变量a和u上的抽象动作A通过变量c和u上的具体动作C使用抽象不变量R（a，c，u）来精化，抽象不变量R（a，c，u）是抽象变量a和具体变量c之间的布尔关系。如果以下条件成立，则动作A由动作C进行数据细化，表示为A≤RC你好。（Rwp（A，Q） wp（C，Ra.RQ））（数据细化条件）保持。谓词a.RQ是程序变量a和c上的布尔条件。上述数据细化的定义可以根据动作A和C的守卫gA、gC和主体sA、sC写成如下：RgCgA（body）（ii）你好。（RgCwp（sA，Q）wp（sC，a.RQ））（guard）（iii）数据细化A≤RC用c替换a，保持变量u。 当然，如果我们不替换任何变量和延迟，而只是添加一些新的变量和延迟，我们有R为真，因此R可以从精化证明中省略上述数据细化规则也将用于下一节中的定时动作，其中介绍了定时动作系统的跟踪细化我们将不为定时动作引入数据细化规则，因为由于第2.4节中提出的所选建模方法，102T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91在时间感知细化中必须考虑的，在系统规范中给出，因此被认为是系统属性。简而言之，我们将一个定时动作系统的约束，比如A，表示为： n，其中Ci，1≤i≤n，是时间作用系统A的约束。4.2微量细化在某些环境中精化一个开放动作系统的想法是保留所讨论的系统的轨迹或全局状态序列（可观察行为）。因此，这种转换通常被称为系统的跟踪细化。迹理论的基本研究可以在[3]中找到。这里我们不去深入研究迹线细化理论的细节，而是应用一种常用的方法，通过数据细化来证明两个系统之间的迹线细化我们将讨论那些与传统表述相一致的观点，并认为它们也适用于定时动作考虑定时动作系统A和C：sysA （g;）：：|{A};延迟dA;vara;actionsA <$dA）：（aA）;initg，a：= g 0，a 0;execdo A od]|sysC（ g;）：：|[约束 条件{C};延迟dC，dX;var c;actionsC<$dC）：（aC）;X<$dX）：（aX）;初始化g，c：=g 0，c 0;execdo CX od]|其中aA，aC和aX是前面定义的任何原子动作，并且定义了对系统的约束。设R（a，c）是局部变量a和c之间的关系，I（c，u）是系统C的不变量.抽象的定时动作系统A被具体的定时动作系统C（迹）所定义，记为A±C，如果存在关系R（a，c）使得：R（a0，c0）<$I（a0，c0）=true（初始化）（i）A≤R，IC（主作用）（ii）skip≤R，IX（辅助动作）（iii）RIgAgCgX（连续条件）（iv）RIwp（doXod，true）（内部收敛）（v）R{C}{A}（定时行为）（vi）第一个条件（i）说系统A和C的初始化建立了抽象关系R。 第二个条件（ii）要求抽象动作A被具体行动C使用R进行数据精化。 第三个条件（iii）又表示辅助动作X是通过对跳跃进行行动上这基本上意味着X的行为就像关于全局变量u的跳过动作，这些全局变量u在精化中不允许被改变。 的T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91103第四个条件（iv）要求，只要抽象系统A的动作A被使能，假设抽象关系R成立，则在具体系统C中也必须有使能的动作。第五个条件（v）指出，如果R成立，则单独执行的辅助动作X必须在某个时刻终止点最后，第六个条件，唯一的定时相关条件，要求在具体的定时动作系统C中满足所有的时间约束。也就是说，具体系统的功能行为和时间行为都必须遵守在执行细化步骤之后的给定约束，否则细化系统的时间特性不能得到保证。在上面介绍的定时动作系统的跟踪细化中，我们采用了来自常规动作系统的跟踪细化的第一个条件（i）-（v这种方法的合理性在于，定时动作系统通过定义延迟来扩展传统动作系统，该延迟确定结果被写入写变量的时间常规动作的操作部分、功能性不被改变。在对定时诉讼制度进行追踪改进时，一个重要的问题是，我们采取了一种尽可能简化举证责任的方法。也就是说，我们不对如何细化定时动作的延迟提出任何直接要求。然而，我们可以观察到，在最后一个条件下，时序得到了确认，在这个条件下，从系统规范中获得的时间要求的可接受性得到了确认。换句话说，从时间的角度来看，通过显示所有的时间义务都得到了具体的满足，确保了系统C。如前所述，定时动作的功能是使用常规动作的数据细化来细化的接下来，我们展示了定时动作的数据细化的正确性。我们需要证明：A≤RC <$A<$dA）≤RC <$dC）保持。在证明中，我们假设定时动作在其操作期间未被禁用，换句话说，定时动作在其操作时间内保持启用。这就是说，我们可以使用下面的时间延迟模 型AdA=^Ao;Tim e;Aw ， 其 中 A o=^Ao ， 1;Ao ， 2 ， 其 中 A o ， 1=^SA ： = （ wA ， gt ，gt+dJ.dA），并且Ao，2=^A[SA. wA/wA];时间=^gt：=SA。ftanddAw=^wA：=SA. 我们使用子大量的鸟类变异stateA=SA和stateC=SC来阐明表示。假设A≤RC。然后又道：wp（AdA，Q）优惠{定时动作模型AdA}wp（Ao;时间;Aw，Q）惠{Ao的定义}wp（Ao，1;Ao，2;时间;Aw，Q）惠{Ao，1，Ao，2，TimeandAw的定义}104T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91^minminmin^wp（SA：=（wA，gt，gt+dJ.dA）;A[SA.wA/wA];gt：=SA.ft;wA：=SA.wA，Q）{“wp（SC：=（wC，gt，gt+dJ.dC）;C[SC.wC/wC];gt：=SC.ft;wC：=SC.wC，Q）优惠{Co，1，Co，2，TimeandCw的定义}wp（Co;Tim e[SC. ft/SA. ft];Cw，Q）优惠{定时动作模型CdC=Co;T ime;Cw}wp（CdC，Q）例4.1考虑下面在例2.2中给出的定时动作系统Mult。让我们假设一个设计者，在充分考虑的基础上，选择了最好的乘法算法，以满足给定的时间要求。在规格。设计者不愿意降低抽象层次在设计周期的这一点上，因此设计者仅在系统的跟踪细化中改变定时信息。 我们要做一个完善的。M<$dmin，dmax）≤M<$dJ，dJMax在证明该细化步骤的正确性时，我们仅需要验证第一个和最后一个细化要求。(i) 初始化。 动作系统Mult的初始化与动作系统MultJ的初始化并不矛盾。(ii) 定时行为。 定时操作M是D：Q{M，D}。我们要求dJ，dJMax∈[d min，d max]. 因此，约束是满足的，因为根据要求，它在抽象的定时动作系统Mult中不成立。因此，我们执行了跟踪细化Mult± MultJ。例4.2考虑上例中给出的定时动作系统MultJ设计者通过引入新的中间变量t和布尔变量b将定时动作M分解为两个单独的定时动作，新的定时动作的操作顺序在改进之后，我们有一个定时动作系统MultJJ，其运算如下：doM1<$M2od，其中两个定时动作M1和M2如下：M1<$d1，d1Max）=^<$b→u：=w;t：=xy;b：=T;且M2<$d2）=b→prod，b：=t，F;.为了证明这种细化的正确性，我们需要证明定时跟踪细化的所有条件都得到了满足。我们拥有：(i) 初始化。 动作系统MultJ J的初始化与动作系统MultJ的初始化不矛盾。(ii) 主要行动。我们的目标是证明M≤IM2，其中I是f orm的不变量：I=^bt=p rod. 我们有：守卫：IgM2gM惠我b真惠真）的。T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91105^Max正文：IgM2wp（sA，Q） wp（sM2，IQ）惠{sM和sM2的最弱前提条件}IbQI[F/b]Q[t/prod]惠{不变量I=bt=prod}（bt=prod）bQ（bt=prod）[F/b]Q[u/w]优惠{logic}（bt=prod）bQTQ[t/prod]优惠{logic}bt= prod QQ[t/prod]b优惠b QQ惠真因此，我们证明了M≤IM2成立。(iii) 辅助动作。 因为辅助操作M1不修改任何接口变量，所以它的行为类似于跳过这类变量：(iv) 延续条件。 总是存在新的定时动作M1或当原始定时动作A被启用时，M2(v) 内部趋同。保持平凡的新辅助行动M1禁用本身.(vi) 定时行为。定时动作M的最大允许操作时间是D：Q{M，D}。虽然我们将动作分解为两部分，但截止日期的范围保持不变，即观察点是M1开始操作的时间点，验证点是M2完成操作的时间点。在计算合成的延迟时，我们使用延迟计算规则（6），尽管合成建议规则（8）。这是由细化的定时动作的相互作用所证明的M1使M 2成为可能。 通过要求d1+d2≤d，满足了最后期限。因此，我们执行了迹线细化MJ±MJ。保持约束最新，它们被更改以满足新的动作定义。在我们的示例中，由于前一个定时动作使后者成为可能，因此截止日期变为Q{（M1;M2），D}。我们不认为这是一种细化，因为约束本身没有改变，也就是说，约束的范围与前面指出的相同。5结论在本文中，我们介绍了一种方法来开发，以逐步的方式，一个抽象的系统向一个更具体的。定义细化规则的一个优点是，它是对传统诉讼系统现有细化规则的明确扩展我们用一个简单的例子展示了一个定时动作系统是如何逐步细化成一种形式的，106T. Westerlund，J.Plosila/Electronic Notes in Theoretical Computer Science 187（2007）91由一个新的辅助布尔变量排序在本文中，我们没有考虑我们的时间形式主义的可扩展性，因为范围是在时域中的原子结构的分解。然而，引入的时间细化规则是朝着这个方向迈出的重要一步，因为我们现在能够从抽象的规范开始开发系统，并以逐步的方式将其细化为更具体的规范，同时保留时间和功能特性。引用[1] R.- J. 巴克和R.库尔基-苏尼奥过程网络的分散化与集中控制。 在Procs. 第二届ACM SIGACT-SIGOPS Symp.分布式计算原理，131-142页，1983年。[2] R.- J. 贝克街和K街。塞尔从模块化系统到动作系统。 在proc 正式方法欧洲'94，西班牙，1994年10月。计算机科学讲义，史普林格出版社[3] R.- J. Back和J. von Wright。动作系统的跟踪细化。并发理论国际会议，第367-384页，1994年[4] R.- J. 回到J。冯·赖特。精化演算：系统介绍。Springer-Verlag，1998.[5] E. W.迪杰斯特拉程序设计的一门学科。普伦蒂斯-霍尔国际，1976年。[6] I. J·海耶斯实时精化演算：机器独立实时编程的基础。在ICATPN史普林格出版社[7] M. E. Majster-Cederbaum，J.Wu和H.岳具有因果模糊性的实时并发系统的动作精化Acta Inf. ，42（6-7）：389[8] J. Plosila. 自定时电路设计-动作系统方法。图尔库大学博士论文，1999年。[9] T.塞切莱亚努同步数字电路的系统设计。博士论文，图尔库计算机科学中心，2001年。[10] E. Sekerinski和K.塞尔一种优先构图的理论计算机杂志，39（8）：701英国计算机协会。北京：清华大学出版社.[11] T. Westerlund和J. Plosila.硬件组件的形式时序模型。第22届NORCHIP会议记录，第293-296页，挪威，2004年11月[12] T. Westerlund和J. Plosila.将时序信息反向注释到正式硬件模型中：案例研究。在信号，电路和系统国际研讨会- ISSCS 2005，页面出现，罗马尼亚，2005年7月。[13] T. Zheng，F. Khendek和B.帕罗精炼定时MSC。在SDL论坛，计算机科学讲义第2708卷，第234-250页。Springer，2003年。