- 选题背景和意义：
-
可编程逻辑控制器PLC 是一种被广泛应用于工业控制领域的反应式系统。目前从业人员编写 PLC 程序主要依靠个人经验需求漏洞、程序错误等情况难以避免。 针对这一问题，使用规范化的语言对系统需求进行描述可以显著提高开发过程中需求的可读性和准确性。 Matthew B. Dwyer 等人提出的规约模式系统SPS将反应式系统中常见的场景分析归纳，抽取出特定的模式，以接近自然语言的形式对场景进行描述， 在时序表达方面有着较强的能力 。 但对包含大量实时控制需求的 PLC 系统，目前使用 SPS 进行规约 描述的研究仍不够完善， 描述能力较差缺乏实用价值。 在 PLC 程序生成领域现有方法 大多要求先对系统进行手工建模再通过模型生成PLC 程序这对 PLC 从业人员存在较大 难度或虽然可以直接根据规约通过模型验证和博弈论的方法自动生成PLC 程序，但所生成的代码规模为指数级，且不符合 PLC 从业人员的开发习惯， 可理解和可维护性较差。
现在有对SPS做出扩充SPS4PLC，SPS4PLC采用接近自然语言的表述方式，有能力对包含时序和实时控制需求的PLC系统进行规约描述。本课题将使用另一健全且在工业领域应用广泛的形式化语言B方法，用B语言对应用需求建模，总结开发模式,最终用开发结果对SPS4PLC的开发模式进行验证.
- 课题关键问题及难点：
由于B方法是基于一阶逻辑的基于状态的语言,而PLC是基于时间逻辑的,所以用B方法对PLC应用需求建模可能会产生无法证明的义务(B方法开发过程中会对模型里的动态行为产生证明义务),所以要考虑用B方法的特性规避这样的情况,总结出开发模式.
对于B方法的软件Atelier B,虽然该软件自动生成证明义务,但是会有一些软件无法证明的义务,所以要学会区分哪些的义务是正确的,哪些是错误的,且学会构建无法证明义务尽量少点模型 - 文献综述（或调研报告）：
B方法是一种比较实用的软件形式化方法，利用抽象机来描述软件的规格说明，通过一系列精化步骤进行设计，产生层次性体系结构及代码，覆盖了冲规格说明到代码生成的整个软件开发周期。这种方法能够严格地进行形式化规格说明的正确性证明，使得 B方法编写的规格说明具有精确性、无二义性、一致性、能进行推理等特点，其已在欧美多国的多个领域得到成功的应用。
在《B方法》一书中，作者详细论述了B方法的数理逻辑和集合论、抽象机理论、广义代换和精化模型以及举例，同时还针对活性问题做了详细的讨论和举例，使得B方法这一建立在严格的数理逻辑的形式化语言具有严格的规范和标准，适合做有高安全性需求的软件系统开发。
现在已有文献做出了B方法验证PLC程序的工作：
《An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting》一文介绍了一种证明PLC程序的方式。这篇文章通过自动地将PLC程序转化为B方法标准，以此来形式化的证明应用的安全性限制和普遍的构造性性质。作者提出了一种工具，这种工具将一个PLC程序转化为一个中间模型，这个模型自动地翻译为一个B语言表示对形式化模型。额外的安全性现实要求然后就会通过定理证明来添加和证明，由此来避免状态个数爆炸的问题。同时也可以精化和证明动态性质，比如死锁问题，通过使用工具proB来进行模型检测，这个工具至此定义和证明LTL的规约。由此可以证明PLC再它的扫描周期内进行所期望的动作。
《Formal verification of PLC programs using the B Method》一文中也类似地提出了将PLC直接转化为B方法规范，这一转化方法的正确性依赖于模型的模拟验证，无法用证明的方式说明其正确性。
从上面的文章中可以看出PLC和B方法之间存在联系，有互相转化的可能。但是现在并没有用B方法直接生成PLC程序的方案，本课题将尝试用方法直接建立PLC程序模型并验证，然后直接转换为可靠性较高的PLC程序。
《例说PLC西门子S7-200系列》以及《西门子S7-200 PLC应用教程》所介绍的PLC开发方式中，都有对PLC基本的经典环节的总结与介绍，这些基本环节在PLC开发中有重要作用。其他的一些用形式化方法开发的方案都有描述PLC基本环节来构造整个PLC程序的方案，所以开发基本模式和构建PLC模型的方法是本课题的核心。
以上是毕业论文文献综述，课题毕业论文、任务书、外文翻译、程序设计、图纸设计等资料可联系客服协助查找。
