一个关于PLC软件确认的模型检验概况

一个关于PLC软件确认的模型检验概况(中文20000字,英文PDF)
摘要：可编程控制器在工业控制系统中有很大的使用由于它的高的同步输入/输出处理性能。PLC程序被用在临界系统，并且为了恰当的工作PLC软件需要与实时约束保持一致。因为PLC程序需要执行低级指令或者像汇编语言，在PLC软件产品最重要的一点是模拟使用了像皮特网或者自动装置的正规途径。后来PLC软件被半自动化的生产从模型和精简的迭代。一方面模型校验是一个闻名的软件核查方法，典型地一系列实时属性通过随手从软件模型中开发转化的系统被核实。明显地，软件校验应用一系列不同的方法去核实基于PLC软件的正确性。
在这篇文献中我们提供了一个广泛的观点关于在模型校验应用在PLC软件产品过程期间中遇到的困难。我们从两个不同的观点分类方法：第一,模型检查方法/工具适用在验证过程,第二,软件模型/来源
代码及其转换模型检查器的规则语言。简而言之，我们主要考察SPIN，SMV和UPPAAL为基础的模型检测活动，使用模型构建指令列表（和相似），功能化方框图和Petri网/自动机为基础的模式建筑活动。作为我们研究的结果，我们提供在研究中，在文学方面的比较像他们的应用领域，性能CON-各方面siderations和模型检验的过程。我们的调查可以可用于为学者和从业者提供指导计划模型检测集成到基于PLC软件的核实活动。
关键词：模型检验可编程逻辑控制器计划核实