共享资源的实时抢占进程代数TPAP在航空电子领域的应用与验证

68《理论计算机科学电子札记》65卷第6期（2002）网址：http://www.elsevier.nl/locate/entcs/volume65.html18页TPAP：一种验证具有共享资源的实时系统的抢占进程代数J'erumeomeErmont和Fr'ed'ericBoniol1ONERA - CERT -DTIM2 avenue Edouard Belin -BP 402531055 Toulouse Cedex摘要本文描述了一个时间进程代数TPAP。该算法的目的是允许对共享公共资源的实时嵌入式进程进行建模，这些进程对通信延迟和调度策略敏感。 定时广播和进程中断抢占是代数的两个主要基本概念。 它们允许描述同步器和异步通信介质，因此在验证全球系统的实时行为时可以考虑这些。我们首先介绍了进程代数，并讨论了它的性质。然后使用TPAP开发了航空电子领域的案例研究，并通过翻译到UPPAAL模型检查器进行了正式验证。1介绍嵌入式系统的设计和掌握是一个主要的挑战，其相关性随着新一代飞机的到来而增加 其复杂性源于其关键性、实时性、高度分布式和集成性。 为了克服这种复杂性，飞机制造商已经选择在联邦架构原则上构建航空电子系统：现代飞机（例如空中客车A340/A330、波音B777、欧洲战斗机或阵风...）的航空电子系统。主要由并行运行、多路数据总线通信、公用机组共享的功能组成这样的系统的功能架构可以用一般术语来描述，S=（S1·S2Sn）··1电子邮件：{ermont，bonnut}@cert.fr2002年2月出版，电子科学和B。 V. 操作访问根据C CB Y-NC-N D许可证进行。J. ERMONT，F.博尼奥尔69为了避免单一的灾难性故障，航空电子功能S1...Sn是基于广播的（即，从1到N个非阻塞传输）。不幸的是，这些通道可能会在系统中引入不确定的（但必然有界的）延迟。此外，航空电子功能可以共享公共计算机。然后，这些计算机上的时间被划分为由每台计算机一个调度器控制的时间片。其基本机制是先占。根据操作上下文和环境，计算机在任何时候决定哪个功能（分配在这台计算机上）必须被执行，哪个功能必须被抢占。抢占是处理实时嵌入式系统（如航空电子系统）的主要机制。然而，抢占行动可能会引入不确定的，tic延迟。因此，考虑到系统的功能架构是必要的，但不足以分析全球系统的行为还必须考虑由每台计算机执行的调度策略和通过通信信道的通信延迟。为了验证实时系统的某些性质，已经定义了几种形式时间自动机[3]允许对进程的通信和行为进行建模不幸的是，由于自媒体表现力的丰富性，它们的行为很难控制。因此，有必要将这种表现力限制在与所研究的问题有关的行为上因此，使用进程代数可以更容易地描述我们必须研究的实时系统，从而避免时间自动机问题。大多数实时进程代数[17，4，15，9，10]充分捕获了由于进程同步或动作引起的延迟;然而，它们通常通过假设理想的操作环境来抽象资源特定的细节本文提出的代数提供了一个正式的框架，结合了进程代数和实时调度领域，从而可以帮助推理系统的最后期限，进程交互，和资源可用性是敏感为了允许抢占机制，进程代数ACSR [7]定义为：P. 我和我的兄弟们。因此，使用表示资源消耗的优先级和定时因此，如果P和Q是分别使用优先级为2和3的资源r的两个进程，则Q抢占P并在资源r上执行。另一个进程代数定义为M. Buchholtz和al。[8]设计用于模拟共享处理器。这个代数是基于这样一个事实，即时间可以通过两种不同的方式演变：使用处理器或不使用处理器。当一个进程处于活动状态时（即可以在处理器上执行）时，时间经过处理器，在该处理器上该进程表征执行时间。当一个进程被抢占时，它让时间独立于处理器而流逝调度策略也是不-J. ERMONT，F.博尼奥尔70V{···}P·∈A∈A使用优先级。我们的代数的计算模型是基于这样的观点，即实时嵌入式系统由一组具有相同优先级的通信进程组成，并且当接收到给定的消息时，这些进程可以被抢占。这样形式化的抢占机制非常类似于反应式同步语言ESTEREL [5]的共享资源的使用将通过进程的抢占来建模，并且通信将由非阻塞广播动作和定时延迟来支持然后，进程的执行受到控制其使用的资源的调度器发送的中断，即，取决于资源的可用性。本文的其余部分组织如下。第2节描述了代数的抽象语法讨论了无死锁性等性质然后提出了一个强时间互模拟及其方程律之后，第3节介绍了一个航空电子设备案例研究，该案例研究形式化了我们的代数，并通过转换到UPPAAL模型检查器[12，1]进行了验证。2带抢占的时间进程代数2.1语法设A是代表事件传播的一组紧急行动。A的元素用a、b、c表示。......你好。让我们把A看作是一组由A ={a|a∈ A}。A中的a表示事件a的接收。让我们考虑也是一种可见的作用，使得ε∈/A<$A。ε将用于表示中断延迟时执行的不可见操作。A set =X，Y，of变量用于递归定义。 最后，考虑在我们的代数中是R并由T表示。现在，我们可以定义代数的表达式，范围为P，Q.通过以下语法：P：：=δ|X|AP|AP|IP|P+P|P·P|X. P|（P↑a）P其中：• 进程δ除了空转什么也不能做• 定义了两种类型的动作：动作a表示事件非阻塞传输，动作a表示事件阻塞接收。进程aP执行紧急动作a，其行为类似于进程P。进程aP在接收到事件a后的行为将类似于P。否则它就闲置了。• 进程P Q可以独立地执行P和Q的操作，或者可以同步互补的操作（如a或a），或者如果P和Q能够这样做，则可以空闲• 过程P+Q表示P和Q之间的选择。选择不仅取决于行动，也取决于时间例如，如果时间可以在≥0J. ERMONT，F.博尼奥尔71我↑↑T{∞}II我∈ P那么P+Q可以像P一样演化。•是一个封闭的时间间隔，它表示一个非确定性的延迟与limits。如果的上界不为空，P也可以空闲t个时间单位，只要t小于（或等于）这个上界。此外，如果它的下限为零，则进程P可以执行不可见动作ε并表现得像P。• 进程（P a）Q是一个抢占进程，它的行为类似于P，直到接收到事件a，然后放弃P并成为Q。这样的操作将有助于描述共享同一资源的进程的行为设R=（Pa）Q，P称为R的被抢占子项.• 最后，过程recX.P是经典的递归定义，它允许指定无限行为。定义2.1（自由变量）设P∈ P. P的自由变量集称为free（P），由P上的结构归纳法定义：自由（δ）=δ自由（aP）=自由（P）自由（aP）=自由（P）free（IP）=free（P）free（P+Q）=free（P）free（Q）free（P·Q）=free（P）free（ Q ） free （ （ P↑a ） Q ） =free（P）free（Q）free（X）={X}游离（recX.P）=free（P）\{X}一个项P是封闭的，当且仅当free（P）=。 一个项P是正则的当且仅当它的所有并行和抢占的子项都是闭的。让Prb常规过程集。例如，P=recX。（aX·bδ）和dQ= recX。（aX↑b）δ被认为是非正则过程。现在让我们介绍一个过程的时间上下限定义2.2（上限和下限）J. ERMONT，F.博尼奥尔72≤P我设U：P → T{∞}是由归纳法定义的上限函数：U（δ）=∞U（IP）=pifI=[m，p]U（aP）= 0U（aP）=∞U（X）= 0U（recX.P）=U（P）U（P+Q）=max（U（P），U（Q））U（P·Q）=min（U（P），U（Q））U（（P↑a）Q）=U（P）设L：P → T{∞}是由归纳法定义的下限函数L（δ）=∞L（IP）=mifI=[m，p]L（aP）= 0L（aP）= 0L（X）= 0L（recX.P）=L（P）L（P+Q）=min（L（P），L（Q））L（P·Q）=min（L（P），L（Q））L（（P↑a）Q）=L（P）对于r中的给定进程P，U（P）=N意味着P可以在持续时间t内空闲，当且仅当t N。此外，L（P）=n意味着P必须在持续时间n期间空闲，即在n个时间单元之前不可能有动作。定义了这两个函数，我们现在可以引入强适时过程的概念要做到这一点，所有这些进程的执行必须执行非空的最小延迟，即具有严格正下限的某个间隔。为了确定一个过程是否是强良时的，我们定义以下谓词。定义2.3设swt：P ×2V×{tt，t}是一个由归纳法定义的谓词：swt（δ，CV，B）swt（aP，CV，B）惠swt（P，CV，B）swt（aP，CV，B）惠swt（P，CV，B）swt（IP，CV，B）惠（L（IP）>0swt（P，CV ，tt））swt（P，CV，B）swt（P+Q，CV，B）惠swt（P，CV，B）惠swt（Q，CV，B）swt（P·Q，CV，B）惠swt（P，CV，B）惠swt（Q，CV，B）swt（（P↑a）Q，CV，B）惠swt（P，CV，B）惠swt（Q，CV，B）swt（recX.P，CV，B）惠swt（P，CV，B{X，}）swt（X，CV，B{X，BX}）优惠（BX=tt）其中CV，B={（X，B）|X∈ V且B∈ {tt，B}}且CV，tt={（X，B）∈CV，B|B = tt}J. ERMONT，F.博尼奥尔73∅P PPPP瑞典广播电视公司一不一→一我P× A × P↑设Pswt={P∈P|swt（P，n）}是强时过程集.例如，设P = recX。[0，2]aX.通过定义swt（P，）=n，即P不是强良时的。它可以在有限的时间内执行无限数量的动作相反，过程Q = recX。[1，2]aX是强适时的。它必须在两个连续动作之间至少空闲一个时间单位。形式上，让rswt是正则强良时进程的集合rswt=rswt.在下文中，我们只考虑rswt中将被重命名为TPAP的进程。2.2操作语义T的元素由t表示。TPAP的操作语义用标号转移系统（Prswt，→）表示，其中→（Prswt×A <$T <${ε}×P）定义见表1。我们写P→Pj是指P可以产生事件a，这样就变成了PJ。同样，我们将P→PJ写成：这意味着P可以在t个时间单位期间空闲，并且这样做变成PJ。如前所述，进程aP正在等待事件a。然后，当从并行协进程接收到a时，它变成P。否则AP必须空闲。因此，这种行为不能用一种关系来定义。一aP→Q。然后，我们必须定义一个辅助关系P~PJ，其中~（rswt rswt），以便表示P等待事件a并且在接收到a时变为PJ。主关系和辅助关系~完全由表1中的规则定义。但是，让我们注意一些语义点：• 规则7，aP~P，定义了接收动作的语义aP等待事件a，并且当接收到事件a时，它表现得像P• 当一个进程发送一个事件（关系n → a）而另一个进程等待该事件（关系n~a）时，两个进程（规则5c和5d）的同步是可能的。• 规则10c表明，通信是基于广播的：一个传输可以同时被多个进程接收。• 如前所述，时间可以做出选择。遵循规则16 b和16 c，如果P可以空闲t个时间单元并且这样做变成Pj，并且如果Q不能（因为t >U（Q）），则P+Q可以空闲t个时间单元并且这样做变成PJ。• 不可见动作ε用于“切割”间隔。P可以在任何时候执行ε（ε是一个持续的动作），这样做成为P当且仅当较低的I的边界为0（规则2）。• 最后，规则8规定了优先购买机制。进程（P a）Q可以接收事件a，然后像Q一样运行。但是，如果没有优先购买权J. ERMONT，F.博尼奥尔74(1)aa∈ AaP →P(2)ε[0，p]P→ P啪啪(4a)→a∈ A <${ε}P+ Qa P'→一PaP 'Q/~(5a)→a∈ A <${ε}帕奎奥帕奎奥→PaP 'Q~aQ'(5c)→aa∈ AQ→P[ recX.P/X]a P'(6)a→a∈ A <${ε}recX.P →P'PbP'(3)→b∈ A（P↑a）Qb（P'↑a）Q→Qa Q'(4b)→a∈ A <${ε}P+ Qa Q'→一P/~QaQ'(5b)a→a∈ A <${ε}PZQ → PZQ'P~aP 'QaQ'(5d)a→a∈ AQ→(7)aa∈AaP~ P(8a)一（P↑a）Q~QP~aP '(9a)一“的P+ Q~ Pa aP~aP 'Q/~Q/→（10a）P Q~aP 'QP~aP 'Q~aQ'(10c)一“的一声Q~P~bP 'a/=b（8b）（P↑a）Q~b（P '↑a）QQ~aQ'(9b)一“ 的P+ Q~ Qa aP/~P/→Q~aQ'（10 b）P Q~aP 'QP[recX. P/X]~aP '(11)一“的建议X.P~ P（十二）δt→δ（十三）aPt aP→(14)t≤p[m，p]Pt[max（0，m-t），p-t]P→PtP'QtQ'(16a)→ →P+ Qt P'+ Q'→PtP'(16b)→t>U（Q）P+ Qt P'→P[recX.P/X]tP'(18)→RecX.Pt P'→Pt P'(15)→（P↑a）Qt（P'↑a）Q→PtP'QtQ'(17)→ →不Q→QtQ'(16c)→t>U（P）P+ Qt Q'→表1操作语义规则如果发生，这个过程执行P的动作（规则3），或者如果P能够这样做，则让时间继续进行这个表达式类似于J. ERMONT，F.博尼奥尔752.3性能本节讨论[16]中定义的一些模型属性时间决定论时间决定论是满足的，当且仅当时间流逝的结果过程是唯一确定的。命题2.4 TPAP是时间确定性的，即P，PJ， PJJ， t：（P→tPjP→tPJJ）PJ=PJJ时间可加性。满足时间可加性当且仅当：一个进程P可以传递t+tJ个时间单位给进程PJ当且仅当P可以传递t个时间单位给进程Q可以传递tJ个时间单位给进程PJ。命题2.5 TPAP满足时间可加性，即P，PJ，t，tJ：（PJJ：P→tPJJPJJ→tJPJ）惠Pt→+tJPJ无死锁。当且仅当任何进程都可以执行一个动作或通过时间时，无死锁性才是满意的。命题2.6 TPAP满足无死锁，即<$P<$l∈A<${ε} <$T <$PJ：P→lPJ有限可变性。有限可变性是满足的，当且仅当任何过程只能在有限的时间间隔内执行有限多个动作。命题2.7 TPAP满足有限变异性。紧急行动。 动作紧迫性是满足的，当且仅当至少有一个进程必须执行动作a∈ A而不让时间流逝。命题2.8 TPAP满足行动紧迫性，即P，PJ∈Prswt， a∈A，t∈T：P→aPJ<$P~t坚持不懈。 当且仅当时间进程不能抑制执行动作的能力时，持久性才得到满足，即P，Q，PJ，t，a：P→aPjP→tQPJJ：Q→aPJJTPAP不满足持续性。例如，进程aP+ [2，3]Q可以立即执行a但是它也可以让2个时间单位过去，这样就变成了[0， 1]Q。它不能执行A。同时，无形动作ε被用来一个被延迟的进程[0，p]P可以执行动作ε或空闲t个时间单位（t≤p），这样就变成了仍然可以执行动作ε的[0，p-t]P。我们讨论ε-持久性，即P，Q，PJ：P→εPJJ. ERMONT，F.博尼奥尔76∼→一2.4时间等价、同余和方程律本节现在介绍进程之间的时间等效性的概念这里使用的定义与米尔纳[14]和拉森和王[13]的作品有关定义2.9（强时间等价）二元关系R是强时间模拟，如果<$（P，Q）∈R <$<$a∈A，<$t ∈T：(i) 当verP→a时(ii) 当verP→ε(iii) wheneverP→t(iv) wheneverP~aPJ ， <$Q ：Q→APJ，<$Q：Q→εPJ，<$Q：Q→TPJ，<$Q：Q~aQJ 和 （ PJ ， QJ ） ∈RQJ和（PJ，QJ）∈RQJ和（PJ，QJ）∈RQJ和（PJ，QJ）∈R对称地，关系R是强时间互模拟。设k为最大的强时间互模拟。强时间等价称为强时间等价。是一个同余，可以由表2给出的一个完整而可靠的公理来定义（本文省略了对同余、完整性和可靠性注1：如[11]中所解释的，对于更简单的实时演算，TPAP不存在展开定理，即通常不能去除并行组合。这一点可以通过使用时间间隔来对不确定性延迟进行建模而无需明确的时钟变量来解释一个直接的后果是，TPAP过程不能编译成连续的条款，而不使用全球和明确的时钟。注2：为了抽象不可见作用ε，可以定义一个弱时间定义2.10（弱时间等价）设f和$定义为：• P• PPJifP（→ε）<$→aPJifP（→ε）<$→t1（→ε）PJ（→ε）···（→ε）→tn（ε）<$PJ，其中t=<$ti≤niaJε aε∗ J• P$P若P（→）~（→）P一个二元关系R是一个周时间的离散模拟，如果R∈（P，Q），R∈A，T∈T：(i) 当verP→a时(ii) wheneverP→t(iii) wheneverP~aPJ ， Q ：QaPJ ， Q ：QtPJ ， Q ：Q$QJ 和 （ PJ ， QJ ） ∈RQJ和（PJ，QJ）∈RQJ和（PJ，QJ）∈R对称地，R是弱时间互模拟。 让你成为最大的弱者一不J. ERMONT，F.博尼奥尔77图1.一、一种操纵面系统，时间互模拟不幸的是，对于TPAP，P不是同余，因为 [0， 0][0， 2]Q<$[0， 2]Q，而是[0，1]P+[0，0][0，2]Q<$/[0，1]P+[0，2]Q。3使用UPPAAL的在前面的章节中引入了这种具有抢占的实时演算的目的是允许对由共享资源、路由器、通信信道等组成的嵌入式系统进行建模和验证。本节提出了一个案例研究这样一个系统正式描述TPAP和验证使用UPPAAL模型检查器。这个案例研究首先在[6]中解释（法语）。3.1航空电子设备案例研究让我们考虑一个子系统，整个航空电子系统的一部分，它控制飞机的副翼该子系统如图1所示该委员会的组成如下：• - 两个共享计算机C1和C2，其执行所有的机载功能（F1，Fi，...，F2，F1，.）• 控制副翼的两个功能F1和F2（分别由C1和C2执行）F2是F1的恢复函数（即，当F1失效时，其代替F1• 控制器Ctrl，随时决定F1是否失效。• 两个通信通道，介质1和介质2，用于将C1和Ctrl之间的启动1和启动2信号传输到C2。每个信号通过每个信道的传输需要0到20个时间单位在正常模式下，F1是主动的，F2是被动的（不执行）。F1周期性地向副翼发送命令J. ERMONT，F.博尼奥尔78（+1）（+2）（+3）P+QQ+PP+（ Q+ R）（ P+ Q）+R P+ PP（↑1）（↑2）（↑3）（δ↑a）P（aP↑a）QaQ（（P+Q）↑a）R（P↑a）R+（Q↑a）R（·1）P·δP（·2）P·QQ·P（·3）（P·Q）·RP·（Q·R）（·4）（P+Q）·RP·R+Q·R（·5）aP·bQ=a（P·bQ） +b（aP·Q）（·6）aP·aQa（P·Q）（·7）aP·aQa（P·Q）（·8）[0，m]P·aQa（[0，m]P·Q） +[0，0]（P·aQ）（·9）[n，n]P·[n，m]Q<$[n，n]（[0，0]P·Q） +[n，n]（P·[0，m-n]Q）（·10）[n，n]P·[n+m，n+p]Q<$[n，n]（P·[m，p]Q）m>0（·11） IP·aQa（IP·Q）如果L（IP）>0（·12）aP·（bQ↑a）R<$b（aP·（Q↑a）R） +（a（P·R））（·13）aP·（[0，m]Q↑a）R<$[0，0]（aP·（ Q↑a）R） +a（P·R）（·14）aP·（IQ↑a）R（a（P·R））如果L（IP）>0（recX1）（recX2）recX.P P[ recX.P/X]如果P[Q/X]<$Q，则Q<$recX.P表2 TPAP公理Ctrl通过Medium1。如果F1失败，则不会再向Ctrl发送“1”。等待70个时间单位后，Ctrl向C2发送“start2”信号。然后F2开始工作，并周期性地向副翼发送 然 后 系 统 处 于 故 障 模 式 。 为 了 简 化 ， 我 们 认 为 只 有 C1 可 以 失 败（Medium1，J. ERMONT，F.博尼奥尔79Medium2和Ctrl应该是可靠的）。图二、正常模式下CPU 1和CPU 2的时间行为每台计算机上的执行由调度程序控制这些处理器周期性地（每20 ms）向CPU（p1和q1到CPU1）发送信号，指示必须执行哪个功能我们假设每个CPU上有两个时间F1（正常模式）和F2（故障模式）在每个CPU的第一个时间片中执行其他功能（不涉及副翼控制，因此在模型化中不考虑）在第二个时间片中执行。图2显示了CPU 1和CPU 2在正常模式下的行为。3.2使用TPAP根据前面的描述，所考虑的系统由七个过程组成，这些过程可以在TPAP中正式定义。F1和F2F1发送“1”和“1ail”并空闲。F2发送“102”并空闲。这些行为可以用以下两个表达式来定义F1 =cmd 1cmd 1all δF 2 =cmd 2δCtrl如上所述，Ctrl等待来自Medium1的信号“1c"。然而，如果它在70个时间单位内没有接收到任何“start 1”的出现Ctrl=recX. （cmd1ctrlX+开始时间2δ）·recX. （（[70， 70]timeout δ）↑cmd1cycle）X在定义这两个CPU之前，我们必须形式化这两个CPU的每个调度程序都会向CPU发送中断J. ERMONT，F.博尼奥尔80∈每20个时间单位：Sch1 =recX.p 1[20， 20]q 1[20，20]XSch2 =recX.p 2[20 ，20]q2[20， 20]XCPU 1在正常模式下，CPU 1执行与F1以及当接收信号“P1”和“Q1”时的其它功能。由于我们对其他函数的行为不感兴趣，我们通过空闲过程抽象它们在故障模式下，CPU1什么也不做，也被空闲进程抽象为了简化建模，从正常模式到故障模式的转换由单个信号“故障”表示，该失效= [0，∞）失效δT1 = p 1 recX。（F 1 ↑q1）（δ↑ p1）X CPU 1 =（T 1↑故障）δCPU 2在正常模式下，CPU 2执行序列T2，当接收到信号“p2”和“q2”时，该序列T2交替副翼控制系统中不涉及的这些函数由空闲进程抽象在故障模式下T2 = recX。（δ↑q2）（δ↑p2）XT2 J= recX。（F2↑q2）（δ↑p2）X CPU2 =（T2↑start 2）T2J介质为了模拟介质1和介质2，我们使用Milner [14]所示的几个简单通道的并行组合。每当简单信道接收到信号时，它会在等待非确定性时间t[0，20]后发送信号。 由于F1每20个时间单位发送信号，并且由于Ctrl至少每50个时间单位发送信号，因此每个介质仅需要两个简单通道。然后，我们可以通过以下方式正式定义这两种媒介：M1 =recX.cmd 1 [0， 20]cmd 1caseXM2 =recX.start 2cycle [0， 20]start 2X介质1=M1·M1培养基2=M2·M2最后，整个系统由前面过程的组成来定义系统=（CPU1·CP U2·Sch1·Sch2·Ctrl·培养基1·培养基2）然后，问题是在假设只有F1可能失效时验证此表达式的两个安全属性（见下一节）下的代数表达式J. ERMONT，F.博尼奥尔81∈E则考虑Sy_stem_J=（Sy_stem·Fai_u_re）。3.3使用UPPAAL进行为了使用UPPAAL进行验证，TPAP的每个术语都必须被翻译成UPPAAL使用的时间自动机（[3]）定义3.1（时间自动机）时间自动机是一个元组A=N，n0，E，C，I>，其中<• N是一组节点• n0是初始节点（用双圆圈表示• C是时钟• I是不变函数，它将每个节点处的不变式关联起来• E是一组边，E <$N × N × Act × 2 C× G。设e=.s，t表示边e的源和目标。a是由e（a！代表发射a和a？表示接收a）。· rt是时钟复位的集合。· gt是守卫的集合。从TPAP到UPPAAL时间自动机的一般转换规则在这里没有给出（但将在本文的长版本中详细介绍）。图3、图4和图5描绘了对应于前一小节中定义的TPAP过程的时间自动机假设副翼操纵系统满足两个安全特性：• 副翼应在120个时间单位之前收到指令• F2只能在F1不工作时工作。为了表达这些属性，我们使用TCTL时序逻辑[2]：1=为了验证这些属性，将R1和R2转换为图6所示的定时自动机。最后的验证在于证明“不快乐”的状态（见图6）是不可达到的。此验证是在256 Mo内存的Sun Ultrasparc 10上使用UPPAAL v3.2.1实现的，对于251和252只需要不到一秒的时间。4结论我们已经描述了一个称为TPAP的时间进程代数，它支持密集时间上下文中的广播和抢占这个正式框架的目的是允许模型化，然后验证实时性。··J. ERMONT，F.博尼奥尔82↑q1？失败？p1？q1？p2？p2？q2？start2？u：=0start2？u：=0p2？u：=0p2？u：=0u =0u==002！p2？u：=0q2？q2？q2？q2？图3.第三章。CPU 1（向上）和CPU 2（向下）的自动机由对共享计算资源上的调度策略敏感的松散耦合通信进程组成的嵌入式系统这样的调度策略可以通过抢占操作来建模。然后，我们开发了一个小的案例研究转化为UPPAAL时间自动机。然后，可以通过模型检查来验证可达性属性。然而，我们的方法的主要不足之一是无法模拟临时先占权，即。悬浮液抢占机制（P a）Q导致在接收到事件a时中止P。在这个意义上，这种表达式的语义然而，实时操作系统通常有更复杂的挂起机制（类似于Unix命令中止和挂起是对具体实时系统建模所必需的两种基本抢占。因此，这项工作的主要观点是延长TPAP与暂停运营商，并将其转化为时间自动机。p1？p1？p1？u：=0u =0u==0101！u：=0u =0q1？u==0快！失p1？u：失J. ERMONT，F.博尼奥尔83=零u==0p1！x>=20u：x>=20u：=0==0q1！你好吗？x：=0x>=70u：=0u =0x =70u==0start2cup！你好吗？你好吗？x：=0u=20u：=0u =0u==0q2！x：=0X =20x>=20u：=0x =20u：=0x>=20u：=0u==0start2！图四、Ctrl自动机（左上），Sch 1和Sch 2自动机（上-中心和右）和介质自动机（下）u =0x>=0u：u==0失图五.故障自动机引用[1] http：//www.uppaal.com.[2] Rajeev Bogurr，Costas Courcoubetis，and David Dill.实时系统的模型检验在第五届IEEE逻辑年会上，01？x：=001？y：=0x =20y =2001？01？y：=0 x：=0u==0好极u==0u==0好极了！好极了！y =20u：=0x=20，x =20u：=0y =20u：=0x=20，y=20，X =2001？01？x：=0 y：=0y =20u =0start2cash？start2cash？y：x =20 y =20start2cash？y：start2cash？u==0start2！u==0start2！y>=20u：=0x=20，x>=20u：y>=20u：=0x=20，u =0start2cashy=20，start2cash？x>=20u =0y>=20J. ERMONT，F.博尼奥尔842002年？什么？h>120什么？什么？h：=02002年？h：=02002年？什么？2002年？不开心什么？2002年？不开心见图6。属性自动机计算机科学，宾夕法尼亚州费城，1990年。IEEE计算机学会出版社.[3] 作者声明：David L.迪尔时间自动机理论。Theoretical Computer Science，126（2）：183[4] JCM Baeten和J.A.伯格斯特拉实时处理代数。Formal Aspects of Computing，3（2）：142[5] 杰拉德·贝里并发系统中的抢占软件技术和理论计算机科学的基础，第72-93页，1993年[6] F. 博 尼奥尔湾Bel 和J. Ermo nt. 适当的 改进 和 验证是一种非常重要的方法，它 需要 一 个异 步 的信 息 分配 架 构： 案 例研 究 和 比 较 。In9`emecon f'erenceinternationalesurles sys t`emestempsr'eelsRTS 2001，mars2001.[7] P. 我和勃雷蒙-格雷瓜尔。李你一种具有密集时间和优先级的共享资源通信过程代数理论计算机科学，189，1997。[8] M. Buchholtz，J.Andersen和H.H.洛文格林共享资源的进程代数。在第二届国际研讨会上的模型时间临界系统，奥尔堡，丹麦，2001年8月。[9] P. D'Baglio。时间与随机系统的代数与自动机。博士论文，计算机科学系，特文特大学，1999年。[10] 哈拉尔德·费彻具有开放间隔和最大进度的实时进程代数。Nordic Journal ofComputing，8（3）：346[11] J. Godskesen和K.拉森实时演算与展开定理。在R. Shyamasundar，编辑，软件技术和理论计算机科学的基础，计算机科学讲义，第652卷，第302- 304315. Springer Verlag，1992年。J. ERMONT，F.博尼奥尔85[12] Kim Guldstrand Larsen ， Paul Pettersson 和 Wang Yi 。 Uppaal in anutshell.International Journal on Software Tools for Technology Transfer，1（1-2）：134[13] Kim Guldstrand Larsen和Yi Wang。时间抽象互模拟：隐式规范和可判定性。信息与计算，134（2）：75-101，1997。[14] R.米尔纳通信和并发。普伦蒂斯·霍尔1989年[15] C.托夫茨湾穆勒通信系统的时间演算。在Proceedings of ConsurSpringer-Verlag，1990.[16] X. Nicollin和J.Sifakis 时间进程代数的综述与综合在KG。Larsen和A. Skou，编 辑 ，第 三 。计 算 机 辅 助验 证 ， 第376-398 页 。LNCS 575， Springer-Verlag，1991年7月。[17] X. Nicollin和J.Sifakis 时间进程ATP的代数：理论与应用。信息与计算，114（1）：131