优先级上限协议验证的工具集

理论计算机科学电子笔记133（2005）315-332www.elsevier.com/locate/entcs操作系统DieterZo？bel，DavidPolock，AndreasvanArkeel1FachbereichInformatikUniversitüatKoblenz-Landau Koblenz，Germany摘要优先级反转问题出现时，优先进程并发地试图进入临界区。这种现象导致对实时过程的最坏情况响应时间的极端悲观估计。在文献中已经提出了各种针对优先级反转的协议，并且在操作系统和运行时执行的系统调用级别上可用。它们属于两个主要的协议家族：优先级继承协议（PIP）和优先级上限协议（PCP）。这些协议的共同点是，它们允许获得更乐观的最坏情况响应时间。与此可预测性方面在时间关键型应用程序中的重要性相反，许多PIP和PCP实现是不正确的，并且允许违反时间界限。本文提出了一个有效的和灵活的工具集，这里应用于验证的PCP族的协议的实现。除了手动设置和仪器外，黑盒验证过程的主要部分都是自动执行的关键词：优先级上限协议，时间关键型应用程序，实时操作系统，半自动协议验证1介绍大量的操作系统和运行时执行程序正在争夺实时和/或嵌入式应用程序的市场。在这种情况下，广告的主要策略是展示在满足基本实时功能方面的完整性。其中之一是针对优先级反转现象的一个或多个协议1 电子邮件地址：zoebel@uni-koblenz.de1571-0661 © 2005由Elsevier B. V.出版在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.071316D. Zöbel等人理论计算机科学电子笔记133（2005）315从应用程序员这些允许的应用程序的良好建立的工程学科，以实现可预测性为一个给定的实时系统。这样做的必要• 进程的最坏情况执行时间• 临界区内执行序列的持续时间• 进程的基本优先事项• (for仅限于PCP）关于某些过程基于此输入，可以推导出过程的最坏情况响应时间，这对于验证进度计划的可行性是必要的（参见[4]，[6]，[11]和[18]）。然而，这种工程方法存在两个主要缺点。第一个结果来自原始文章[10]中对协议的非正式描述虽然协议被证明是正确的，但立即实现将允许优先级反转[7]，并且也违反基本定理[19]。在这一点上，有必要声明，我们的论文的目的不是要对PIP和PCP的发明者的优点提出质疑。相反，应该注意的是，这里提到的问题是一个一般性的问题：存在一个非正式指定的协议，一个执行实时进程的正式模型，一个正确的证明，但一个不正确的协议。这个明显的矛盾是解决的看法-这是不那么明显-在现实中，不是协议被证明是正确的，但其他一些正式的模型。工程方法的第二个缺点来自于实现不可靠的事实。在大多数情况下，关于PIP或PCP协议可用性的虚假广告表现为过度简化的摘录、奇怪的协议接口和各种形式的错误和缺陷。在[9]中给出了几个例子，例如，与声明相矛盾的是，实时操作系统iRMX [16]实现了一种用于取消累积优先级继承的延迟机制。因此，曾经为了获得可预测性而引入的协议在操作系统供应商手中变成了不确定性的来源。在某些情况下，对可行性计算进行轻微修改可以消除这些缺陷（如上文提到的iRMX），而在其他情况下，执行错误是不可修复的，会导致意外违反时间界限。下表强调了大多数操作系统以及一些运行时系统提供了一个避免优先级反转的API：D. Zöbel等人理论计算机科学电子笔记133（2005）315317PIP家族PCP家族-操作VirtuosouC/OS IIOSE系统iRMXRTLinuxPSOsLynxOSOSEK/VDXRTAISolarisSolaris...：：：运行时：阿达95：系统准时RTOS 32实时JavaRTOS-UH Pearl无论操作系统是否提供可预测的PIP或PCP协议，在续集中提供的工具集都有助于重新获得某种我们方法的根源并不新鲜。 有各种各样的论文打算在自己的描述中验证该协议，也就是说不适用于外部实现（参见例如，[8]或[5]）。相比之下，我们的方法在几个方面走得更远。首先，形式化描述可用于多种目的：作为证明系统的形式化基础，作为实现的明确指令，以及作为验证协议实现的工具集的输入（见图1）。第二，同样的形式描述作为协议的操作规范。这个属性可以用于断言动态可测试的不变协议属性，从而建立可验证的标准并避免非正式实现建议的挑战，例如[3]中给出的。此外，该工具集由一个通过定义良好的数据接口进行交互的组件系统组成，该数据接口允许以非常通用的方式验证过程交互，因此不仅适用于PIP和PCP协议。执行验证形式化描述验证Fig. 1. 作为验证、实施和确认本文重点介绍了协议的形式化描述、基于该描述的工具集的组成以及协议实现的验证第2节介绍了正式的描述，它有一个实质性的方向对一个模块化的工具集进行验证的目的。此外，在第2节中，还提到了如何将形式描述用于方案验证。粗略地说，验证协议实现的过程分为两个主要步骤，第3节中为映射到测试套件的并行进程生成执行空间，第4节中执行仪表化实时进程及其评估。最后第5节评估了迄今取得的成果318D. Zöbel等人理论计算机科学电子笔记133（2005）315并且认为该方法可以应用于对抗优先级反转的协议的范围之外。2可互换协议格式协议形式化描述的设计是在符号的通用性和集成到各种操作过程之间的折衷。在我们的上下文中，主要的操作过程是对某些操作系统的一致性进行测试。因此，这里的折衷方案包括基于UML和Z规范符号的协议规范[2]，以可互换的XML格式表示更准确地说，这里使用的是UML的类图和状态图。图形表示背后的元语言被编码到文档类型定义（DTD）中，这样类图和状态图都可以用XML表示。背后的架构概念是从描述安全关键系统的建议中借用的[17]，该建议建立在三个视图上：结构，反应和功能视图。在这种情况下，类图代表结构视图。对于协议的规范，类图描述了相关对象的集合以及它们之间的关系。特别是对于防止优先级反转的协议，相关对象是由单个调度器管理的竞争临界区的进程（见图2）。任何一个类图都有一个唯一的XML表示它的属性，方法和关系，例如。为调度程序：：<操作名称=“sigEnterCS”rtype="”rname="”observable=“TRUE”<参数名称=“p”type=“过程”/><参数名称=“c”type=“CriticalSection”/>：：协议的反应方面由状态图指定。在这些协议的情况下，交互发生在活动对象（进程和调度程序）之间。基于DTD，状态图用一种独特的符号描述，表示它们的嵌套结构、状态和从一个状态到另一个状态的例如，对于来自2sigEnterCS方法在本文中作为一个持续的例子D. Zöbel等人理论计算机科学电子笔记133（2005）315319CriticalSection**+sigPreempt（）+sigRun（）+sigBlock（）+sigUnblock（）+mayEnterCS（CriticalSection c）：bool+mayLeaveCS（CriticalSection c）：bool+notHoldingAnyCS（）：bool+priority：int+actualPriority：int过程想0..1* 1.. n1CS*上限：int0..10.. 1块*ownedBy用途图二. 类和关联在上面的类图中，在调度器的状态图中存在对应的转换。：：对于转换，必须区分一般形式[“[“guard”]”] op”（“param”）”的接收事 件 和 形 式 [“[“guard”]”]“/”[ [target” 的 发 送 事 件 。 “]op”（“param”）”]。事件序列的触发发生在正在运行的进程进入或留下关键部分或运行至完成。例如，由描述的触发事件（也参见图3）[self.mayEnterCS（j）] /sched.sigEnterCS（self，j）以验证是否允许过程实例p获取临界段j。如果这是真的，则进程向调度器类的实例sched发送消息，该调度器类在调度器的状态图中具有对应的接收事件sigEnterCS（图4）。的序列P*1+sigReady（p：Process）+sigEnterCS（p：Process; c：CriticalSection）+sigLeaveCS（p：Process; c：CriticalSection）+sigComplete（p：Process）next（）：Process getRunning（）：ProcessleaveCS（p：Process;c：CriticalSection）wantsCS（p：Process; c ： CriticalSection ） enterCS（p：Process）blockProcess（p：过程;抄送：CriticalSection）wakeUpSet（p：过程）：\fsetProcess ceilingOk（p：Process，cc：CriticalSection）：bool hasPendingCS（p：SysCeiling（p：Process）：CriticalSection调度器<<新加坡>>320D. Zöbel等人理论计算机科学电子笔记133（2005）315当一个可能的新进程以运行进程的状态继续执行时，事件终止。过程封锁getName（）sign（）56sign（）12[self=pidle][else]3睡觉4ready（）78getString（）[self.mayLeaveCS（j）] / sched.sigLeaveCS（self，j）9[self.mayEnterCS（j）] / sched.sigEnterCS（self，j）10[self.notHoldingAnyCS（）]/sched.sigComplete（self）running[self.notHoldingAnyCS（）]/sched.sigComplete（self）11图三.流程状态图另一触发事件在时间触发环境中是实时的。这是由调度器的转换T10建模的，该转换到目前为止，类图和状态图指定了进程和调度程序之间语义，特别是禁止交织的防止，必须用第三种方法来表达，这里用Z-规范表示。选择Z有两个主要原因，第一是易于以数学方式指定协议的语义行为，这也可以用于形式证明。第二个原因是有几个解释器可用于执行Z指定的协议。因此，Z解释器是验证协议实现的有价值的工具。与结构和反应模型一致，Z规范介绍了PCP的功能基础，此处表示为PCP系统。整个描述被称为模式，并被细分为语法部分，定义了它们之间的排序和映射类型。例如，这里指出P是进程的有限集合，优先级是一个映射，给任何进程一个唯一的优先级。以下部分是语义性质的，定义了值之间的关系，例如，进程的实际优先级大于或等于其基本优先级：D. Zöbel等人理论计算机科学电子笔记133（2005）315321PCP系统P：F工艺CS：FCriticalSectionpriority：Process>›不存在优先级：Process ›→Nceiling：CriticalSe›→N拥有者：关键要素›→需求：过程›→关键要素：过程参与关键要素部分：：·actualPriority（p）≥priority（p）天花板={c：CS·c<$→max（{p：dom（usesD{c}）·priority（p）}）}：调度器活性sigLeaveCS（p，c）2h =离开-CS（p，1延迟-EnterCS（n）75[hasPendingCS（n）]3空闲/n.sigRun（）6[else]4/h.sigUnblock（）sigComplete（p）n = next（）r = get-Running（）1610[isSleeping（p）]11/r.sigPreempt（）[else]/p.sigBlock（）sigEnterCS（p，c）12wantsCS（p，c）13[ceilingOk（p）]见图4。调度程序的状态图322D. Zöbel等人理论计算机科学电子笔记133（2005）315公司简介p？：过程P=PJp？∈PJCS=CS优先级=优先级JJstateProcess=stateProcessOwnedby=Ownedby想要=想要JJ使用=使用JstateProcess（p？） =跑步JstateProcess=stateProcess{p？›→准备好了}notHoldingAnyCSPCPSystemp？：过程p？∈Pp？/=pidle所有者D{p？联系我们PCP是高度反应性的，而模式PCPSystem仅表示其静态行为。因此，有必要定义它的动态行为，它对应于调度器和进程的状态图中所描述的状态之间的转换。任何转换、任何保护和任何状态blob都可以修改PCPSystem的状态空间，并且此后由专用的Z模式表示：• 任何状态图的每个转换都有一个对应的Z模式，以表示进程状态或调度器状态的变化例如，通过发送sigEnterCS-消息，进程从正在运行的-状态到就绪状态。 相应的Z模式是TRProcessT10：TRProcessT10符号“PCPSystem”表示实际状态PCPSystem到新状态PCPSystemJ的转换。T10的决定性变化由模式的最后两行反映，其中在关系stateProcess中，参数processp？从运行状态切换到就绪状态。• 每个防护都必须表示为返回布尔值的Z模式例如，当进程运行到完成时，保护self.notHoldingAnyCS（）D. Zöbel等人理论计算机科学电子笔记133（2005）315323p？：进程p！：过程sleeping[p！/p？]下系统n！：过程stateProcessD{running}={}你好！∈PstateProcess（n！）=准备return（n！） = max（{q：P|stateProcess（q）= ready·（q）符号“PCPSystem”表示状态保持不变。如果进程p？在任何临界区之外• 任何状态图的每个状态都可能改变整个系统的状态。特别是，这对于负责执行协议语义的调度器是正确的。作为一个例子，下一个模式必须确定和输出哪个进程n！运行下一个：显然n！被输出为具有最大实际优先级的就绪进程。• 出于技术原因，有必要实例化操作的自由参数，这里具有候选过程或候选关键部分。对应的Z模式根据约定GENClassTransaction命名并被调用。 那里的事务名指向一个特定的方法，其参数在类图中显示。对GEN-模式的调用由实例化参数的序列应答eters。 例如，调用GENERAcerT10来确定可能准备就绪的候选进程：GENEERT10此外，特定协议的特征不变量应该被表达。这个不变量简化了协议验证，有助于检测形式描述中的错误并监控验证过程。在PCP的情况下，不变状态的一个主要谓词：当进程p1拥有一个临界区（关系ownedBy）时，进程p1和p2都可能使用临界区c2（关系uses），那么c2的状态被限制为自由或由p1拥有。324D. Zöbel等人理论计算机科学电子笔记133（2005）315：：状态=空闲PIP1、P2：P; C1、C2：CS|（c 1，p 1）∈ ownedBy（p1，c 2）∈uses<$（p2，c 2）∈uses·ran（{c2}DownedBy）={} ran（{c2}DownedBy）={p 1}PCPSystemInv不变量PCPSystemInv足够强大，可以证明系统在优先级上限协议下的基本属性，例如：一个拥有临界段c1的进程p1在PCP下将不会被阻塞（对应于[10]中的引理9）。这个属性可以直接从PCPSystemInv中导出，因为那些可能阻塞p1（由关系使用表示）的进程（如p2）不允许拥有任何冲突临界区（如c2）。因此，一方面，协议验证必须推导出最终显示定时属性有效性的决定性属性。另一方面，不变量PCPSystemInv的有效性必须通过应用协议的形式化描述来建立。具体而言，这必须通过以下步骤进行验证：(i) 最初，调度器处于空闲状态，并且PCPSystemInv被满足。(ii) 从调度器的空闲状态返回到空闲状态的任何转换序列保留PCPSystemInv。(iii) 任何可能的转换序列都是有限的，并在调度器处于空闲状态时触发。与原始方法相比，新方法以自己的方式证明了协议。3测试集让我们想象一下，一个工具可能带来的好处，以评估所实现的协议对优先级反转的实时功能。测试工具的一个理想结果是给应用程序员一个断言，即对应于PCP的不变PCPSystemInv对于被测实时操作系统（进一步指定为被测IUT下的实现）成立，或者某个其他可能较弱的断言成立。但这种想象力还远没有在一个有效和灵活的工具集中实现。另一方面，有很多关于一致性的文献D. Zöbel等人理论计算机科学电子笔记133（2005）315325XML+DTD设置信息XML+DTD类图XML+DTDstatecharts基于Latex的Z-规范XML+DTD完全执行空间JazaZ-Interpreter执行空间产生程序测试和自动生成测试套件。然而，几乎所有这些文献的焦点都是通信协议，这些协议主要导致两个通信顺序系统的测试套件的推导。在实时系统的范围内，只有很少的科学工作是针对一致性测试（例如[14]和[1]）和基于规范的测试（例如[13]和[12与这些方法相反，可以从IUT中导出的信息关于协议执行的状态信息必须由实际运行的进程提供，该进程在争用某组临界区的某组进程的上下文中执行。在这种情况下，测试套件是一组特定的执行序列，作为IUT上的测试用例运行。一个基于测试套件的工具集是强大的，因为假设一个测试套件代表了一个等价类的计算的行为然而，可能的是，一个软件对于某个输入值n是容易出错的，并且对于值n和对于值>n工作良好。<这类错误不能通过这里使用的测试套件来捕获。 相反，我们寻找最低值n，其中一些代表性的执行过程是可能的，例如，为了证明优先级的间接继承，需要考虑3个过程。通过观察到测试套件根据3个过程的规范工作，给出了某种信心，即被测系统对于任何大于n的数字也工作良好。因此，所提出的测试套件仅保证在假设正确性与运行参数无关图五.执行空间生成器作为生成测试套件的初步步骤，必须确定和分析并行进程在这方面326D. Zöbel等人理论计算机科学电子笔记133（2005）315执行空间由争用临界区的进程的一组有限执行序列组成。这一步使用了两个主要组件：语法指导的执行空间生成器和用于Z规范的语义解释器 对于后者，Jaza解释器（参见[15]）对指定协议版本的Z模式进行操作。执行空间生成器构成了一个前端，以交互方式或批处理模式为Jaza解释器提供动画。设置信息描述了测试场景，包括过程及其优先级、关键部分以及类图、状态图和Z模式上的方案特定信息（见图5）。 例如，对于触发转换TRProcessT10的事件sigEnterCS，相应的Z-模式的序列由相应的状态图（跟踪图3和图4中的转换）：（mayEnterCSTRProcessT10）（TRUEERT12）（wantsCS）（TRUEERT13）（<$ceilingOK（15）（16）（下一页）（TRIBUTERT4）（hasPendingCSTRIBUTERT5）（delayedEnterCS）（TRQerT7）（TRQerT8）（TRProcessT7）由此，必须生成中间状态序列，该中间状态序列在对应于转换TRProcessT7的方法sigRun中结束。 对于测试套件的推导，只有起始状态和最终状态与记录哪个过程想要进入关键部分相关，并且由于协议的规则，可能选择了一些其他过程执行从验证某个IUT的角度来看，只有运行过程才能反映系统的状态。这种调度程序空闲且某个进程正在运行的状态称为可观察状态。它们非常重要，因为在这里，• 必须满足不变的PCPSystemInv，它是一组进程的断言，• 正在运行的进程可以输出其标识和其实际优先级因此，协议状态序列可以被压缩为与后续验证步骤真正相关的可观察状态除了对可观察状态的压缩之外，还可以应用执行空间的进一步减少。当一个进程在存在就绪进程的情况下准备就绪时，D. Zöbel等人理论计算机科学电子笔记133（2005）315327i=1JXML完全执行空间es-DTDXML可观察的执行空间减免政策XML可观测子空间XML+DTD可行路径减少执行空间产生程序可行路径生成器压缩都有更高的优先级。然而，这种减少并不能阻止对于每个示例，通过从n开始的该规则，可以将每个示例分解为多个示例。到n−1（n−i）！进程就绪的不同顺序（其中nisoughthen.（a）在任何情况下，对于任何顺序，其左侧为任何顺序具有Mj=0mj！可以订购m个临界截面的采集这些简单的计算揭示了可以生成执行空间即使在压缩和还原的情况下，也仅用于少量的过程和临界段需要制定额外的政策来定义观察重点。这样的焦点可以从一开始就可达到的某种状态开始，并不断发展。为了实现这个效果，需要执行空间生成器的反馈。作为最终结果，测试套件被导出，它是在这个减少的执行空间中所有可行路径的集合（在下一节中解释）（见图6）。见图6。 测试集328D. Zöbel等人理论计算机科学电子笔记133（2005）3154验证过程验证过程是顺序的，在测试套件的一个可行路径之后测试另一个可行路径。在此上下文中，可行路径由每个进程的执行序列组成，并通过以某种方式交错这些进程的意图来增强因此，任何进程都有一个特定的基本优先级和就绪时间。这里，例如，具有优先级12和相对就绪时间4的进程P2的执行序列最终请求临界段b3：：<进程名称=“p2”优先级=“12”><执行时间=“1”/><输入名称=“b”/><执行时间=“1”/><执行时间=“1”/><联系我们：上述执行序列的所有这些操作都是时间触发的，并被调度为持续一个时间单位。基于这种假设，在给定协议下执行的可行路径导致所有进程的唯一交错可行路径和测试用例都用XML表示，以便于可扩展性。为了说明测试用例的性质，下面是一个摘录，从过程P2在时间44开始：： execute time=“1”/>/exp> enter name=“b”/>/exp> execute time=“1”/>/exp> execute time=“1”/>/exp> enter name=“b”/>/exp>：注意，在时间6，进程P1继承了优先级12.相应的图形表示更加简洁和直观（见图7和图5）。为了更深入地研究PCP，让我们假设P1被指定为在临界段a和b上运行的过程。在特定的执行序列3交换格式es-DTD描述了一组特定进程和关键部分的执行空间（见图6）。4交换格式tc-DTD描述了由可行路径组成的测试用例（见图7）。5这些图表是自动生成的。它们指示运行的实际优先级-宁过程。由于进程之间的阻塞关系，这些优先级依赖于继承由于未成功获取临界截面而引入阻塞。为了使这一点明显，进入和离开操作是由上升和下降的矩形与内部的关键部分的名称来描述的。一个空心的、上升的矩形表示获取临界区不成功，并导致正在尝试的进程处于阻塞D. Zöbel等人理论计算机科学电子笔记133（2005）315329在测试中，P1不进入b。 但是，应符合PCP工艺 当试图进入临界区b时，必须阻塞p2.随后可以看到，PCP的现有实现产生了不同的测试用例，从而揭示了其不符合性。P3：P2：P1：10 10 101212 12 12 12 1001 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19图7.第一次会议。执行PCP规定的测试用例现在是时候专注于IUT了。通常，操作系统或运行时执行程序不处置标准操作进入和离开作为从测试用例调用。这些协议操作在IUT方面的仿真必须手动编码临界区也是因为必须创建进程。例如，对于Solaris，在PCP下请求的临界段必须通过系统调用pthread_mutexattr_setprioceiling（）并且初始化后可以用ptread互斥锁和ptread互斥解锁来代替enter和leave。此外，所有操作，如进入、离开和执行，必须以持续一个时间单位的时间触发方式在IUT上执行。 这个时间单位的持续时间必须至少调整到一个值，运行过程能够反映IUT的实际状态。在这里，决定性信息由进程标识及其继承的优先级组成。这些活动被称为仪器（见图8）。有时，IUT不提供系统调用来直接输出实际（继承的）优先级。在这种情况下，需要进一步的仪器和指示剂过程，延长验证过程。基于可行路径描述，IUT执行这些进程，并为它们的实际行为产生与Jaza解释器生成的一致行为相同的XML输出格式。这使得容易BB b14 14 14 1414BB1212B12 1212一一一330D. Zöbel等人理论计算机科学电子笔记133（2005）315XML可行的道提及模式插装测试用例XML符合测试用例tc-DTDXML真实测试用例提取器和仪器评价在IUT上运行见图8。验证过程检查违规行为。应用于操作系统Solaris，它假装实现PCP（以及PIP）的评估显示偏差。 可以看到（图7和图9）进程P2在很早的时候就被Solaris阻塞了。由于该协议对进程交错的限制比PCPSystemInv-不变量所要求的更强。这一观察导致了Solaris实现所谓的最高锁协议的假设。该协议属于PCP族，它是原始PCP在限制交织程度方面的简化。此版本的及时性计算必须考虑到具有中等优先级的进程被不必要地延迟。5结论本文介绍了一个复杂的工具集，用于一致性测试的PCP。特别是用于压缩和还原以及用于评估的组件到目前为止具有原型特征。尽管如此，已经有了一些引人注目的结果。上面使用Solaris作为IUT的协议或多或少代表了使用PCP作为有吸引力的标签并实现一些较弱协议的一般策略，这里是最高的锁协议。陷阱是，一般来说，应用程序程序员D. Zöbel等人理论计算机科学电子笔记133（2005）315331P3：P2：P1：10 10 12 1212 1212 12 1001 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19见图9。 Solaris作为IUT没有意识到这一事实及其对及时性计算的影响。更令人吃惊的是PIP的结果。一方面，到目前为止，没有一个测试过的操作系统符合PIP变体，它满足与PIP相关的所有定理（对应于原始文章[10]）。另一方面，在设计PIP的形式化描述时，原始协议的未检测到的错误已经被公开[19]。从这个意义上说，我们的工具集可以被认为是在需要信心的应用领域中实现更可信实施的一步。由于半自动化的验证过程的经验是，整个设置，仪器，测试套件生成和评估可以在两天内完成一个给定的操作系统或运行时执行。这表明：验证不一定昂贵。正如本文所解释的，该工具集具有复杂的结构和显著的自动化程度。需要几个中间文件。然而，只有两种DTD定义的数据格式（表示为es-DTD和tc-DTD）被使用。这强调了开源背后的理念，应该被理解为其他科学家提供改进组件的动画，并将此工具集用于验证协议反对优先级倒置。引用[1] B'eatriceB'erar d andLaur entFribur g.一个通用的、针对一个并行的、严格的程序的验证：ABR一致性协议。计算机辅助验证国际会议（CAV'99），第96-107页，意大利特伦托，1999年7月施普林格出版社[2] J. P. 鲍恩A.Fett和M.G. 欣奇ZUM在计算机科学讲义（LNCS）1493，柏林，德国，1998年9月斯普林格。B b14 14 14 1414B b12 12 14 1412一一一BB332D. Zöbel等人理论计算机科学电子笔记133（2005）315[3] P. A. Buhr，A.S. 哈里杰山口L. Lim和J.尘面向对象的实时并发。ACM SIG-THEORY NOTICES，35（10）：29[4] G. C. 布塔佐硬实时计算系统：可预测调度，算法和应用。Kluwer Academic Publishers，1997.[5] 布鲁诺·杜特尔特。优先级上限协议的形式化分析在IEEE实时系统研讨会（RTSS[6] C.M. Krishna和Kang G.阿信实时系统。麦格劳-希尔公司，纽约，1997年。[7] P. J. Moylan，R.E. Betz和R.H.米德尔顿优先继承权问题。技术报告EE9345，纽卡斯尔大学，1993年。[8] 迈克尔·皮林，艾伦·伯恩斯，凯瑞·雷蒙德.实时调度继承协议的形式规范。Software EngineeringJournal，5（5）：263[9] DavidPolock anddDiete rZéobel. Conformanc etestingoffpriorityinheritence nceproton g.我是丹妮尔·C。Young，编辑，第七届实时计算系统和应用国际会议论文集（RTCSAIEEE计算机协会。[10] Lui Sha，Ragunathan Rajkumar，and John P. Lejkuzky.优先级继承协议：一种实时同步的方法。IEEE Transactions on Computers，39（9）：1175[11] Alan C.肖 实时系统和软件。 John Wiley and Sons，纽约，2001年。[12] 亨德里克·塞恩安德斯·彼得森和汉斯·汉森。固定优先级调度实时系统的集成测试。Steve Liu IainBate，编辑，IEEE/IEE实时嵌入式系统研讨会，伦敦，2001年12月。[13] AndreeasUlrichanddHartmutKéonig. 基于空间的数据流分析系统。在IFIP联合国际会议上正式描述技术和协议规范，测试和验证（FORTE/PSTV[14] M. 你是我的儿子。在测试约束下生成可实现的成本测试。1998年10月在波士顿举行的98年军事通信会议[15] 联合Utting. Jaza用户手册和说明书。在线手册版本V0.86，怀卡托大学，2000年。[16] Ch. 维克里PC的实时和系统编程。McGraw-Hill，Blue Ridge Summit，PA，1993.[17] 马蒂亚斯·韦伯结合状态图和Z用于安全关键控制系统的设计。 在Marie-Claude Gaudel和JamesWoodcock，编辑，Industrial Benefits and Aavances in Formal Methods（FMESpringer-Verlag，1996年3月。[18] DieterZéobel and dWolfga n gAlbrecht. Echtzeitsysteme-GrundlagenundTechniken. Lehrbu ch. 国际汤姆森出版公司，波恩，奥尔巴尼，1995年。[19] DieterZüobell and dDavi d Polock. 在 此 之 前 ， 我 已 经 检 查 过 了 。 InJoéelGossens ， editor ，12thInternational Conference on Real-Time Systems（RTSBirp，11，rue du Perche，75003Paris.