基于模式的实时转台系统的形式化建模和分析案例研究 - 实时嵌入式系统的组件化设计

理论计算机科学电子笔记253（2009）161-178www.elsevier.com/locate/entcs基于模式的实时转台系统Davor Slutej1创新、设计和工程学院Müalardalenuniversity，Vêasterévas，SwedenJohnHakanson2乌普萨拉大学信息技术系瑞典乌普萨拉Jagadish Suryadevara，Cristina Seceleanu，Paul Pettersson3M？alardalenReal-TimeResearcCentre，M？alardal enUniversity，Vêasterévas，Sweden摘要工业实时系统的设计者通常面临着复杂系统建模和分析的问题，即使采用基于组件的设计范式。在本文中，我们提出了一个转台系统的形式化建模和分析的案例研究，其中的组件是描述的SaveCCM语言。我们的实时系统的内部结构的基本原则的搜索，促使我们提出了三种建模模式的实时组件，可以在适当的设计环境中实例化的共同行为。这种可重用模式的好处在案例研究中显示，通过允许我们为转台系统的实时组件生成易于阅读和管理的模型。此外，我们相信，模式可能铺平了道路，以通用的模式为基础的建模框架，特别是针对实时系统。关键词：组件，实时，嵌入式系统，规范，验证，建模模式，案例研究1介绍开发工业实时系统是困难的，并对系统的安全性和可靠性提出了很高的要求。短的开发周期需要可靠的环境，1 电子邮件地址：davor@slutej.com2电子邮件：johnh@it.uu.se3 电子邮件：paul. mdh.se，jagadish. mdh.se，cristina. mdh.se1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.034162D. Slutej等人/理论计算机科学电子笔记253（2009）161成本可预测的方法。最先进的技术是由一个特设的混合方法和工具，系统验证主要是在实现层面上进行广泛的测试。然而，在设计过程中，测试已经做得太晚了，即使在经过良好测试的模型中，bug也可能仍然存在。在这种情况下，在设计过程中管理复杂性和确保关键系统属性的技术成为必要。一种有前途的设计方法是采用正式的基于组件的开发技术。在这种方法中，组件被引入为可部署到系统中的可执行软件单元实现基于组件的软件范例的关键问题之一这个问题的一个潜在的解决方案是正式的模块化验证，基于组件的软件通过模型检查。在本文中，我们提出了一个案例研究的形式化建模和分析的实时，基于组件的转台系统，其中的组件是描述在SaveCCM语言[8]。为了进行验证，我们使用SaveCCM的集成开发环境，通过带有UPPAAL端口的插件连接，U ppaal端口是模型检查器UPPAAL的扩展，它实现了部分降阶技术[10] 有效的模型检查。该技术利用了组件网络的拓扑结构，从而提高了验证方法的可扩展性我们在这个案例研究和其他类似例子中的经验是，除了使模型检查有效之外，一个要求很高的任务是为组件及其组成产生可管理和易于掌握的设计模型。这促使我们尝试提取一些在实时系统设计中经常出现的常见行为模式，并将其表示为类似于有限状态机的符号。 这种表示法使我们能够在高层次上应用这些模式 的软件开发，如在文件中所示，同时简化生产模型。我们相信，在设计基于组件的系统时采用模式也可能有助于通过基于模式的重新设计来记录相关的软件。诗工程。 然而，这超出了本文的范围。通用程序设计模式在面向对象设计社区中已经广为人知了一段时间[9]。然而，在基于组件的实时系统的设计中，一些不同的方面可能需要在建模模式中表示;例如，我们的SaveCCM组件的语义是读-执行-写语义，因此运行到完成模式可以证明在设计中是有益的。类似地，在组件执行期间对访问状态序列的可重用建模，或者通过提供系统的方法将截止日期与行为相关联来减少实时组件行为的时间方面的非确定性，通过模式，也可以在建模阶段帮助设计者。在本文中，我们介绍了刚才提到的抽象的常见实时组件的行为，运行到完成，历史，和执行时模式，分别。接下来，我们将它们应用于基于组件的转台生产单元建模本文的其余部分组织如下。在第二节中，我们简要回顾了D. Slutej等人/理论计算机科学电子笔记253（2009）161163p1p3p4Cp2B一（一）l0y≤Ty=Ty ：= 0l1y ≤JLf（b）第（1）款z：= 0l0z ≤Maxz≥最小值a：= 1−aLf（c）第（1）款图1.（a）通过连接端口p1到p3和p2到p4组成组件A、B和C的组合的示例，以及定时行为：（b）具有周期T和抖动J的时钟，（c）在Min和Max时间单位之间的计算更新数据变量a在我们的案例研究中，SaveCCM语言用于组件建模的基础知识在第3节中，我们介绍了三种建模模式，并将其描述为有限状态机，之后，我们将在第3节中介绍实时转台生产单元示例，包括组成组件的正式模型4.系统 我们比较我们的方法，相关的，在部分5. 最后，第6节总结了本文件，并概述了今后工作的可能方向。2SaveCCM在本节中，我们简要介绍了Save组件建模语言[8]，它将用于本文的案例研究。该语言是一个更大的框架的一部分，称为SaveCCM，用于实时和嵌入式系统的基于组件的设计[1]。SaveCCM语言由图形语法和相关的形式语义组成。由于篇幅限制，本节仅对SaveCCM进行简短的非正式概述。对于语言的完整描述，我们请读者参考[8]。在SaveCCM中，系统由相互连接的组件构建，具有由输入和输出端口组成的定义明确的接口。通信风格基于管道和过滤器范式，但数据传输和控制流程明确分离。前者由数据端口之间的连接捕获，其中可以写入和读取给定类型的数据，后者由控制组件激活的触发器端口捕获图1（a）示出了图形SaveCCM符号。三角形和方框分别表示触发端口和数据端口。组件保持被动，直到所有输入触发端口都被激活，此时它首先读取所有输入数据端口，然后对该输入和内部状态执行相关计算。在此之后，组件写入其输出数据端口，激活输出触发器端口，并再次返回到被动状态。这种严格的通过将输出端口连接到其他组件的输入端口，除了这个164D. Slutej等人/理论计算机科学电子笔记253（2009）161组合，可以通过将互连组件的集合放置在封闭组件内来分层地组合组件。从外部看，这样的复合组件与行为由单个模型或代码片段给出的其他组件是无法区分的为了支持SaveCCM模型的分析，需要将每个组件与行为模型相关联，该行为模型由具有不同出口位置的时间自动机[3]组成（参见图1（b-c）），以及组件数据端口和内部自动机变量之间的映射。当一个组件被触发时，端口值被复制到定时行为的内部变量，然后按照定时自动机中的指定进行。每当它到达出口位置时，变量值就会根据给定的映射复制到输出端口，并且输出触发器端口被激活。SaveCCM中使用的时间自动机建模语言基于局域网，用于U PPAAL工具[16]。它扩展了时间自动机语言它最初是由Alberr和Dill [3]引入的，具有许多将在案例研究中使用的功能，包括：全局和局部有界整数变量以及对这些变量的算术运算，数组，以及一种小型C类编程语言，可用于定义函数和谓词。对于时间自动机语言的详细描述，我们请读者参考[5]。3组件建模模式建模模式是一种设计具有明确意图的模型的方法和结构。在这一节中，我们提出了三种建模模式的实时组件的常见行为，以最终提供设计人员有用的抽象机制，为高层次的建模和分析的CB实时系统。我们选择用一种类似有限状态机（FSM）的符号来定义模式，在本文中我们称之为模式FSM（或PFSM）。这些模式可以在特定的正式框架中单独或组合地实例化，以增加模型的可读性及其对验证的适用性。为了证明我们的主张，在第4节中，我们将所提出的模式作为组合应用于工业实时转台系统的CB建模（例如，参见图10）。分析框架是UPPAAL[5，16]的时间自动机（TA）语言通用PFSM定义和图形符号。设V是一组数据变量，G是V上的一组布尔条件（守卫），A是一组更新变量的动作。然后PFSM是一个元组S，start，exit，E，Att，其中S是一组状态，start是进入状态，exit是退出状态，E是状态之间的转换集合，Att是一组定时属性，例如执行时间，最后期限等。PFSM的执行在特殊控制状态开始时开始。在一个给定的状态下，一个传出的转换只有在其相关的保护评估为true时才能被执行;在这种情况下，我们说转换被启用。在启用多个传出转换的情况下，可以非确定性地执行一个实心圆表示开始控制状态，半实心圆表示退出控制状态D. Slutej等人/理论计算机科学电子笔记253（2009）161165图2. 组件行为x==3 update（）开始出口图3.一种具有Run-to-Completion模式的等价时间自动机模型状态（参见图2）。PFSM的不同属性，例如执行时间，截止日期等，可以添加到PFSM模型的图形表示中（例如图7）。3.1运行至完成模式在运行到完成（RTC）执行模型中，组件以不可分割的步骤执行，没有任何并发活动的中断。RTC语义的主要优点是简单性和保证没有死锁。另一个优点是，它可以删除不必要的交织，从而加快形式化验证，使模型更接近实现。该模式通常用于高级行为建模语言，如Stat- echarts及其变体[12，17]。在Statecharts中，事件以RTC方式处理，可能是复合转换（即，相邻箭头的路径）。模式说明。在这种模式中，我们假设组件执行通过触发启用的转换来继续改变状态，直到它到达一个没有启用传出转换的状态。此时，执行终止。要实现该模式，需要将相应的PFSM转换为时间自动机（TA）。运行到完成可以通过在自动机中引入新的边来实现，这些边描述了组件执行的终止设L是位置li，i∈ {1，.，n}在相应的TA中。对于每个位置li∈L，我们假设gj，j∈ {1，.，m}是相应输出边的保护。从li的出口边连接li和出口位置。警卫1、《金刚经》云：（jgj）。Example. 图2表示一个简单组件的PFSM规范，它遵循我们的运行到完成模式。图3描述了作为时间自动机的等效行为，它充当模式实现。PFSM的状态S1、S2和S3分别映射到等效TA中的位置l1、l2和l3L1x>=5 sense（）L2x =5 activate（）l3X 5x>5166D. Slutej等人/理论计算机科学电子笔记253（2009）161图4. 具有历史记录x==3 update（）开始退出图5. 具有历史模式3.2历史模式执行历史是行为建模技术的核心特征[2，12]。行为的历史机制会记住在退出之前，在执行期间最后访问了哪个状态。下次重新开始执行时，可以重新进入此状态。在Statecharts [12]的分层状态机建模中，通过使用历史机制，可以直 接 退 出 和 重 新 进 入 内 部 状 态 。 类 似 的 方 法 被 采 用 在 CHARON 中 ，CHARON是混合系统的正式建模框架[2]。模式说明。 该模式提供了一种机制来记住组件行为模型中的执行历史。假设执行是一个状态序列，该模式具有记住执行期间达到的最后一个状态或特定状态的方法。因此，下一次，执行可以从通过历史机制存储的状态恢复。与Statecharts类似，在PFSM表示中，历史机制表示为圆圈内的H，并充当起始状态。该模式通过使用整数变量H实现为TA，该整数变量H沿着连接从开始到退出状态的任何状态的每条边进行更新，并具有相应的位置标识符。特殊边缘将起始状态连接到每个感兴趣的状态，同时适当地测试变量H。此外，退出边缘将每个感兴趣的状态连接到退出控制状态。变量H可以在进入指定的最终位置时适当地重新初始化。Example. 图4展示了具有历史模式的组件行为。在开始状态下，历史由带圆圈的H符号表示。在图5中，我们给出了与TA等效的行为模型，它实现了历史模式。图4中的状态被映射到TA中的位置1、2、3变量H被初始化到初始位置，即，H= 1.将起始位置连接到位置1和2的边缘是由于图案，并且分别由条件H==1和H==2保护此外，历史变量H用沿着进入相应位置的每个边缘（离开和离开的边缘）的位置标识符来更新1x>=5 sense（），2x>=5activate（），H=13H==1H==2D. Slutej等人/理论计算机科学电子笔记253（2009）161167可以跳过输入相同的位置，例如，图5中的位置2）。最后，在图5的位置3处重新初始化H。3.3执行时间模式对于嵌入式和实时系统，指定和分析组件的最佳或最差执行时间执行时间的变化还引起，例如，非确定性时序、抖动和变化的端到端时序，它们代表在设计时分析（和掌握）的重要现象。在下文中，我们将介绍一种用于指定组件的最佳和最差执行时间的模式。图6. 执行时间模式PFSM模型的时间属性标注模式说明。在这个模式中，我们假设执行一个组件的总累计时间在一个区间内，其中上界和下界分别是最短和最长的可能执行时间。因此，组件将在间隔中的某个时间实例产生输出（数据和触发）。我们还假设组件使用指定执行时间上下限的间隔进行注释。为了实现该模式，我们使用一个专用时钟，比如说exec，它用于测量组件被触发后的时间。时钟在从位置开始向外的边沿上复位。我们进一步引入了一个位置，比如延迟，以及从位置延迟到出口位置的边。位置延迟用exec上的不变量注释，对应于执行间隔的上限，而出口边缘用对应于执行下限的保护来装饰。Example. 图6表示使用执行时间模式指定的PFSM。它的执行时间是在（封闭的）间隔[l，m]中图7显示了实现该模式的时间注意，当到达出口位置时，时钟延迟的值在间隔[l，m]中。x==3 update（）x>=5 sense（）L1exec=0x>=5 activate（）l2 l3开始出口exec>=1delayexec =m图7. 具有执行时间模式168D. Slutej等人/理论计算机科学电子笔记253（2009）161图8. 转盘示意图 系统4转盘生产单元在工业自动化中，生产单元是整个生产系统的一部分- 一家工厂在本节中，我们提出了一个转盘生产单元的正式模型，之前在[6，19]中描述过案例研究是使用第2节中描述的组件框架和第3节中介绍的模式设计的。通过使用这些模式，我们可以为案例研究获得简单易懂的组件模型，如以下小节所示。转盘单元如图8所示。它主要由一个带有四个产品槽的转盘组成。将产品装载到位置0处的槽中，然后旋转到位置1，在位置1处对其进行钻孔。然后将其旋转到位置2进行测试，最后旋转到位置3进行卸载（或可能在下一个循环中重新钻孔）。这些位置与用于装载、钻孔测试和卸载。钻孔和测试是最关键的工具位置，因为生产单元的总体目的是验证通过单元的产品的钻孔。转盘的所有槽可同时占用，产品并行加工。当一个循环完成时，意味着所有位置完成其功能，旋转盘旋转90度，从而定位产品进行下一阶段的处理。由于旋转是由来自工具的非时间确定性信号启动的，因此在槽的旋转之间没有固定的周期。4.1系统设计根据系统的非正式描述，我们可以确定系统由五个主要软件组件组成：转盘，加载器，钻孔器，测试器和卸载器，对应于单元的功能这些组件与多个传感器和执行器（如位置传感器、夹紧和钻孔设备）交互，这些传感器和执行器不需要显式建模。此外，当我们专注于建模D. Slutej等人/理论计算机科学电子笔记253（2009）161169图9. 转台系统表1组件Loader、Driller、Tester和Unloader的通用接口端口数据类型描述地位int表示产品在刀具位置的当前已知状态的输入（0表示空槽）。结果int一种保存产品处理后状态的输出。开始bool启动刀具加工的一种输入。已完成bool一种输出，当由组件控制的刀具完成加工时发出信号。以及对系统的功能和定时行为的分析，我们对错误情况进行说明，例如，没有故障情况，如破损的工具等。这简化了系统模型，而不失一般性。我们现在详细描述软件组件的接口和行为。图9显示了转台系统的软件架构组件的接口定义了其行为的访问点，在我们的例子中是数据端口和触发器端口。转盘组件在系统中充当中央控制器，所有其他组件彼此独立，并与转盘具有类似的接口。公共接口方法支持重用，以及扩展或修改系统架构的灵活性。我们为每个组件定义了一个公共接口，除了转盘，如表1所示。数据流由数据端口之间的连接、公共接口内的连接以及与外部传感器和执行器的连接定义。通过触发端口之间的连接，控制流与数据流分开建模。如图9所示，流程从Clock组件开始，在Unloader结束。组件行为根据上一节定义的建模模式假设建模为有限状态机。历史和运行到完成模式相结合，以实现组件的建模有限状态机器行为，即使组件将以时间触发的方式执行。执行时间模式用于对执行每个组件所需的时间进行建模。因此，模型呈现直观的概念建模，保留了底层形式主义的分析能力，即，时间自动机建模的行为在SaveCCM170D. Slutej等人/理论计算机科学电子笔记253（2009）161图10. 行为模型转盘组件。rotateSlots（）是temp：int：= status0aRotate：= true状态0：=状态3;状态3：=状态2状态2：=状态1;状态1：=临时端startWork（）是for positionsi dostarti：=true端（）是ositionsidostatusi：=结果i位置idostarti：=falseetedi开始i：finnishedi图11. Turntable使用的函数和谓词。组件模型和模式的语义。在下文中，我们描述了每个组件行为及其相关功能和预测，这些功能和预测根据与相应组件的数据和触发端口相关的变量进行定义。4.1.1转盘组件转台控制器的接口由两个触发器端口、一个传感器输入、一个执行器输出和四个公共接口实例组成。时钟组件生成触发信号以周期性地激活转盘，转盘进而激活加载器组件。致动器输出aRotate连接到转动旋转盘的电机，并且传感器输入sRotated感测旋转何时完成。转盘组件的行为协调光盘的旋转与其他组件的执行。最初，它旋转圆盘，并适当地设置其他组件的端口。然后，它等待其他组件发出信号，表明它们的处理已经停止，然后通过再次转动光盘重新启动主循环4。从一个空的系统开始，所有组件至少需要四次旋转才能并行工作。第一次旋转仅启动Loader的处理，然后将第一个产品加载到工作台上。除了控制光盘的旋转，该组件还保持每个位置的状态信息。工作台每旋转一次，状态信息就移动一步。 详细的行为被建模在图10中，根据相关的函数和谓词（在图11中列出）。内部变量statusi、starti、finishedi、resulti表示位置i的相应公共接口端口的数据值。4因此，即使转盘被周期性地触发，光盘的旋转周期也取决于四个时隙中的处理时间。D. Slutej等人/理论计算机科学电子笔记253（2009）161171图12. Loader组件的行为模型。图13. Driller组件的状态机模型。图14. Tester组件的状态机模型。4.1.2加载器组件如上所述，加载器与转盘共享公共接口，并从转盘接收触发器。它还有一个到司钻的触发输出、传感器输入sLoaded和执行器输出aLoad。行为模型如图12所示。当被触发时，组件检查位置0处的插槽的状态。如果存在之前的产品，由卸载器转发进行再处理，则将产品留在槽中进行重复钻孔。 否则，将新产品装载到槽中，以便在下一个循环中钻孔。4.1.3司钻组件图13显示了Driller组件行为的模型，该模型与执行器和传感器相互作用，用于夹紧和钻孔产品。触发时，组件检查位置1处插槽的状态。如果是空的，司钻什么也不做，否则槽中的产品被固定（夹紧），钻头开始旋转并下降。当钻孔完成时，钻头被提升并停止，并且槽的状态被相应地更新4.1.4测试器组件Tester的行为模型如图14所示。它的输入触发从司钻接收，输出触发输出发送到卸载器。与钻机类似的工具172D. Slutej等人/理论计算机科学电子笔记253（2009）161图15. Unloader组件的状态机模型测试器是传感器sTesterDown，其在自测试过程开始的2个时间单位内测量孔当被触发时，组件检查位置2处的插槽的状态。如果是空的，它什么也不做，否则它会测量产品中钻的孔，并根据其判决更新状态4.1.5卸载器组件图15显示了卸载器行为的模型位置3处的钻孔产品的状态指示 如果产品被错误地钻孔，则其不被卸载，否则，组件激活致动器以卸载产品。如果槽是空的，如在初始旋转中，卸载器不做4.2封闭系统为了验证的目的，我们定义了一个封闭系统，即没有输入或输出的系统通过对转台进行组合，建立了转台的封闭模型控制器软件，环境的时间自动机模型这是由致动器和传感器控制的。转台控制器的软件架构如图16所示（如Save-IDE中SaveCCM语法所示）。按照第3节中介绍的建模模式，将上一节中建模的每个组件的行为转换为TA。转台控制软件的环境用复杂的真实世界方面的适当抽象来建模，以这样的方式，真实物理环境的行为（和定时）被包括在模型中。 此外，如前所述，该模型是在正常行为的假设下完成的，这意味着不会发生异常处理或错误条件，例如故障传感器或在UPPAAL工具中，转台系统的环境被建模为时间自动机（TA）环境基本上由与系统及其组件相关的执行器和传感器组成由于篇幅限制，我们省略了一些环境自动机，我们建议读者参考我们最近的工作[19]以获得更详细的环境模型。系统与环境之间的通信接口通过共享变量来实现。这些变量对应于建模系统软件与其传感器和执行器之间的通信端口，以及驱动验证过程的测试自动机。 表2中给出了接口及其初始化。简化建模过程，缩小状态空间D. Slutej等人/理论计算机科学电子笔记253（2009）161173图16.在Save-IDE中建模的转台系统的控制结构和系统架构在模型中，系统的所有方面都没有明确建模。相反，模型侧重于系统的关键方面。 用于转台正式验证的环境模型由行为Disc、Clamp、Drill和TestTool组成。钻具由两个可控部件建模：夹具和钻具。这些环境模型的行为分别如图17和18所示。 夹具的作用是将产品锁定到位，以便进行钻孔。时间自动机最初是在位置UnLocked中，并且当边缘保护aClamp变高（值变为1）时转换到位置Locking。 它可以保持在位置锁定，只要相关的不变claCLK≤ClampTime保持。当夹钳处于解锁位置时，也会发生同样的情况。 这将对夹钳的连续行为进行建模。钻孔机的作用是在产品上钻孔时间自动机表2环境组件TA变量数据类型最初盘a旋转，s完成bool假夹具a夹钳，bool假锁定，解锁钻a向下钻取，a向上钻取bool假sDrillDown、sDrillUp测试工具a测试器向下，a测试器向上bool假sTesterDown，sTesterUp174D. Slutej等人/理论计算机科学电子笔记253（2009）161claCLK=0，sUnlocked=假紧急aClamp解锁claCLK>=ClampTimesUnlocked=true锁定claCLK =箝位时间claCLK =夹紧时间解锁claCLK>=ClampTimesLocked=true！紧急止血夹claCLK=0，sLocked=false锁定图17. Clamp环境模型的行为drillCLK=0，sDrillUp=假紧急钻机下移drillCLK>=MinDownTimesDrillDown=trueaDrillMoveDowndrillCLK =最大停机时间DrillUpdrillCLK>=MinUpTimedrillCLK =MaxUpTimeaDrillUp紧急DrillDownsDrillUp=true钻机上移drillCLK=0，sDrillDown=true图18. 环境模型的Drill行为（图18）最初处于DrillUp位置，当保护aDrillMoveDown变高时，转换到DrillerMovingDown 它 可 以 保 持 在 这 个 位 置 ， 只 要 相 关 的 不 变drillCLK≤MaxDownTime保持不变，以模拟钻孔可以发生的最大时间。当钻头位于DrillerMovingUp位置时，也会发生同样的情况。在MinDownTime或MinUpTime之后，司钻分别从下钻或上钻的连续行为中移出。测试工具的工作原理与钻头类似，通过致动器发出的命令向下移动，直到传感器被激活，然后通过不同致动器发出的命令再次向上移动，直到相应的传感器被激活。此外，Disc是用两种状态建模的，等待和转弯。从等待到转弯的转换由致动器aRotate启动，清除传感器值sCompleted，并重置时钟，确保在转弯时间时间单位内转换回等待，此时传感器值sCompleted也已设置。4.3要求和验证在本节中，我们将介绍转台系统的验证方面。这项工作已经在Save-IDE中完成，这是SaveCCM的集成开发环境。对于建模，Save-IDE提供了用于架构和行为建模的图形编辑器。对于通过模型检查进行的系统（符号）仿真和验证，工具UPPAALPORT[11，10]是UPPAAL[16]的扩展，通过插件集成。系统架构和组件行为的表示以SaveCCM XML文件格式表示[8]，环境存储在UPPAALXML文件中。UPPAAL端口连接系统环境模型中全局变量的输入和输出已经验证了关于转盘控制系统的安全性和活性的一组属性在UPPAAL中，活性属性可以被指定为导致形式为P~PJ的属性，这意味着如果系统已经达到某个状态，在满足P的情况下，它最终将达到满足PJ我们讨论了下面是几个代表性的属性。第一个具体的属性是：D. Slutej等人/理论计算机科学电子笔记253（2009）161175Q<$死锁（1）属性1是一个安全属性，指定不存在死锁情况。当系统无法继续运行时，就会发生死锁。在实时系统中，这通常是由两个任务互相排斥获取资源（例如信号量）引起的。它也可能是由环境模型中的故障引起的。该物业已按上文所列予以核实。A是一个通用量化器，指的是在状态空间的所有执行路径上要验证的属性。盒子Q是一个泛量化器，它覆盖路径上的所有状态，状态由所有变量的值和自动机的位置定义。关键字deadlock表示执行中没有传出（延迟或操作）转换的状态。转台系统被验证为无死锁。没有僵局并不意味着该制度一定会取得进展。控制系统可以继续组件触发，而组件不通过它们各自的有限状态机前进。以下一组属性验证转盘系统是否正在运行。它检查中心组件转盘是否在空闲和转动状态之间连续移动这是使用属性的引线来指定的。菱形Q是路径中状态的存在性量化器，这意味着该属性最终会被路径中的一个状态满足（在这种情况下是所有路径Q转盘。旋转转盘。旋转~转盘。闲置（2）转盘。空闲~转盘。转折属性2确定组件Turntable始终前进。只有当各个组件也按照设计策略进行时，这才是可能的个别组成部分的进度可核实如下。装载机。准备好了~装载机。第1003章完了（三）上面的lead-to属性3验证了Loader总是前进。我们可以验证所有其他组件的类似属性。此外，我们验证了一个重要的安全属性，即当转盘组件正在执行时，没有其他组件正在执行：AQ（转盘。车削加工（4）（装载机。准备就绪测试仪。准备卸载。准备好，司钻。准备好了））属性4模拟了这样一个事实，即当转盘转动另一个组件时，根据设计策略，用户只是在他们的就绪属性5建立环境组件和相应SaveCCM组件之间的状态对应关系。该属性可确保只要转盘不转动，圆盘零部件也不转动：AQ（<$Turntable. 旋转圆盘。车削）（5）下一个属性（6）指定控制模型永远不会向其环境发送两个冲突信号在这里，它检查系统是否同时激活176D. Slutej等人/理论计算机科学电子笔记253（2009）161与司钻组件相关的致动器，同时，当它们移动向相反方向钻孔AQ <$（司钻。a下钻钻头。aDrillUP）（6）5相关工作在文献中描述了许多用于嵌入式系统的基于组件的开发（CBD）框架。 BIP框架和工具包IF [4]旨在通过支持构造纠正和组合验证来实现可预测的嵌入式系统开发。虽然BIP操作员自下而上设计系统，但我们的方法支持CBD在更实用的传统自上而下设计中，支持Save-IDE [18]中的建模和使用UPPAAL端口工具包[11，16]的正式验证。Charon工具包[2]支持嵌入式系统的模块化规范，基于代理和模式的概念，分别用于架构和行为规范。我们的组件行为规范语言共享Charon中模式的一些特征，但没有层次结构，并且在我们的方法中，组件的执行历史通过使用简单的设计模式提供Statemate工具包[14]是开发复杂反应式系统的早期工作环境系统开发的模块化是以不同的视图（如结构、功能和行为）来提供的。我们对组件（Statemate中的模块）的行为规范的方法类似于Statecharts [13]，Statemate的行为语言虽然不是分层的，我们的组件行为FSM符号（见第3节），结合本文中提出的模式，类似于状态图功能运行到完成和执行历史。本文以转盘生产系统为例，采用不同的方法和工具进行了初步分析。 在[7]中，转盘模型在工业系统的模拟语言χ[20]中指定，并翻译成Promela，Spin模型检查器的输入语言，以验证模型的几个特性。在[6]中，转台系统的χ模型被翻译成三种模型检查器的规范语言：CADP、Spin和Uppaal，比较了转换的容易程度、每种规范语言的表达能力以及各自模型检查器的能力和性能。在[15]中，转台生产系统在COMDES-II基于组件的软件框架中实现。作者开发了COMDESS-II模型到UPPAAL时间自动机模型的语义转换，允许对类似于[6]中的一组属性进行正式验证。6结论在本文中，我们介绍了如何SaveCCM组件为基础的方法开发的嵌入式系统已被应用在一个案例研究，建模和D. Slutej等人/理论计算机科学电子笔记253（2009）161177验证工业转台生产系统。提出了一种基于构件的系统体系结构模型，并给出了系统构件的详细行为模型。为了生成一个易于管理和掌握的转盘设计模型，我们使用了三个简单但有用的设计模式。组件的有限行为在有限状态机符号中指定，使用两种设计模式编码运行到完成语义和历史状态。引入时间-ING使用第三种设计模式指定执行时间和组件的顺序。我们还描述了如何将设计规范从语法上转换为SaveCCM中使用的建模框架，以便使用UPPAAL端口进行进一步分析。在整个案例研究中，我们一直在使用Save-IDE及其与UPPAAL端口的连接，用于编辑模型，以及执行（符号）仿真和通过模型检查进行验证。作为建模结果，我们相信我们已经产生了一个非常直观的基于组件的转台系统模型。作为验证结果，我们已经证明系统模型满足系统的所有特定要求，在TCTL中形式化为安全性和活性属性。作为未来的工作，我们打算开发一个丰富的行为建模语言和正式的分析支持的继任者SaveCCM，称为ProCom。该语言将基于本文中描述的设计模式，并可能基于其他新开发的、更复杂的模式，这些模式可能有助于简化正式模型及其验证。引用[1] Mi kaelAkerholm ， JanCarl s on ， JohanFre drik s on ， H ansH ans s on ， JohnHakan s on ， Ander sMüoller，PaulPettersson，and Massimo Tivoli.车辆系统基于组件开发的SAVE方法。Journal of Systemsand Software，80（5）：655[2] R. Alzheimer，D.作者：J. Yerang，F. Ivancic，V. Kumar，P. Mishra，G.J. Pappas，and O. 索科尔斯基嵌入式系统的层次化建模与分析。Proceedings of the IEEE，91（1）：11[3] 作者声明：David L.迪尔时间自动机理论。Theoretical Computer Science，126（2）：183[4] Ananda Basu，Marius Bozga，and Joseph Sifakis.异构实时构件的bip建模。见SEFM，第3-12页[5] Gerd Behrmann ，Alexandre David和Kim G. 拉森关于乌帕尔的教程。在Marco Bernardo和FlavioCorradini的编辑，实时系统设计的形式化方法：第四届计算机、通信和软件系统设计的形式化方法国际学校，SFM- RT 2004，LNCS第3185号，第200-236页Springer–Verlag, September[6] E. Bortnik，N. Trcka，A. J. Wijs，S. P. Lutti k，J. M. Vandd e Mortel-Fronczak，J.C. M. Baeten，W. J. Fokki nk和J. E.鲁达利用Spin、CADP和Uppaal对转台系统的χ模型进行了分析。Journalof Logic and Algebraic Programming，65（2）：51[7] V. Bos和J.J.T.克莱恩制造系统的自动验证。机器人与计算机集成制造，17：185[8] J. Carls on，J. Hakakans on，andP. 别担心。 Save CCM：一种简单的适用于实时系统的组件模型。在Proceedings of the 2nd Workshop on Formal Aspects of Components Software（FACS 2005），Electronic Notes in Theoretical Computer Science。Elsevier，2005年。[9] E.伽马河赫尔姆河Johnson，and J. Vlissides. 设计模式：可重用的面向对象软件的元素.艾迪森·韦斯利专业计算机公司AddisonWesley出版公司，马萨诸塞州雷丁，1995年。178D. Slutej等人/理论计算机科学电子笔记253（2009）161[10] J. Hakakakans onandP. Pettter ss on. Partialorderde d e e d e d e e d e d e e d e d e e d e e d e d e e d e e d e ed e e d e e d e e d e e d e e d e d e e d e d e e d e e d e e d e e d e e d e e d e e d e 第一届国际时间系统形式化建模与分析研讨会论文集，计算机科学讲义。[11]约翰·哈塔米，约翰·卡尔，阿雷里·莫诺，保罗·佩特，还有D·阿沃尔·S·鲁特。带uppaal端口的嵌入式系统的Componen-based设计与分析。第六届国际自动化技术验证和分析，第252[12] D. Harel和E.格里用状态图进行可执行对象建模。IEEE Computer，30（7）：31[13] 大卫·哈雷尔。Statecharts：A Visual Formalism for Complex Systems. 计算机程序设计科学，8：231[14] David Harel ， Hagi Lahover ， Amnon Naamad ， Amir Pnueli ， Michal Politi ， Rivi Sherman ，Aharon Shtull-trauring，and D Mark Trakhtenbrot.Statemate：用于开发复杂反应系统的工作环境IEEE软件工程学报，1991年16期。[15] 徐珂，P. Pettersson，K. Sierszecki和C. 安杰洛夫 使用uppaal和模型转换验证comdes-ii系统。嵌入式和实时计算系统和应用，2008年。RTCSA '08。第14届IEEE国际会议，第153-160页，8月。2008年[16]