自动验证Bossa操作系统进程管理器的安全性能调度策略的WS1S逻辑证明技术

理论计算机科学电子笔记185（2007）17-32www.elsevier.com/locate/entcs自动验证Bossa属性2Jean-Paul Bodeveixa MamounFilali a，Julia L. GillesMullerc/aIRIT，U iversit′ePaulSabatier，Toulouse，France丹麦哥本哈根大学cOBASCO Group，Ecole des Mines de Nantes-INRIA，LINA，Nantes，France摘要Bossa是一个操作系统进程管理器的开发环境，提供了许多安全保证。在本文中，我们将展示如何自动化检查的安全性能的调度策略，在这个环境中开发。 我们发现，大多数相关属性可以被认为是不变或细化属性。为了使相关的证明义务自动化，我们使用了WS1S逻辑，Mona为该逻辑实现了一个决策过程。使用FMona工具实现证明技术。保留字：调度，精化，模型检测，WS1S1介绍领域特定语言（DSL）是一种围绕与特定领域相关的精确构造和抽象而设计的语言[8]。这样的语言捕获领域的专业知识，指导程序员开发简洁，高层次的程序，并表示在共同的领域抽象。这项技术已经证明了它在研究和工业领域的各种领域中简化程序开发的价值[16]。除了减轻程序员的任务，DSL程序有可能是高度安全和高效的，因为语言可以被调优以简化验证和优化，并且因为验证和优化工具可以被调优以适应常见的领域习惯用法。然而，创建验证器或优化器1电子邮件：filali@irit.fr2这项工作得到了丹麦研究委员会（21-03-0545）的部分支持，以及法国研究和新技术部（Ministry of Researchand New Technologies）支持的“A CISr i t eInform a t ique e“项 目的 部分 支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.02618J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17对于一种编程语言来说，这仍然是一项艰巨的任务，在DSL的情况下，由于需要为每种新语言从头开始，这就更加复杂了。一个解决方案是建立在现有的通用验证和优化工具的基础上，但在这方面几乎没有经验。在本文中，我们通过介绍一个案例研究来帮助理解这一领域，该案例研究使用现有的验证工具来构建Bossa DSL的验证器，以实现操作系统（OS）进程验证器[17]。博萨进程调度是一个古老的问题，但没有一个单一的调度策略是完美的所有应用程序。事实上，在多媒体和嵌入式系统等领域日益苛刻的应用已经激发了许多新的调度算法[10，22，23]。由于这些算法在标准操作系统中不可用，因此需要特定调度策略的应用程序的开发人员必须在操作系统级别自行这是困难和容易出错的，需要目标操作系统的大量专业知识。为了解决这个问题，我们开发了Bossa环境来开发操作系统进程管理器[17]。Bossa提供了两种DSL：一种用于描述给定OS的调度要求的规范语言和一种用于实现调度策略的编程语言这两种语言都是专用于调度域的抽象语言，允许以高级和自然的方式描述操作系统调度行为和调度策略。Bossa已被移植到Linux和Chorus[12]，并已用于研究[9]和教学。”[14]《易经》中有一个很好的解释，就是“君子之道，焉可诬也？有始有卒者，其惟圣人乎验证器使用抽象解释来检查操作系统调度要求的规范是否一致，以及Bossa调度策略是否满足指定的要求。验证确保调度策略仅将那些能够运行的进程视为有资格执行。还检查其他一些属性，例如是否存在空指针取消引用。这些检查确保Bossa调度程序不会崩溃或挂起操作系统。其他属性，如公平性和活跃度，可以考虑，但我们选择专注于与操作系统交互相关的属性，因为这些通常超出了调度算法设计者的专业知识范围，因此非常适合DSL封装专业知识的目标。本文由于Bossa验证器是手工制作的，并且混合了相关属性的编码和检查，我们发现它很难维护，特别是在扩展Bossa编程语言时。因此，我们有兴趣使用现有的验证引擎实现Bossa验证。以前[5]，我们已经研究了如何在B [1]形式方法中考虑Bossa方法。这项研究表明，Bossa所做的一些验证可以表示为B不变量或精化的证明义务。然而，这些证明义务中的大多数并没有被工作室B [7]中可用的证明器自动履行：工作室B[ 7 ]是一种支持基于细化的B开发方法[1]的工具。原因包括缺乏合适的决策过程和抽象生成器，特别是考虑到J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1719由博萨政策操纵的过程是无限的。因此，我们需要一种能够以自然的方式表达Bossa属性的逻辑，以便于扩展到新的功能，以及一个能够为这种逻辑提供决策过程的验证引擎。在本文中，我们通过FMona工具[4]的接口证明了WS1S逻辑非常适合表达Bossa代码和属性。WS1S的决策过程由Mona验证工具提供[13]。因此，我们可以自动验证我们之前工作中考虑的所有属性，并涵盖Bossa验证器考虑的其他属性。本文的其余部分组织如下。第2节概述了Bossa，并更详细地介绍了相关第3节介绍了我们使用的工具和技术。第4节考虑了操作系统要求规范的验证。第5节介绍了调度策略的表达及其与操作系统要求规范相关的验证第6节考虑了我们使用的验证方法与其他一些第7节总结并提出了一些未来的工作。2果壳中的博萨在本节中，我们将概述Bossa DSL，然后考虑在显示Bossa调度策略满足特定条件时出现2.1用于编程调度策略的Bossa DSL进程调度程序是操作系统的一部分，负责选举进程以访问CPU。要做到这一点，它必须跟踪有资格进行选举的进程集，并有办法选举其中之一调度策略描述了调度程序在这些操作中所采取的策略。因此，这些操作是Bossa DSL提供的用于编程调度策略的构造和抽象的焦点。单调速率（RM）[15]是一种调度策略，常用于管理实时系统中的周期性进程。当一个进程应该被选择来访问CPU时，这个策略会选择周期最短的合格进程。图1显示了这个调度策略的Bossa实现的摘录。该实现声明了流程属性（第2行）、流程状态（第3-10行）、排序标准（第11行）和事件处理程序（第12-30行）。流程属性记录了每个流程的策略特定信息。在RM策略中，这包括流程的周期。仅为基于优先级的策略提供的排序标准指定了进程的相对优先级在RM策略中我们将在本节的其余部分描述流程状态和事件处理程序。RM策略定义了六种进程状态：运行、就绪、屈服、阻塞、计算结束和终止。由策略管理的进程始终处于这些状态之一。每个进程状态都与一个状态类相关联，20J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17它描述了状态中进程的资格。状态类如下：• RUNNING：活动进程（单处理器上最多一个• 准备：有资格当选的进程，• KERNELBLOCKED：由于最近与操作系统的交互而不合格的进程（例如，I/O请求• POLICYBLOCKED：由于最近与调度程序的交互而不合格的进程（例如，量子过期），• KERNEL POLICY BLOCKED：由于最近与OS和调度程序的交互而不合格的进程• 已终止：已终止的进程策略可以在每个状态类中定义多个状态，以表达策略所需的进一步细化。例如，RM策略在READY状态类中定义就绪和屈服状态，以区分无条件准备运行的进程（就绪）和只有在没有其他进程可用时才应该运行的进程（屈服）。最后，一个数据结构与每个状态相关联：一个进程变量代表一个状态，它最多可以包含一个进程，或者一个队列代表一个状态，它可以包含任意数量的进程。事件处理程序描述调度策略如何对检查进程资格的各种操作系统事件作出反应。示例包括使进程不合格的进程阻塞和使进程再次合格的进程解除阻塞。必须处理的事件集特定于目标操作系统。对于Linux 2.4，策略必须为10个事件提供处理程序。我们详细描述了unblock.preemptive处理程序（第14-19行），因为它说明了大多数语言结构。如果需要，当进程解除阻塞并且操作系统允许调度策略抢占正在运行的进程时，将触发此处理程序。 处理程序操纵进程e.target，该进程是这就是开放。它首先检查此进程当前是否被阻止（e.targetinblocked，line 17）. 如果是，处理程序将解除阻塞进程的状态更改为就绪（第18行），然后检查是否应该抢占正在运行的进程（第19行）。 对于后者，它测试是否有正在运行的进程（！empty（running））以及解除阻塞进程的优先级是否大于正在运行的进程的优先级（e.target> running）。 如果这两个条件都满足，那么正在运行的进程的状态将更改为就绪，请求抢占它。该语言还提供了整数和时间的操作，队列上的循环等。它不提供无限循环或递归函数。2.2用于指定操作系统调度要求的Bossa DSL调度策略必须在最低级别与目标操作系统交互。在这个级别上，操作系统差异很大，因此调度策略的定义必须针对目标操作系统进行调整。因此，事件处理程序集、其J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1721调度程序RM={1process={timeperiod;cycleswcet;timerperiod timer;intmissed deadlines;}2状态={3RUNNING运行：进程; 4READY就绪：选择队列; 5READY成品率：过程; 6KERNEL BLOCKED阻塞：队列; 7POLICY BLOCKED计算结束：队列; 8终止; 9}10排序标准={最低周期}11handler（event e）{12/* 事件块。*： e. 目标区块*/13在街区。* {e. target=>blocked;}14/* 事件解除阻塞。先发制人的：e. 目标解锁*/15开启解锁。抢占式{16如果（e. 目标被阻塞）{17e. target=>ready; 18if（（！空（运行））（e. target>running））{running=>ready;}192021/* 事件收益率。用户名 *： e. 目标希望屈服于任何符合条件的进程*/22投降。用户名 * {e. target=>yield;}23/* 事件bossa。附表：e. 目标操作系统请求进程选择*/24在博萨。时间表{25if（empty（ready））{yield=>ready;}select（）=>running; 27如果（！empty（yield））{yield=>ready;}282930interface={.. .31Fig. 1. Bossa Rate Monotonic调度策略行为，以及它们之间可能的交互不是固定的，而是由操作系统进程管理行为的专家为每个操作系统指定的此规范由一组事件类型和一个事件自动机组成。事件类型描述了所需的事件处理程序集及其行为要求。后者是根据相关过程状态的前提条件和后条件来指定的，例如生成事件的过程（源）或事件所关联的过程（目标）。每个事件类型规则描述了在事件生成时可能发生的进程到状态的映射，以及在事件处理程序完成时允许的进程到状态的映射集。具体化是用状态类来表示的，与策略无关。 作为一个例子，对块的要求。* 处理程序可表述如下：block.* ：[tgt inRUNNING]->[tgt inKERNEL_BLOCKED]此规则指定当进程（tgt）阻塞时，它必须处于RUNNING状态类的状态，并且处理程序必须将阻塞进程置于KERNEL BLOCKED状态类的状态，以记录该进程不合格。这条规则，然而，这不足以捕获在例如Linux 2.4中可能发生的调度器和OS之间的可能交互附录介绍了更复杂的Linux 2.4块。* 事件类型。事件自动机描述操作系统生成事件的序列。22J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17各种事件。例如，在Linux 2.4中，要终止一个进程，操作系统首先阻止终止进程，然后选择其他进程，最后生成一个process.end事件来从调度程序中删除该进程。 有些序列是不可中断的;例如，Linux2.4总是在阻塞一个进程后立即请求选举一个新进程，在阻塞和重新启动之间不可能有中断。他们对于可中断序列，操作系统专家还提供有关中断期间可能发生哪些事件的信息。Bossa事件类型编译器在任何可中断序列中的每一步都使用这些事件的所有排列来增强事件自动机。2.3Bossa验证问题Bossa验证器对操作系统规范和调度策略应用各种一致性检查。我们在下面描述这些检查。对于操作系统规范，主要目标是确保事件类型一致。Bossa区分了上下文敏感事件和自动事件。只有当过程到状态的映射满足相应事件类型的先决条件时，才会一个例子是解除阻塞，它起源于OS级别，其中进程状态是已知的。在这种情况下没有一致性要求无论当前进程到状态的映射如何，都会发生自动事件一个例子是阻塞，它来自于用户级别的操作，其中流程状态是未知的。一致性要求事件类型为每个进程到状态的映射指定至少一个允许的行为，这些映射在事件发生时可以保持。为了检查这一点，验证器考虑事件自动机指定的所有可能的事件序列，以及事件类型规则指定的沿着这些序列的事件的所有可能的影响对于策略，主要目标是确保事件处理程序定义良好（例如，没有空指针解引用）并且它们尊重事件类型。在这种情况下，验证器使用根据策略定义的状态实例化的事件类型和事件自动机来识别处理程序间的事件。对于事件类型所允许的并且根据事件自动机可到达的每个进程到状态的映射，验证器分析通过事件处理程序的每个执行路径，以确定对进程状态的影响。由此产生的进程到状态的映射必须与事件类型规则指定的后置条件兼容。这部分验证器已在之前详细介绍[14]。这两种形式的验证都依赖于对所有可能的执行路径的分析，这表明模型检查是合适的。然而，标准的模型检查技术仅限于有限状态空间。 在Bossa的情况下，状态空间的大小由过程的数量决定，通常没有边界。因此，我们转向Mona工具[13]，它能够在存在未知整数值的情况下进行推理。J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17233Mona验证工具我们首先回顾Mona工具[13]，然后描述在此设置中的转换系统，3.1MonaMona为逻辑WS1S实现了一个决策过程，定义如下：定义1（WS 1 S逻辑）令{x1，. ，xn}是一阶变量的集合，并且{X1，. ，Xn}是二阶变量的集合。WS1S逻辑的最小语法如下：• 项t定义为：t：：= 0 |Xi|s（t），其中s是后继符号。• 公式f定义为：f：：=t∈Xi|f|ff|2001年， F|202Xi. f（第一次和第二次或第三次定义）一个封闭公式是WS1S有效的，如果它在自然数集合N上的解释是有效的一阶变量表示自然数，二阶变量表示N的有限子集。逻辑是可判定的。为了表示与Bossa相关的属性，我们使用Mona的FMona [4]高级这个接口允许声明枚举类型，更新记录，对有限结构化类型的量化，以及参数化高阶宏。FMona代码会自动翻译成Mona。作为一个例子，我们考虑一个类似于叠加的概念的定义[6]。我们假设我们有一个自动机，其状态由Location类型标识，以及数据类型Data上的关系树。 的叠加过渡的tr是一种新的关系，它定义在“叠加”类型上，record{d：Data;w：位置;}如下：pred superpose（type Data，type Location，pred（var Datad，var Location l，s.w=ls'.可以部分应用。例如，如果l1和l2是位置，则superpose（tr，l1，l2）是叠加类型对上的谓词。类型参数自动合成。3.2跃迁系统和性质我们定义一个转换系统为一个三元组，由一个状态空间，一个初始化谓词和一个二元转换关系组成在我们的例子中，系统由进程的数量参数化。 Mona甚至可以分析这些系统的性质，如果参数还没有被实例化，这是Mona在我们的上下文中相对于传统模型检查的本质优势。在本文中，我们认为安全性表示为不变量。遵循Mona术语，我们不区分属性和谓词。定义2（不变量）一个谓词P被称为相对于一个24J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17转移系统，如果它在转移系统的初始状态下为真不变性属性依赖于稳定性，不考虑实际执行。当不变性不能成立时，我们可以考虑一个较弱的性质：谓词总是真[19]，即，满足于所有可达到的状态。定义3（总是真谓词）一个状态s对于一个转移系统S来说是可达的，如果存在一个序列s0，. ，Sn= S，使得s0是S的初始状态，并且对于每个i （sJ，sJ）<$sc→csJA C C A C迭代技术的实现。我们感兴趣的大多数时间属性都可以表示为固定点[2]。但是，既然我们这样做J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1725对于到达不动点没有一般的可判定性结果，我们必须提供到达它所需的迭代次数的界限。宏向后由迭代次数N参数化，转换系统由谓词init和tr以及验证inv的谓词定义。从一个以inv的否定为特征的状态开始，在转换关系的逆的n次迭代（通过递归宏函数）之后，我们检查实际上已经到达了一个固定点（通过稳定谓词），而没有到达任何初始状态。通过这种方式，我们验证了初始状态和满足以下条件的状态之间的路径inv不存在。pred backward（type S，var nat N，pred（varSs）init，pred（varSs，bwd（init，tr，n（N，NOT（inv），inverse（tr）;pred（type S，var natN，pred（varSs）start，pred（varS s，ifN= 0 thenstart（s）else exSs'：<$（N-1，start，tr，s'）<$（s' = s| tr（s'，s））endif; pred check bwd（type S，pred（var S s）init，pred（var S s，s'）tr，pred（var Ss）bad）=stable（bad，inverse（tr））所有Ss：bad（s）错误初始化（s）4使用Mona我们现在介绍事件类型和事件自动机到FMona的转换，以及它们的一些属性是如何表达的这些性质包括表示不变量和系统中进程数的保持，事件类型和事件自动机的翻译已经自动化。Mona会自动检查任意数量进程的属性。4.1事件类型的翻译我们用一组与之相关的进程来表示Bossa状态类然后，系统的状态由记录Classes表示，其中每个字段表示一个状态类。附加的状态类NOWHERE表示不受调度程序管理的进程。var natNproc;#最大进程数typeProc =. NProc;#interval type：0.. NProc-1type Classes=record{RUNNING ， READY ， KERNEL BLOCKED ， POLICY BLOCKED ， KERNEL POLICYBLOCKED，EXPLAYATED，NOWHERE：Proc;}的集合;我们用一个“before-after”谓词来表示与给定事件关联的事件类型，该谓词是与各种类型规则关联的关系的析取。例如，如果block.* 有单一类型规则：block.* ：[tgt inRUNNING]-> [tgt inKERNEL BLOCKED]则会自动生成以下谓词：• Eblock，定义Classes类型元素之间的前后关系，由源（src）和目标（tgt）进程参数化。 （block.* 没有源进程，但转换类型的签名都是相同的，为简单起见。）pred Eblock（varProcsrc，tgt，var Classes s，（（{tgt}}运行中）运行（sRUNNING：=s.RUNNING\{tgt};READY：=s.READY\{tgt};KERNELBLOCKED：=s.KERNELBLOCKED\{tgt} 运 行{tgt};}） ） ; 策 略 阻 止 ： =s. 策 略 阻 止\{tgt};26J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17KERNEL POLICY BLOCKED：= s.KERNEL POLICY BLOCKED\{tgt};删除：=s.删除\{tgt};NOWHERE：= s.NOWHERE\{tgt};为了简化FMona代码生成，规则左侧发生的进程总是从每个状态类中减去。这种方法主要在左手边包含过滤器的析取时有用，因为这样就没有必要单独检查它们。FMona代码是冗长的，但不需要简化，因为Mona为所有等价公式生成一个等价的基于自动机的内部表示。• block，它是src和tgt的任何可能值的转换Eblock的析取。pred block（var Classes s，4.2事件内属性的验证事件类型不应允许调度策略将一个进程置于多个状态、将多个进程置于RUNNING状态类的状态或删除进程。这些属性直接编码为不变属性或状态表达式的保留4.3事件间属性的验证事件的顺序由Bossa事件自动机描述。在这个自动机中，Bossa区分自动事件和上下文敏感事件。事件类型必须被构造成使得在自动机中出现自动事件的每一点处为了检验这个性质，我们必须考虑系统的完整动力学这由事件自动机、事件类型和系统状态（类）的组合来表示，以描述每个事件前后进程到状态类的映射由此产生的转换关系在状态空间NClasses上定义：type Location =. 12; #自动机状态type NClasses=record{d：Classes; w：Location;};转换关系本身NNext是通过叠加描述事件类型（块等）的关系来定义的到事件自动机中的转换。事件类型的表示的分离发生在-中断被叠加到表示事件序列中的可中断点的自动机状态。其余类型规则的表示被叠加到相应的自动机转换。pred interrupts（var Classes s，s'）=#中断事件解除阻塞抢占（s，s '）|解除阻止计时器目标（s，s '）|......;predNNext（var NClasses s，s'）=#自动机变迁的事件叠加（中断，2，2，s，s '）|叠加（中断，4，4，s，s '）|. . . ...这是什么？|superpose（block，0，1，s，s '）|叠加（bossa schedule，1，4，s，s'）|......;我们的目标是检查系统的每个可达状态是否满足预先定义的条件。J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1727从该状态允许的自动事件的条件。然而，计算系统的可达状态一般不能自动化，因为状态空间是由进程的数量参数化的因此，我们使用状态空间的有限抽象，其中布尔值与每个类相关联，指示类是否为空（假值）type AClass=record{RUNNING，READY，KERNEL BLOCKED，POLICY BLOCKED，KERNEL POLICYBLOCKED，NOWHERE：bool;}此类型由自动机的状态位置扩展typeNAClasses=record{d：AClasses; w：Location;};类的状态空间和它的抽象ABlasses之间的抽象关系包含表示不变量inv（4.2）和每个布尔域的定义pred state abs（var Classess，var AClasses a）=投资者（a.RUNNING参与.RUNNING））（a.KERNEL BLOCKED Particles.KERNELBLOCKED（a.POLICYBLOCKEDParticles.POLICY BLOCKED））（a.KERNELPOLICYBLOCKED参与者.KERNELPOLICYBLOCKED参与者）（a. AQUATEDPARTIES. AQUATED/=）（a.NOWHEREPARTIES.NOWHERE/=）;谓词nabs将抽象关系扩展到叠加自动机的状态空间。它接受一个NClasses类型的具体值和一个NAClasses类型的抽象值作为参数，并将状态位置映射到它们自己，并将附加到每个类的进程集抽象为布尔值。pred nabs（varNClassesc，varNClassesa）=c.w=a.wstate abs（c.d，a.d）;先决条件的满足现在可以在抽象层次上表达：抽象状态的每个具体对应物必须满足自动事件的先决条件。 我们首先介绍了一个谓词检查前的具体状态，类型NClasses，断言au-目前的状态下，华为是满意的。 抽象级谓词检查（varNAClassesa）表示a到nabs的所有具体化都满足检查pre。对抽象系统的向后分析，在一个步骤后终止于此，在每个可达抽象状态上验证这个属性，从而在可达具体状态的超集上验证这个属性。 给定宏AInit和ANext，计算具体系统的初始化和转换关系的抽象，通过以下断言检查属性：backward（1，ANext（NNext，nabs），AInit（NInit，nabs），check）;言论• 这项研究揭示了Bossa事件类型描述的Linux内核行为抽象中的一个错误。Bossa工具执行的分析没有检测到错误，因为它执行的分析不太准确：它考虑使用三个值（空，非空，未知）对状态类进行抽象，并且不对未知状态进行验证。• 即使在理论上可以计算可达系统的可达状态集这就是为什么我们28J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17已经应用了迭代方法。然而，它的收敛性是有保证的，因为抽象状态空间是有限的，即使转换是由进程的数量参数化的。• 这里执行的分析相当于模型检查，但由于状态空间NAClasses上的转换关系是参数化的，因此有限状态模型检查器并不直接适用。使用有限状态模型检查器需要程序转换，这通常很难验证。在我们的建议中，抽象是在语义层面上指定的。该方法的正确性依赖于一个简单的元级定理。5使用Mona的我们现在展示如何将Bossa配置策略（见图1）定义的进程状态和事件处理程序转换为FMona，以及如何验证它们与事件类型的一致性。5.1进程状态和事件处理程序的Bossa规范进程状态声明被自动转换为FMona作为一个类型decompress，它将每个状态与一组进程相关联，以及一个与状态和类相关的胶合不变量。这个粘合不变式还包括一个状态的表示不变式，它建立在状态类的表示不变式的基础上：typeBstates=record{running：Proc集; ready：proc集; yield：Proc集;blocked：Proc集;计算结束：过程集;终止：过程集;}的情况;pred Bstates 2Classes（var Bstates c，var Classes a）=inv（a）表示不变量a.运行=c.运行a.READY=c. ready准备就绪产量=a.KERNEL BLOCKED=c.阻塞a.POLICYBLOCKED=c.计算结束a.内核策略阻塞=a.终止=c.终止;事件处理程序到FMona的转换依赖于Bossa语句上的最弱前提演算。不能转换为FMona的子表达式的抽象（算术表达式等）也被执行。状态更新和空检查被保留。Bossa事件处理程序可以部分定义。例如，只有在状态为空时，才允许将进程置于指定为进程变量的状态。为了保证事件处理程序的格式良好，在这种情况下会生成先决条件例如，在下面的处理程序中，由于状态yield是作为变量实现的（参见图1，第6行），因此只有当yield为空时，到yield关于yield.user。* {e.target=>yield;}FMonatranationhinclinc我们将证明这不可能发生。predByield系统暂停（varProcsrc，tgt，varBstates s，（（s.yield=）J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1729（s5.2保险单的核实我们现在展示如何使用FMona来表示策略与事件类型。此属性基于Classes类型上的转换（称为抽象转换）与Bstates类型，据说是具体的。 它相当于实例化事件类型规则，这些规则是根据状态类定义的，相对于由给定策略定义的状态。预处理转换的泛型精化属性（这里使用）被实例化并表示为具体类型上的谓词：predcheckref（type State c，type Statea，pred（var Statecs c，var Stateasa），pred（var Statecs c，spred（var State a s a，s（all State c s（trc（s c，sex State a s所有状态c s c：所有状态a s a：（（s c，s a）pre（tr a，s a））int n =nums（nums）;然而，这种细化属性通常是无效的。例如，只有当屈服状态为空时，才可能向屈服状态过渡。由于事件类型不要求关联的状态类READY为空，因此没有细化。因此，我们必须考虑自动机允许的执行，并且只检查给定抽象可达的Bstates类型的具体状态的精化。这种抽象是通过用布尔值表示每个状态来获得的，如果状态不为空，则为true。具体的和抽象的状态叠加到自动机的状态上。然后，对可达抽象状态的所有具体对应物验证精化属性。只考虑从给定状态的允许转换。在我们的例子中，收敛后，得到三个抽象的过渡向后应用。一般来说，迭代方法的收敛性是可以保证的，因为抽象状态空间是有限的。然而，状态空间的大小可以比所需的迭代次数大得多（640对（3）在RM策略中6相关工作在本文中，我们使用WS1S逻辑和Mona自动证明了Bossa调度器的属性。值得注意的是，尽管这种逻辑的最坏情况复杂度是非基本的，但所考虑的调度结构所需的计算似乎是可行的。这证实了其他领域的结果，例如数据结构的静态分析[11]和软件结构[21]。其他方法和证明技术也可以使用。关于方法，我们提到B方法，我们在以前的研究中使用过[5]。从来没有-30J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）17然而，这里提出的方法需要一些B不支持的特性，即考虑事件自动机和抽象的使用。我们对这些特性的使用拓宽了可以表达的属性集，同时保留在WS1S逻辑中。这反过来又使举证义务得以自动履行。关于证明技术，国家可以用计数器来表示。因为Mona实现了Presburger算法，所以Mona可以被使用。然而，像FAST [3]这样专门用于算术的工具应该更有效.WS1S逻辑的使用允许我们避免将集合抽象为计数器。也可以使用Petri网[20]。虽然在这种情况下计数器的使用受到限制，但应该可以精心制作模型。在这两种情况下，所考虑的属性不能自动决定，需要进行抽象或应用收敛加速。7结论在本文中，我们展示了如何使用Mona来检查之前由特定工具检查的Bossa属性。这种方法将证明义务的生成（仍然是Bossa特有的）与相关证明的构建（由通用工具执行）分开。 由于证明义务的生成比证明构造简单得多，这种方法应该更容易随着语言需求的发展而扩展和修改Bossa veri fier。扩展还可以透明地使用Bossa验证器中没有内置的自动证明器的功能，例如整数推理。尽管如此，尽管本研究考虑了Bossa验证器检查的安全属性，但它没有解决Bossa编译器用于生成优化代码的一些属性。为此，需要Bossa和FMona之间更强的耦合。使用通用验证器似乎可能不如专用于Bossa的验证器有效尽管如此，已经有大量的研究致力于提高通用证明器的效率，这超出了为特定领域语言开发工具的典型可用性。在实践中，我们观察到我们的方法与Bossa验证器具有相同的性能，大约一分钟即可验证典型的调度策略。特别是，我们使用迭代技术，避免了二阶量化，大大提高了执行时间和内存使用。Bossa验证器检查与操作系统的调度要求相关的属性。使用我们的方法，现在还可以考虑与调度算法和调度应用程序相关的例如，调度器的实现是否在给定的调度程序下，应用程序是否会在截止日期前完成？最后，可以考虑生成认证代码以及证明注释代码[18]。空房的 Bossa可在http://www.emn.fr/x-info/bossa/上获得。J. - P. Bodeveix等人/理论计算机科学电子笔记185（2007）1731引用[1] J. - R.阿布里尔 B-Book：将程序转换为意义。 剑桥大学出版社，1996年。[2] A.阿诺德有限迁移系统Prentice-Hall，1994年。[3] S. Bardin ，A.Finkel，J.Leroux 和L.彼得鲁奇FAST ：符号转换系统的快速加速在Proc.15th Conf.Computer Aided Verification（CAVSpringer，2003年。[4] J. - P. Bodeveix和M.菲拉利一个通用的工具，用于表达验证的发展。 在1999年10月6日至8日在乌普萨拉大学举行的第11届北欧编程理论研讨会NWPT比约恩·维克多和王毅。[5] J. - P. Bodeveix，M. Filali，J. Lawall，and G.监听器手机监听器形式化方法满足领域特定语言。在第五届综合形式方法国际会议（IFM），荷兰埃因霍温，LNCS第3771卷，第187-206页[6] K. Chandy和J. Misra。 并行程序设计基础。Addison-Wesley，1988年。[7] 很清楚。拉特利亚湾版本3.6。技术报告，http://www.atelierb.societe.com/。[8] C. Consel和R. Marlet 使用语言开发的方法体系结构软件。在C. Palamidessi，H. Glaser和K. Meinke，编辑，第10届编程语言实现和逻辑编程国际研讨