加速安全实时模型检查技术研究

202《理论计算机科学电子札记》65卷第6期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 65. html16页s停车可以让你更快地到达那里模型增强以加速实时模型检查2M. OliverMüoller1金砖国家，奥胡斯大学，540DK-8000ArhusC， Denmark3摘要我们提出了一种近似技术，可以使安全性和通用路径属性的实时模型检查当循环导致重复的控制情况时，这是有益的。基本上，我们用精心选择的额外转换来增强时间自动机模型。这增加了状态空间的大小，但潜在地减少了要探索的符号状态的数量。我们给出了一个时间自动机形式主义的正式定义，丰富了基本的数据类型，握手同步，紧迫性和承诺的位置。我们证明了通过跟踪语义，如果一个安全属性可以建立在增强模型，它也适用于原模型。我们将我们的技术扩展到一组更丰富的属性，可以通过一组轨迹（通用路径属性）来决定。为了使通用路径属性延续到原始模型，时间自动机形式主义的语义相对于所应用的增强被制定。我们的技术是特别有用的系统中，调度程序规定repetition- tion的控制在过去的时间。作为一个典型的例子，我们提到的LEGORCXTM程序的翻译U PPAAL模型，其中的循环调度程序是一个静态的实体。我们允许调度程序和相关的任务我们将我们的技术应用于砖分拣机模型的安全属性和报告运行时数据。1电子邮件地址：omoeller@brics.dk2 本文的更详细版本可作为作者论文的一部分http://www.brics. dk/~omoelller/papers. HTML.3计算机科学基础研究，由丹麦国家研究基金会资助-是的。·2002年由ElsevierSc ie nceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。摩尔203||1介绍安全关键系统的故障对人类生命具有高度危险，最低的难以置信的昂贵。一旦第一批10万件产品出货，大规模产品的错误就很难纠正。这就需要验证系统的正确性，或者更好地：确定给定的设计或实现符合其规范。形式方法可以被看作是实现这一目标的系统技术的集合与模拟或测试相反，形式验证相当于证明，系统的形式模型满足通过时序逻辑表达的在模型检查方法中（例如[6]），系统被视为解释公式并可能满足公式的结构（简而言之：Sys=θ）。然后，通过专门的模型检查算法完全自动地执行建立或反驳Sys=Sys通常，离散控制图用于表示系统的状态，而状态之间的转换反映了随时间的演变。在混合模型[3]中，这种演变需要根据数学描述（通常是微分方程）连续改变变量。即使对于低自由度的模型检查问题，然后是不可判定的。实时模型可以被视为混合模型的特殊版本，其中连续部分是时钟，其值根据恒定斜率随时间增加。 只要所有时钟都以相同的速度运行（斜率为1），模型检查问题仍然是可判定的[2]。一个流行的和研究良好的形式主义是时间自动机[4]。固定形式主义的一般可判定性结果-无论是在模型语言还是逻辑中-都是由一些模型检查工具遵循的，例如混合模型的HyTech [9]，或实时模型的Kronos [13]和U PPAAL[11]。 既然国家基本模型的空间从根本上是不可数的，工具有诉诸象征性的技巧在这里，连续部分由有限商捕获。对于实时系统，时间计算树逻辑（TCTL，见[2]）特别令人感兴趣，因为它可以表达大量自然发生的特定属性，如安全性和时间响应。特别是定时可达性是深入研究的主题，因为它足够强大，可以捕获许多例行检查，并且可以比一般TCTL更有效地验证。实时系统模型检测技术起源于一种称为状态爆炸问题的现象。在密集实时中，这被理解为符号状态的数量过多。4开发了许多优化技术，4在密集时间中，在任何两个后续时钟之间存在中间时钟评估时钟评估，因此状态空间是有限的。 然而，对于某些句法限制摩尔204||旨在扩大算法处理的范围。此类优化的示例是尽可能减少时钟数量[8]或减少内存消耗[12]。工业规模的例子仍然是一个严峻的挑战，因为扩展它们的状态空间通常会超过机器的内存或用户的耐心。一个有前途的方法是将模型检验问题Sys=θ转化为一个更简单的问题Sysθ=0，这是保守的，因为有效性后者意味着前者的有效性。我们通过向模型中添加精心选择的部件来构建系统这增加了可达状态空间的大小，但可以减少必须探索的符号状态的数量。这个（看似）悖论可以最好地解释为在控制结构中包含小循环的定时系统。如果相同的控制情况重复发生，则（可能有许多）对应的符号状态可能是不可比较的，因为时间已经延迟了。现在，如果通过一个具有大延迟的附加步骤来旁路具有小延迟的大量环路，则这会产生大量时钟评估。如果较小的集合包含在这个（添加的）较大的集合中，则相应的步骤从要探索的符号状态列表中消失我们使用UPPAAL[11]的模型检查引擎进行实验，因此，保持UPPAAL时间自动机模型的描述，我们的技术。然而，我们的技术是通用的，足以应用其他的时间自动机方言。作为一类可能从我们的技术中受益的问题，我们提到了在LEGO RCXTM微控制器中运行的控制程序的UPPAAL 存在自动转换-LEGORCXTM程序到UPPAAL模型的应用[10];我们的技术可以直接使用该程序作为在哪里应用增强的提示。计划本文的结构如下。第二节介绍了UPPAAL时间自动机模型的形式化语法和语义。第3节定义了我们的模型增强技术，并证明了它的安全性。在第四节我们将我们的方法推广到了泛路性质。在第5节中，我们将模型增强应用于砖块分拣机。最后，我们做一个总结。2乌帕尔时间自动机我们给出了U ppaal [11，5]中使用的时间自动机模型的形式语法。基本上，这意味着网络的时间自动机与离散数据和握手同步.形式语义通过将模型与迹集相关联来定义。UPPAAL是一种用于实时系统建模、仿真和验证的工具，由奥尔堡大学的BRICS和乌普萨拉大学的计算机系统典型应用领域可以统一处理的时钟评估集的数量总是有限的[2]。摩尔205联系我们联系我们包括实时控制器和通信协议，特别是那些定时方面很关键的协议。更多信息和文档可以在主页上找到。52.1UPPAAL时间自动机的形式表示我们将UPPAAL模型的形式语法定义为以下内容的并行组合：过程，在每个过程中，控制位置通过转换连接并配有各种标签。作为预备，我们假设变量（Vars）、时钟（Cl）和同步信道（Ch）的不相交集合。变量表示整数或整数的绑定数组.表达式是在变量、时钟和整数常量上构造的。 表达式的形式为v：=expr，分配或时钟重置。在第一种情况下，v是一个整数变量（或数组中的一个位置），expr是一个关于变量和常量的算术表达式。 在第二种情况下，v是一个时钟，expr需要为常数0。 守卫是变量和时钟约束的布尔表达式的合取，形式为x const或x-y const，其中x，y是时钟，{，<=，==，>=，>}，const是一个整数常量。不变量的形式为xconst，其中x，y是时钟，<，<=，const是整数常量。 同步的形式是s！ 还是s？其中s是同步信道。我们将同步理解为握手，即，一个过渡配备了s！和一个配备了S？ 可以同时服用。为了简单起见，我们假设一组标签-标签-其范围包括语法上正确的不变量、赋值、保护和同步。作为格式良好的条件，所描述的语法的标签被约束为仅出现在适当的位置，仅包含声明的变量，时钟和同步通道，并且以语法正确的方式使用数组。可以选择将位置声明为紧急或已提交。在这两种情况下，必须在时间流逝之前离开该位置。离开已提交的位置优先于进行其他转换。如果同步通道被声明为紧急，则在这些通道上同步的转换优先于时间延迟。Def. 1（乌帕尔法）一个UPPAAL进程A是一个元组L，T，Type，l0，其中• L是一组位置，g，s，a• T是一组跃迁 l−−→lJ，其中l，lJ∈L， g是保护， s是同步标签（可选），a是分配列表（可能空）;我们称L为转换的源，而LJ为转换的目标• 类型：Lo，u，c是位置的类型函数（普通、紧急或承诺），5http://www.upp等。Com摩尔206→我⟩• l0∈ L是初始位置。我们使用以下访问函数来引用不变量、保护、同步和赋值。• Inv：L→Labels映射到位置的不变量（可能为真），• Guard：T→Labels映射到转换的守卫（可能为真），• Sync：T→Labels{}映射到转换的同步标签（如果有），并且• Assign：T Labels将重新映射到与过渡关联的分配（可能是空列表）。Def. 2（Uppaal模型）UPPAAL模型是元组A，Vars，Cl，Ch，Type，其中• A是一个向量的过程A1，. ，An;我们使用索引i来表示 Ai-特定部分Li、Ti、类型i和10，• Vars是一组变量，对应于有界整数和数组，• Cl是一组时钟，Cl<$Vars=，• Ch是同步信道的集合，Ch_Vars=Ch_Vars并且Ch_Cl=Ch_Cl，• Type是扩展Typei的多态类型函数，即，类型映射· 位置为{o，u，c}（普通、紧急或已提交-根据类型i），· 信道到{o，u}（普通或紧急），· 变量为{int，array}。我们使用o，u，c，int和array作为谓词，即， 对于同步信道s，表达式u（s）评估为真，当且仅当Type（s）= u。Def.3（配置）U型PPAAL模型的配置：A，Vars，Cl，Ch，Type是三元组（l，e，v），其中l是控制向量，e是环境对于离散变量，ν是时钟评估，即：• l=（l1，.，ln），其中li∈Li是进程A i的位置，• e：Vars →（Z）将每个变量v映射到一个值（如果是int（v））或一个值的元组（如果是array（v））。• ν：Cl → R ≥0将每个时钟映射到非负实数。 对于d> 0，记法（ν + d）：Cl→ R ≥0描述了函数“ν移位d”，有如下意义：<$x∈Cl。 （v（x）+d）= v（x）+d。为了简单起见，我们只允许一个初始配置，表示为.（l0，. ，10），101n[Vars<$→（0）]，[Cl<$→0]，其中所有过程都在其初始位置，所有变量和所有数组位置的值为0，所有时钟为0。局部属性是一个布尔表达式，它覆盖变量、Cl和项Ai.li。在模型的任何配置中，它要么是真的，要么是假的。 我们用符号e，ν| =来声明局部属性在所包含的变量和时钟的求值e，ν下保持为真。类似地，我们写（l，e，v）|=在包含形式Ai.li的表达式的情况下。Ai.li为真，当且仅当进程Ai位于位置li，即，l =（.，li，.. . ）.摩尔207不不−−−−→我aJJJ我j−−−→我J我 J我 我 JJJ我J我2.2UPPAAL时间自动机的迹语义我们将一个U型模型M与一个典型不可数集相关联（M）迹线是无限的或最大扩展的（死锁）。如果在（M）个导联中没有迹线，则模型M确实满足安全性质到一个违反安全的配置。 一个普适路径性质在M中成立，如果所有轨迹都符合此属性。我们从制定简单动作、同步动作和延迟步骤开始。为了修改控制向量l，我们使用符号l[liJ/li]来指示在位置i处，li被liJ替换，并且其他位置不变。我们很容易使用赋值a作为函数e（和ν）的变换器，并将结果赋值为a（e）（和a（ν））。a中的赋值被认为是按发生的顺序适用的。定义4（简单动作步骤）对于配置（l，e，ν），简单动作如果存在转换L，则步骤g，alJ∈T， l在l中，使得(i) e，ν |= g, and(ii) a（e）、a（v）|=Inv（liJ），以及(iii) 如果在l中用c（lc）表示l c，则c（li）。i−−→i i i我们把它简化为h（l，e，v）=a∈（l[lJ/l]，a（e），a（v））.Def. 5（同步动作步骤）对于配置（l，e，v），当且仅当对于通道s存在两个同步动作步骤时，启用同步动作步骤。转换lg i，s！，ailJ∈T且 lg j，s？，ajlJ∈T，我，我在l中，i=j，使得(i) e，ν| =gigj，并且(ii) aj（ai（e）），aj（ai（v））|=Inv（liJ）<$Inv（ljJ），和nd(iii) 如果l中的c与c（lc）相等，则c（li）相等。c（lj）。Σ我们可以用h（l，e，v）=s？？l[lJ/l][lJ/l]，a（a（e）），a（a（v）.Def. 对于配置（l，e，v），具有延迟d的延迟步骤当且仅当以下所有条件成立时，才启用(i) e，（ν +d）|=Inv（li），我(ii) 伊因湖 - c（li），(iii) 不允许离开紧急位置的动作步骤，即， 如果u（li）对于某些li∈l，则.Σ<$（l，e，v）=<$（l，e，v）.s！（l，e，v）=（lJ，eJ，νJΣ），以及(iv) 在紧急信道上不启用同步动作，即，（l，e，v）=s！？ （lJ，eJ，νJ）蕴涵< $u（s）。我们用h（l，e，v）=d（l，e，（v+d））来简化它。Def. 7（定时跟踪）一类U型模型的迹是有限的或无限的，配置序列{（1，e，v）}K =（（1，e，v）0，（1，e，v）1，. ）与K步骤，K∈ N <${∞}，使得我摩尔2081不n我一一一.Σ（i）（l，e，v）0=（l0，... ，l0），[Vars <$→（0）n]，[Cl<$→ 0]，(ii) 对于每个k K，两个随后的配置k和k+ 1是经由简单动作步骤、同步动作步骤或延迟步骤连接，即，（l，e，v）k=a<$（l，e，v）k+1或（l，e，v）k=s！？（l，e，v）k+1 或（l，e，v）k=d（l，e，v）k+1，annd(iii) 迹线是无限的或最大延伸的，即，如果K <∞，则对于（l，e，v）K，不启用动作步骤或延迟步骤。Def. 8（迹语义）设M是一个U型时间自动机模型。那么M的迹语义，写作（M），是可以根据定义7构造的迹的集合。我们现在准备正式定义定时可达性和定时安全性。Def. 9（定时可达性/安全性）我们将定时可达性定义为一个双向的一类U型时间自动机模型M与可达性谓词E<> M，其中M是M的局部性质。M|当<且仅当<${（l，e，ν）}K∈ T（M）. 克兰克<湾（l，e，v）k|= 0。定时安全，用M表示|= A[]，则是定时可达性的对偶：M |= A[] ϕif and only if ¬ ( M|= E<> ¬ϕ ).3模型增强我们引入模型增强作为一种技术来丰富给定模型的行为这被证明是保守的定时安全性能在一个方向上。模型扩充需要增加可达状态空间的大小。然而，要探索的符号状态的数量可以更少，因为更大的部分可以在一个步骤中覆盖。我们通过一个简单的延迟环例子来说明这种现象我们定义一个原始的转换如下。UPPAAL模型形式上为定义10（模型增广）设M=λA，Vars，Cl，Ch，Typeλ为g，aUPPAAL模型，且l令A=l−−→lJ， L， T，Type，其中• 对于某个过程Ai，即A的一部分，li∈Li，其中我们要求o（li）;我们称li为A的增广点，• g一个警卫，• aa作业列表• lJ∈ LA，LA是一组新的位置，LA<$（Li） =0，• TA是一组转换，使得所有源都在 LA中，并且所有目标都在L A中。在LA Li中，• 类型A：LA→ {o，u，c}新鲜位置的类型函数。摩尔209y = 0时X 10快速x =大y == 10y = 10g，a我我一我一我我大MA（M）国家数量时间[秒]内存[KB]国家数量时间[秒]内存[KB]1080.0137690.01448100350.0144090.0137610003050.0442490.0144010· 0003· 0051.511· 70490.01440100· 00030· 005175.215· 44090.024161· 000· 000300· 005 22· 449.9442· 79290.02400表1则AugA（M）是U型模型，它丰富了M在以下意义上：（i）AS= A1，...，Ai−1，AJi，Ai +1，.，An，与AJ=<$L<$L ， T<$T<${l−−→lJ}，Type联系方式，10分，6分（ii）类型J通过将位置lA∈ LA映射到类型A（lA）来扩展类型。我们称A为模型增广，AugA（M）为增广模型。例11（延迟环路）考虑一个模型M，其中只有一个过程P（图1）。P执行多个持续时间为10的延迟循环，并在达到总延迟LARGE当性质E>P.QUICK在前向状态空间探索中被验证时，在确定位置QUICK确实不能到达之前，大量的这些延迟环被探索。图1示出了图1上的增强模型AugA（M）。对，在哪里.A=T−x−−=−−LA−R−G→EΣAUGMEN T，{AUGMENT[I nv：x<=LARG E]}，{AUGMENT−→S}。增强过程可以被理解为增强x =大x >大型不y：= 0Sx >大型不y = 0时X 10快速x =大y：= 0Sx =大y == 10y = 10Fig. 1. 原始过程P（左）和具有模型增强A的P（右）。表1示出了利用Uppaal的前向可达性分析的数据。7The6 符号表示不相交的联合。7所有运行时测量都是使用UPPAAL的命令行版本执行的，verifyta 3.1.58，在Solar OS下的UltraSPARC-II 300 MHz上执行。我一摩尔210⟨⟩T Tg，a一一一我A−−→一一一一J在原始模型中，过程P（左）的探索状态数在参数LARGE中线性增加，而当使用AugA（P）（右）3.1模型增强的合理性我们的技术是健全的证明，一些地方的财产持有不变。定理12（可靠性）设M=A，Vars，Cl，Ch，Type是U型模特和模特是当地的财产。 则对于任何模型增强A =g，a布里尔lJ，L，T 用l表示对于某个i ∈ L，以下成立。M |=E<>|= E<> ϕ证据我们证明了（男）（AugA（M））. 为此，它表明，对于在M中达到的任何配置s=（l，e，v），在AugA（M）中的相应配置sA=（l，e，v）假设在% s中启用了简单或同步的操作步骤。每M的跃迁，在AugA（M）中存在一个等价的跃迁以定，第10条，o（l），则<$c（l）和过渡Lg，aL没有优先于其他行动步骤。由于s和sA的l、e和ν相同，因此在sA中启用相同的简单或同步动作步骤。假设在s中启用持续时间为d的延迟步长。则条件（i）至（四）符合第六项定义。对于sA，条件（i）和（ii）也成立，因为l、e和ν对于s和sA是相同的。满足条件（iii），因为在s中没有启用离开紧急位置的动作步骤。 o（1A）需要<$u（l），thusl−−→lJdoes不属于对es的任意处理。对于条件（iv），lg，aL没有同步的定义，A−−→A点火。因此，在sA中不能启用紧急信道上的同步，除非它也在s中启用，但情况并非如此。因此，在配置sA中还启用持续时间为d的延迟步骤，从而完成证明。Q推论13（安全保守设M是一个这是当地的财产。 对于任何模型扩增A：UPPAAL模型和A（M）|= A[]M |= A[]3.2适当的增强虽然没有正式要求，模型扩充必须返回到原始的控制结构。否则，他们永远不会得到改善。模型扩充增加了状态空间和非确定性水平.总的来说，这是一件坏事。只有当额外的循环消除了只能通过时间的推移来区分的控制序列的冗长乏味的重复时，这种修改才是有益的。也就是说，重复A−−→一一一一J摩尔211模一定的时钟偏移必须存在。在利用这种现象之前，必须在模型的所有过程中应用在状态空间探索的早期采用新引入的循环是至关重要的在前向可达性分析中，这可以通过使用广度优先搜索顺序来实现。然后在具体控制返回到增广点之前探索一个增广循环。更严格的可能性是修改模型检查算法，以便首先探索开始模型增强的转换。成功的模型增强所面临的挑战是(i) 为了找到有希望的增强点，(ii) 确定适当的延迟，以及(iii) 构造应触发返回原始控制结构的条件在第5节中，我们在一个中等规模的例子中讨论了这一点，其中有两个并行任务，其中一个循环调度器决定了随着时间的推移重复4通用路径属性的模型扩充通用路径属性是TCTL的片段，其中一个属性可以被单个反例跟踪反驳。我们扩展我们的模型增强技术是保守的，这更丰富的属性集。为了保持死锁，我们修改了与模型扩充相关的转换关系。通用路径属性的形式如下：：=A[]..中文<（简体）.. ζ∨ ζ... 没关系 ϕ这是一个当地的财产。特别地，无界响应的定义A[]A>等价于A[]<$A>，因此是一个普适的路径公式。运算符A>表示必然性：在未来的某个时刻，某些属性必然成立。<如果存在一个不包含配置的无限迹，其中，到达死锁而不经过死锁保持的状态。迹σ =（s0，s1，. . ）∈ T（M）满足位置i处的普适路径公式，根据以下规则：（σ，i） |=A[]j≥i。（σ，j）|=（σ，i） |=A<>n=1 （σ，j）|=（σ，i） |=2（σ，i）|= σ1或（σ，i）|= σ2（σ，i）|=2（σ，i）|= σ1和（σ，i）|= σ2（σ，i）|=si|=一个 模型M满足一个公式σ，如果对于所有迹σ =（s0，s1，. . ）∈ T（M），摩尔212g，ag，a我一一一（σ，0）|= 0。8应用具有普适路径属性的模型增强提出了一个技术问题。可能的情况是，在增强点处的新转变允许从死锁情况中逃脱，其中没有进一步的动作转变是可能的。在这种情况下，A>属性在增广模型可以保持，尽管它们不适用于原始系统。解决方案在概念上很简单;我们要求，在增强点中，只有在另一个动作转换也可以进行的情况下，才可以进行添加的转换。我们将其形式化如下。定义14（增广路径语义）设M是一个UPPAAL定时的au.tomatamodelanddA=l−−→ l j，L，T，T y p e M o del augmen t a ta t i mmO D E La n d d A = l − − → l j，L， T，Typemodelaugmen t a t a ti m o de l and d A = l − − → l j，L，T，T y p e m o d e m o d e m o d e l.我们将AugA（M）的弱迹集定义为根据定义7的迹集的子集通过以下侧条件从T（AugA在一个配置（l，e，v）中，当hli∈l时，在li−−→lJ上变换i上的作用i仅为如果启用了另一个操作转换，则启用从 T （ AugA （ M ） ） 中 移 除 违 反 此 条 件 的 所 有 迹 以 产 生 TA （ AugA（M））。我们写AugA（M）|当且仅当对于所有迹σ=（s0，s1，.. . ）∈TA（AugA（M）），（σ，0）|= 0。命题15（保守于普适路径性质）设M是一个U型时间自动机模型，M是一个泛路性质. 对于任何模型扩增A：A（M）|= AM |= ζ示例16对于具有图1中的单个过程P的UPPAAL模型A（M）|= AA[]（<$P.T <$A<>P.S），因此M |= A[]（<$P. TA<>P.S）。请注意，无论何时启用转换T→AUGMENT，由于T中的不变量y≤0，M中的一个原始转换被启用为好. 因此，对于T → AUGMENT，总是满足边条件，并且T（AugA（M））= TA（AugA（M））。5快速验证砖块分拣机我们演示了如何将我们的模型增强技术应用于一个特殊的类的例子，即基于任务的乐高积木RCXTM的升级程序，可以自动转换为UPPAAL模型。 我们使用[10]中的砖块分拣机示例作为案例研究。砖块分拣机模型在控制循环的地方得到了增强，8由于我们的模型语义包含时间收敛的迹线，A>属性仅在时间进程假设下成立：全局参考时钟最终必须超过任何时间界限，比较[1，2]。摩尔213结构被检测到。对于安全属性，这在模型检查时间方面产生了加速。5.1砖块分拣机模型砖块分拣机（图2）是一台由传送带、光传感器和踢臂组成的机器。红色和黑色砖块在传送带上经过传感器，传感器足够敏感，可以区分两种颜色。 一段时间后，踢O臂可以推动一块砖的皮带。一个控制器协调传感器和踢O臂，并试图确保每一块黑砖都被推到踢O臂上，而每一块红砖都被允许通过。在物理实现中，该系统内置于LEGO 中，以RCX TMMindstorm微控制器作为控制单元。该控制器执行由确定性调度程序以循环方式组织的两个十任务。在RCXTM中使用两个任务主任务和启动任务程序，这是翻译成三个U PPAAL过程[10]。 三个亲-cess模拟环境。并且一个Hurry_Dummy被添加到紧急信道Hurry上的永久操作者同步。这就构成了U型分拣机。 我们想建立一个安全属性，第二块砖被踢出，而不管它精确地何时进入传送带。形式上，我们模型检查排序器|= A[]<$black_brick2.PASSED.分拣机流程：传感器？！ 启动臂RCX型号RCX 0主任务RCX0启动任务环保黑砖黑砖2踢离臂快点笨蛋图二. 砖分拣机示意图5.2砖分拣机模型的扩充然而，某些类别的例子表现出相当规则的结构，这种技术可以更系统地应用。我们在这里提到乐高RCXTM微控制器，其中NQC程序可以自动translate到U PPAAL模型进行分析。我们使用NQC程序到UPPAAL模型的翻译[10]。原始任务被转换为UPPAAL过程，WAIT-UNTIL语句对应于增强点。此外，还必须修改控制器以允许停车状态。UPPAAL模型分类器的模型检查的一个问题是，在某些时间点，进程执行忙循环。 更准确地说，当传感器等待看到砖块或踢臂等待砖块摩尔214为了处于正确的位置，所有的过程都经常返回到相同的控制状态（经过一些延迟）。我们试图通过适当的模型扩充来避免这种繁忙的循环。这可以理解为允许进程在某些情况下暂停，直到启用定时条件保持为真。从UPPAAL模型排序器开始，我们定义了一个模型序列，增强 进程RCX、RCX 0_main和RCX 0_kick_off是增强的。增强点的选择是根据的特定过程。RCX 0_timer 1RCX 0_active [RCX0_currentTask]==1，RCX 0_timer==CSRCX 0_timer：=0 RCX0_Go！RCX 0_startRCX 0_active [0]：=1，RCX0_currentTask：=0，RCX 0_timer：=0RCX 0_active [RCX 0_currentTask]==0，RCX 0_timer ==CSRCX 0_timer 1RCX0_startRCX 0_inTaskRCX 0_timer：=0，RCX0_Go？RCX0_inSchedRCX0_timer =CSRCX 0_timer：=0，RCX0_currentTask：=RCX 0_currentTask +1RCX 0_active [RCX0_currentTask]==1，RCX 0_timer==CSRCX 0_active [0]：=1，RCX0_currentTask：=0，RCX 0_timer：=0RCX 0_currentTask：= RCX0_currentTask +1RCX 0_active [0] == 0，RCX 0_active [1] == 0RCX 0_Go！RCX 0_timer：=0RCX 0_active [RCX 0_currentTask]==0，RCX 0_timer==CSRCX0_inTaskRCX0_Go？RCX0_inSchedRCX0_timer =CSRCX 0_timer：=0，RCX 0_currentTask：=驱动快点？RCX 0_active [0]==1停车RCX 0_timer：=0，RCX 0_currentTask：= RCX 0_currentTask +1RCX 0_currentTask+1快点？RCX 0_active [1]==1RCX 0_timer：=0(i) （ii）增加的可持续发展进程图3.第三章。Round-Robin按钮会反复在任务列表中切换任务0 = main增强_1RCX0_Go！增强_2RCX0RCX0RCX 0_timer ==143RCX 0_timer = 143RCX 0_active [0]：= 0RCX 0_IN_1> 42RCX 0_IN_1 = 42快点？RCX 0_active[0]：= 1RCX 0_active [0]：= 1RRRCX 0_timRCX 0_main_51_S1RCX 0_IN_1 =42RCX 0_Go？RCX 0_currentTask==0RCX 0_Go！RCX 0_main_51_S0RCX 0_timer：=0RCX 0_timer ==20RCX 0_IN_1>42RCX 0_Go！059测试输入（0）<=var[4]，70067跳转59RCX 0_main_51_S3RCX0_currentTask==0RCX0_Go？070...RCX 0_timer = 143RCX 0_timer==143RCX 0_timer：=0RCX 0_main_59_S1RCX 0_timer = 20RCX 0_main_59_S0见图4。 乐高RCX TM任务的一部分和相应的U PPAAL过程。- 是的图3（i）显示了UPPAAL过程 它使用数组RCX 0_active和整数变量RCX 0当前任务，以跟踪下一个要释放的任务。如果可能的话，它通过转换到RCX0_inTask来实现这一点，否则通过RCX0_inSched的self循环空闲。如果一个相应的任务是活动的，则释放该任务的执行（RCX 0-inTask）。任务执行一条指令，然后通过在通道RCX 0 go上同步，将控制权交还给调度程序。如果相应的任务处于非活动状态，则跳过该任务（向右自循环）。...031 InType2、开关034 InMode2、布尔型037 OutDirA，前向039 OutModeA，打开041 输出功率A，1045 OutDirB，前向047 OutModeB，打开049 输出功率B，6053 显示1057 StartTask1RCX0_Go！摩尔215#探索状态平均继承人数#死锁时间[秒]存储器[KB]分类器151· 1031.28086.841· 840AugA（Sorter）22· 9662.092021.152· 512表2此后，调度者继续进行下一个任务。当超过现有进程的数量时，变量RCX 0- current task将返回0。增强调度器（ii）在右侧示出。如果任务不活动，则可以到达停车场。如果其中一个任务再次激活，则必须立即离开该位置。这是通过在紧急通道Hurry上同步并声明位置Driving紧急来实现的。任务在进程RCX0_main和RCX0_kick_off中，条件测试导致控制结构中的循环。在八个地方应用了模型增强。其中六个是等待条件成立的条件，如一个如图4所示。剩下的两个允许可选的时间延迟，只要进度取决于要满足的时间条件这相当于9个模型增强，增加了16个位置，总共有34个转换。我们参考了其他改进的自动分拣机（分拣机）。表2中列出了分拣机和自动分拣机（分拣机）的配置。 所有运行均使用优化选项-sWabA -S 2（主动时钟减少、广度-firstsearch、convexhullapproximation、最小速度。在AugsortA（排序器）中，前向状态空间探索的运行速度快四倍，但消耗很少更多的内存。这是应用凸壳优化的结果。在排序器中，凸包是在许多遇到的区域上构造的，每个区域都有一个小的延迟。也就是说，对于每个离散部件，最多存储一个区域。AugA（分拣机）是一种用于为新一代客户提供数据的设备控制位置。自动排序器（排序器）是一种高度成功的经验，它可以理解额外的非确定性。 此外，AugA（排序器）产生额外的死锁状态，显然是由于不幸的时间冲突。一般来说，这是不可取的，因为仍然不清楚原始模型是否是无死锁的。然而，在这类例子中，原始模型在构造上是无死锁的，因此死锁必然是虚假的。请注意，自动分拣机（分拣机）也适用于其他功能。如果yhold_dinAugA（排序器），则状态空间在一次运行中被动态扩展;因此，运行时数据将是相同的（模小运行时在计算一个符号配置的不变量时的困难）。在模型检测运行中，我们利用凸壳近似技术。这种近似增加了可达状态的数量，摩尔216在一个方向上具有安全属性的保守。在没有此选项的情况下，在此示例中创建的大量符号状态超过了用于排序器和用于Aug排序器A（排序器）的可用1G B。6总结模型增强是一种专门的近似技术，对各种时间自动机方言都是安全的。请注意，我们限制了流程的修剪，即，系统的现有行为从未被禁止。这使得我们的技术的一般合理性证明，并与其他近似技术相结合成为可能。在我们的应用程序上的乐高LEGO RCXTM程序，节省并不显着。尽管如此，在一个砖分拣机的例子运行时的改进证明，该技术有潜力。节省了大约75%的时间但是增强模型消耗了稍微多一些的内存。需要更多的实验来确定这是否仅限于本例。任务的增强点可以从UPPAAL模型的控制结构中导出，甚至可以直接从LEGO RCXTM程序中导出。存在从这些程序到相应U PPAAL模型的翻译[10]。可以修改该转换以直接计算UPPAAL模型的增强版本，从而在这类应用中为该优化技术我们的技术与[7]中的凸壳过逼近有关然而，它在近似的选择上有更细的粒度，甚至可以与凸包相结合。除了凸包，我们的技术规定了一种方法来修改模型检查算法，使通用路径属性从增强模型到原始模型。致谢。 感谢Kim G。拉尔森提供了许多有用的评论。引用[1] 马丁·阿巴迪和莱斯利·兰波特一个老式的食谱实时。Rex Workshop“Real-Time：Theory in Practice”，Lecture Notes in Computer Science，第600号，第1-27页，1992年[2] Rajeev Bogurr，Costas Courcoubetis，and David Dill.高密度实时模型检测。信息与计算，104：2[3] 放 大 图 片 创 作 者 ： Rajeev Bogurr ， Costas Courcoubetis ， NicolasHalbwachs，Thomas A. Henzinger，Pei-Hsin Ho，Xavier Nicollin，AlfredoOlivero ， Joseph Sifakis ， and Sergio Yovine. 混 杂 系 统 的 数 学 分 析 。Theoretical Computer Science，138（1）：3摩尔217[4] 作者 声明： David Dill. 时间 自动机 理论 Theoretical Computer Science ， 2（126）：183[5] 放 大 图 片 作 者 ： John Bengtsson ， Pedro R. D’Argenio, AlexandreLarsen ， M.OliverMo？ ller ， Pa ul Pettterss on ， C ar tenWeis e ，andWangYi. U PPAAL-现在，下一个和未来。In F.卡塞角雅德湾Rozoy和M. Ryan，编辑，并行过程的建模和验证，编号2067计算机科学讲义，第100Springer–Verlag,[6] Edmund M. Clarke，Orna Grumberg，and Doron A.佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[7] 孔拉多·道斯和斯塔夫罗斯·崔帕基斯使用抽象的实时可达性属性的模型检验。在 Bernard Ste Escheren ， 编 辑 ， Proc. of the4thWorkshop on Tools andAlgorithms for the Construction and Analysis of Systems ， number 1384 inLecture Notes in Computer Science，pages 313-3