英语原文共 6 页，剩余内容已隐藏，支付完成后下载完整资料
基于Event-B的自动生产线形式化建模与验证研究
1.北京理工大学电子与控制工程学院，北京，100124，邮箱: fu_kaiming@163.com
2.教育部数字社区工程研究中心，北京，100124，邮箱：fangbin@bjut.edu.cn
3.北京城市轨道交通实验室，北京100124，中国，邮箱： fangbin@bjut.edu.cn
4.计算机智能与智能系统北京重点实验室，北京100124，邮箱： fangbin@bjut.edu.cn
摘要：自动生产线在工业领域投入使用之前，必须经过长期的大量的严格测试，才能在设计过程中检测出误差。然而，在实际的测试过程中，由于测试方法的不同，同样的错误导致了不同的测试结果，并且由于现场环境不能被测试的局限性，也存在一些特殊的条件。该形式化方法也适用于大型无功分布式系统的开发。本文提出了一种称为Event-B的形式化方法，提高了系统的安全性和可靠性。并利用Rodin等相关工具在PLC(Programmable Logic Controller)自动生产线上进行建模、细化和验证。本文的结果表明，我们的方法有助于减少早期开发阶段的系统细节，从而使证明更简单、更自动化。从而为工程项目对可靠性的更高要求提供了一种新的参考方法，从而保证了所设计软件的正确性。
关键词：自动生产线，PLC，模型，验证，Event-B，形式化方法
1.引言
自动生产线依靠机械、电气等控制技术，它是一种现代自动控制系统。数字逻辑控制器PLC作为各种自动化系统的核心，在现代工厂自动化领域发挥着越来越重要的作用。由于自动化程度和集成度高，一旦自动生产线出现问题，不仅会造成产品的损失，而且有时甚至会造成设备的损坏。 为保证生产线的稳定和安全，需要高可靠的要求。
形式化方法是基于严格的数学技术对计算机系统进行研究的方法。软件开发的形式化方法的主要目的是确保所设计软件需求的正确性。现了数学建模的功能描述，同时用数学逻辑进行了验证，以发现我们使用的系统其潜在的危险因素。如图1所示，在开发阶段，集成表单开发过程通过规范和设计过程中的数学证明，可以保证程序的可靠性 避免模块测试，从而确保了程序的正确性，降低了开发成本。
本文选择Event-B形式化方法对生产线自动控制过程进行建模和细化，并结合功能需求和使用机器证书的安全性要求，对自动生产线控制过程进行了建模和改进。在本文中，Rodin平台被用于该项目，该平台基于Eclipse开发平台，通过平台扩展提供插件。Rodin平台主要扩展了一些证明和模型检查器，大大提高了Event-B建模的建立和验证效率。
2.Event-B建模的理论和方法
2.1、Event-B建模介绍
Event-B是一种形式化的开发系统，其组件可以建模为离散转换系统。事件-B模型包含两个部分：一个由转换系统建模的动态部分(称为机器)和一个捕获模型参数和假设的静态部分(称为上下文)。Event-B处理系统复杂性的主要技术是逐步细化，设计细节逐渐引入到形式化模型中。精化可以使机器变抽象，而且由于抽象机器包含的细节比具体的少，所以它们通常更容易验证。然而，在开发大型复杂系统时，细化往往是不够的。机器包含足够的细节来陈述和证明相关的安全特性，这可能会导致无法管理的复杂性的证明。我们在开发大型列车控制系统时注意到了这一局限性。为了说明和解释无碰撞属性，我们需要对火车进行详细的建模，例如，将它们的布局和运动正式化。因此，我们不得不陈述许多复杂的不变量，从而导致了许多复杂的手工证明。这产生了另一种方法，从系统模型中抽象出更多的细节，以降低复杂性并提高结果证明的自动化程度。除了扩大环境模型和改进机器之外，机器使用参考(参见)来接触环境，即过程连接模型的动态部分和静态部分。机器可以引用任意数量的环境，即：0, 1个或多个环境。因此，根据事件-B模型引用不同的环境来扩展和细化每个环境和机器，每台机器，使结构Event-B模型显示各种各样的情形。环境与机器的关系如下：
它代表了环境的静态部分，包含一个向量集、常数、公理和定理。此外，载体是用户定义类型的集合，常量在系统不变公理中作为载体集合和常量属性表示它们的性质。定理是由载体集合而来的常数，并推导出其性质，同时也应该是经过严格证明过的。 同样，它代表机器的一个动态部分包含变量、不变、定理、变体和事件。另外，变量表示机器的状态，不变量是变量的属性。定理是可变或不变的发射性质，也需要严格证明。变量用来证明事件的收敛性。事件模型用于表示状态和转换，这意味着系统可能发生什么和何时发生。安全条件是所需的事件，当满足状态健康条件的参数和变量时，事件就会发生。Event-B是一种基于模型建模的形式化验证方法，用于确定模型的安全性、有效性和完整性以及模型精化过程的一致性公理和定理。模型需要证明，这就是证明义务。证明义务都是公理和定理所涉及的不定式约束模型，通过相应的数学推导，所产生的模型用于验证结论的正确性。第二部分研究了证明义务的内容、形式规范和形式验证方法。
2.2自动生产线
在接下来的部分中，我们将介绍事件B上的自动生产线模型。自动生产线用于生产无线电药品。这些无线电药品具有放射性，可能对设备和人员造成损害，因此，对控制程序的正确性和可靠性提出了严格的要求。本节，我们将讨论系统的传输部分。总体过程如图3所示：
根据工艺过程，理想的生产线控制系统可以按照时间周期划分为加工阶段和加工阶段。传递阶段包括制品和回收站两部分。将所述配送到与相应站相对应的部分，在配送定位完成时，就开始处理。在实施的一部分过程中，至少有一个完整的处理所有固定装置的过程，这些装置需要在处理时间内完成回收工作，所以在下一个周期进入车间，也就是回收和固定过程并行。自动生产线采用PLC控制，通过控制一系列的钢瓶、输送机、电磁铁和伺服电机作为主要的执行机构，按顺序将固定装置送到车间。它分为上下两层，由电梯连接。下层通过输送机输送加工夹具，上层由主通道和五个制造站组成，将固定装置送到相应的站。根据生产线的功能，我们简化了五种圆筒描述的交付过程。一类负责提升者和主通道之间的传递过程。B级钢瓶将固定装置送到各车站，形成主通道。C级钢瓶定位车站上的固定装置。D级钢瓶驱动提升器，连接上下层。E级钢瓶负责提升机与输送机之间的输送进度。整个交付过程将分为11个主要步骤，进展随时可能暂停或重新启动。
2.3 Event-B的细化
精化提供了一种将系统动态行为的细节逐步引入到正式模型中的方法。Event-B是一个渐进的建模方法，通过细化，该模型比前层模型有更具体的方式，更多的功能和细节，细化政策设计描述的是一个从抽象到具体的过程模型。
一般来说，系统的初始模型是一个相对抽象的模型，只是为了大致了解系统的功能，并不能查看实现细节。在初始模型细化和分解之后，然后通过横向细化引入新的系统元素，通过纵向精化完成系统的实现部分，重复上述步骤，可以细化模型，直到模型达到需求要求，才能实现。在对模型进行细化的过程中，我们应该进行形式验证，以确保模型每层的模型的正确性。根据生产线，我们应该从相同的基本功能入手，然后通过横向细化引入新设备，实施纵向细化的功能变更，最后进行形式验证，以确保细化过程的正确性。
2.4 Event-B建模的过程
因为在建立模型的同时，Rodin平台会自动生成所要验证的模型证明的义务，所以作者采用层层模型法验证，即以法规和形式验证的形式逐层验证，只有通过验证、层次模型，将是下一个层次的细化。这种好处是能够减少错误并修改模型的数量，从而更容易定位。下面将介绍生产线的主要方法Event-B模型的构建和验证过程。
在这方面，为所有按钮引入单独的事件，这些按钮描述正常操作期间的进度事件的状态，如图4所示。
在初始模型中，由三个布尔变量描述—启动、暂停、停止三个信号按钮状态，并介绍了在相应的输入状态下所描述的事件，即按下按钮进入正常工作状态后，启动生产线；当系统进入停止按钮后立即停止等待状态，当启动信号到达时恢复当前工作；当按下复位按钮时，生产线立即复位，恢复初始状态并进入停顿状态。
事件进度指按下“开始”按钮后的工作状态，此模型中的事件进度仅为抽象事件，未采取任何操作，该事件在当前模型中执行时不进行替换，我们需要遵循这个事件的模型细化，详细描述它们的行为。未扩展属性的事件进度表示该事件不是扩展事件。该属性将指示事件可能会产生不确定的行为，并且需要在模型收敛之后加以证明。确保模型是收敛程序，以确保可访问性，在模型的后面将详细描述细化。在FUN-7功能要求的初始模型中对事件做了粗略的描述，除了最初的模型代表了正常的工作进度，还包含停止和重置状态描述事件，类似事件的进展情况，它不必具体描述事件行为，因为在这一阶段对事件进行详细的描述是不够的，因此也需要在后续模型中加以细化。
2.5如何逐步完善
第一个模型细化mac1来细化初始模型并分解它，同时输送到气缸并进入模型，并进行法令和验证。在第一个模型的细化中，主要目的是解决原问题模型中的事件进度问题。在初始模型中，事件进度表示生产线系统开始运行，但没有执行任何操作或是空替换。在第一个模型中，通过参考环境ctx0，ctx1步骤细化mac1，将气缸和输送机放入模型中，通过这些事件进行细化处理。进度事件分为11个主要步骤，如果进度处于活动状态，则必须有且仅有一个步骤处于活动状态。在每个步骤中引入新的国家机构和程序的作用，并描述每一步骤，当规约中有11条并验证了所有主要步骤的完成时，细化事件进展，并且之后事件将不会在重新出现Event-B模型，由11个主要步骤取代。
如图5所示，气缸和输送机中环境的输入和输出状态，以及进入模型的状态。其中载波集代表一定有限的输入和输出集，常量表示对象可能声明的元素的集合。公理描述了载体集合和元素之间以及不同元素之间的关系。缸具有三个互不相同的输出状态和三个互不相同的输入状态。输送机包含移动和停止状态，该步骤包括工作，完成和停止三种相互不同的状态。
引入新元素并进行描述，通过在机器中引入变量来描述事件。从一个事件细化到事件的初始进度模型，步骤2是除法中的一个步骤进展。这一步有三种状态包括工作步骤，该步骤有三种状态，包括工作步骤、步骤和步骤失败，以及这一步只涉及到对一个气缸A1的操作。所以这个步骤可以用三个事件来表示来表示步骤2，可以显示步骤2完成的步骤，同时也可以表示步骤2的失败。
扩展属性表示事件扩展的过程，其中轻型部分完全继承于事件进度。与最初的模型事件相比，第2步：通过添加新的条件3在健康条件中进行改进；步奏2和过程4：圆柱体的2D状态条件对事件进行限制。新动作也引入了事件行为1，推送出行为2，汽缸的规定和台阶的状态发生变化。其中，ACT 2的非确定性行为，其行为应根据生产线的实际运行状态来判断，这可能会产生不同的执行结果，它仍然预期事件步奏2工作事件（预期事件），需要在后续模型中对其收敛做出说明。
3.自动生产线事件B模型的验证
第2步完成事件描述只是以法规的形式部分完成了正式的方法，所以接下来的部分也要进行正式的验证。在本文中，罗丹平台工具平台上设计的生产线模型进行验证，并会自动产生相关的证据义务，证据主要涉及两项义务，如图7所示。第一项义务是需要证明事件步骤2的工作和不变量产生的不变义务维护证明。根据国家安全基金-2规定的安全条例，在D级圆筒必须引入状态的前提下发射的类圆柱，因此，第一个模型被引入到细化无穷大的描述中，如图8所示，而事件2工作行为1需要满足不定式的要求。在这里，通过添加一个保护的方式，使第2步中的条件确定工作证明义务。需要证明的第二个义务是事件步骤2的行为2所产生的行为义务的可行性。如图8所示，因为这两项义务相对简单，因此可以完全自动地证明。完成和验证规约只是第一个事件，步骤2精化了工作的一小部分。每个步骤还包括其他事件，例如步骤2，步骤2FILE类。如图9所示，步骤2_Done也是从进度继承的，与步骤2_Working不同，表示事件在步骤2步骤后要完成的过程。按魏氏条件，第3步：第2步=完成，第4步：圆筒A1=推出，激活步骤3。在这里，第2步没有判断是否完成了第2步，只有在事件完成后，步骤2和步骤2工作不同，第2步不做不确定的行为，因此，步骤2是一个一般事件，没有验证可行性证明义务。但是因为它涉及气缸A1的操作,还需要证明满足不变圆柱轴D，即证明步骤2_Done/缸体AxD/INV保持证明的不变义务，证明和步骤2的工作类似，在这里不再重复。证明义务不能自动证明罗丹提供的衍生规则基础机制，证明策略和第一工具，人为地增加了假设和交互规则的数量，手动指导。Event-B是一种增量建模方法，通过改进模型与模型的比较方式更具体，更多的功能和细节，正如肉眼粗糙的表面所能观察到的事物一样，它需要显微镜来看细节。完整的Event-B模型应该是环境的控制器，然后从环境中反馈给控制器的封闭模型。在完成模型的基本描述之后，下一步是进行纵向精炼。为了生产线控制系统的目的,纵向细化的最终目的是取代现有的逻辑变量和实际可测量的可控信号。
通过对PLC生产线模型的十三次精化和验证，他为所有相关内容建立模型，通过核查证明罗丹平台义务已经完成，根据罗丹平台的统计，总共提出了5-30 2237项举证义务，自动证明1292943次人工复核，未解决0，自动证明率近58%。
4.总结
自动
全文共6325字，剩余内容已隐藏，支付完成后下载完整资料
资料编号：[11517]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
