基于线性时序逻辑的制卡流水线控制系统建模研究
2017-09-07沈阳齐德昱
沈阳+齐德昱
摘要：多工位制卡流水线设备控制系统是一种相当复杂的计算机控制软件，要求能够使用工业控制机或PC机等一般计算机设备控制流水型设备的各工位的生产和协作，保证产品在各工位间传送、加工过程流畅，出错率低。本文采用形式语义及方法对金融领域卡片生产设备的通用系统服务框架进行研究和建模，以确保建立一个稳定、可移植性强的通用开发框架，通过这个通用开发框架，可以迅速高效地开发出针对某一特定机型的计算机控制软件。本文将使用线性时序逻辑语法对多工位制卡设备控制系统进行形式化语义描述和建模，主要针对整个制卡流程以及在卡片在一个模块中的状态这两个方面进行建模。通过形式语义的动作推理，验证了本模型是动作是可实现的，状态是可达的，为进一步的全面建模研究工作奠定了基础。
关键词：形式语义；多工位；建模；线性时序逻辑
中图分类号：TP316 文献标识码：A 文章编号：1007-9416（2017）05-0083-03
现今现代流水型多工位加工设备的控制系统存在以下不足：（1）系统设计开发思路仍然停留在“一机一程序”的时代（PC或PLC程序亦然）；（2）未能适应除机械标准件以外其他自定义部件的快速替换；（3）机器控制代码难以复用与重构，存在不必要的重复或冗余；（4）勉强复用或扩展现有代码导致思路局限，可能带来功能上的隐患；（5）与外部系统缺乏足够丰富的交互接口，难以与新技术集成（如云计算，自诊断）；（6）缺乏领域专用的设计，开发和仿真测试工具。
总而言之，其根源在于缺乏一个以形式化理论支持的领域专用软件框架。我们面对的问题是：一个怎样的程序结构（框架）才能满足现代流水型加工设备控制系统的需要？作为这类设备的设计与制造商，需要不断根据产品及用户的需求，来设计与生产各种各样的设备，因此有必要研发一种通用设备服务来支持实现这种流水型多工位系统的要求，并具有很强的开放性和扩展性。如果采用UML的方式对该系统建模，尽管其静态语义由元模型给出，但其动态语义却十分模糊，不利于对其所描述的需求进行形式化的验证和确认，本文将采用线性时序逻辑对流水型加工设备控制系统中的部分功能进行形式化建模和验证，以保证其无二义性以及准确性[1]。
1 使用线性时序逻辑语法描述制卡流程
流水型多工位设备的包括：启动、重置系统、格式化、数据加载、打印、过卡等多个子过程。主要功能描述如下[2]：
（1）启动：各组件实例化，系统进行初始化。（2）重置系统：要求对整个流水线进行清理，包括清理残存在系统中的卡片、清空数据和状态等。（3）格式化：将客户端卡片设计软件中生成的卡片模板（XML文件）与相关变量进行映射并发送到服务器端。（4）打印：该环节最为复杂，机器对卡片的打印包括多个流程，如发卡、打凹凸字，热转印、烫金、写磁、出卡等。本节主要选取打凸字的过程作为线性时序逻辑描述的目标。（5）过卡：只让卡片从发卡器到出卡端整体过一遍，并不进行打印的过程，作用是确保流水线通道通畅[3]。
除上述子过程之外还是铣槽、IC片加密等过程就不再一一赘述。
打凹凸字过程的顺序图如图1所示，整个打凹凸字过程中涉及到的对象有：操作员，Client，ModuleServer，Service，工位，分别记为：w，c，ms，sv，pos。
我們用这样一个四元组来表示这个顺序图：SD=
Obj=< w， c， ms， sv， pos >
Msg=
Loc={
F（m1，s）=
F（m2，s）=
F（m3，s）=
F（m5，s）=
F（m7，s）=
F（m9，s）=
F（m11，s）=
使用LTL对该顺序图主要事件进行形式化表示的语义描述如下：
2 使用线性时序逻辑语法描述单一模块中的卡片状态
制卡过程中的卡片状态图2所示，对于制卡过程中，卡片的状态图是最需要关注的，包括重置系统、制卡、过卡等多种状态。本节将选取在制卡过程中卡片状态的转换这个过程，用线性时序逻辑反映卡片状态以及相关的逻辑验证[4]。
各状态含义[5]：（1）DEMAND状态：卡片已经准备就绪，可以制卡。（2）ACTIVE状态：制卡过程中的复合状态。（3）ACK状态：系统响应卡片请求，由于制片过程与机器的交互是一问一答。首先要收到机器返回的ACK状态才到进行下一步操作。（4）RETRY状态：机器由于某种原因暂停工作，卡片进入重试状态。（5）COMPLETE：机器遇到某些不可恢复的错误，卡片进入完成状态。（6）FINISH：制卡过程结束。
制卡时，卡片首先进行初始化操作，以确定是否准备就绪，然后立即进入DEMAND状态。当接到doServiceProcess事件时，接收到机器的ACK响应后，进入激活状态（ACTIVE），ACTIVE无条件进入ACK状态。在ACK状态中进行等待阻塞，监听机器返回的消息，如果是retry，卡片进行TRETRY状态，如果是ok，则进入FINISH状态，如果是error，卡片进入COMPLETE状态。在RETRY状态中，当接到doServiceRecoverOnRetry事件，则进入ACK状态。在COMPLETE状态中，当接到doServiceDeplyOnComplete事件时，卡片也进入FINISH状态[6]。
该状态图的静态语义形式化如下：
图2所示的状态，设转换动作为Translate，状态集类为States，则可形式化如下：
对应的部分语义为：
3 可达性验证
根据2，3节建立的形式语义模型，该模型形式语义的动作推理如下[7-8]：
对于动作（包括上述的原子动作或复杂动作），如果存在解释和，使满足，则称动作是可实现的。
状态的可达性：（1）如果动作满足以下条件，则称状态是可达的；（2）如果动作是可实现的，则状态是可达的；（3）假设有动作和，如果和都可实现，则状态是可达的。
例如上述形式化中的，有，由于都是可实现的，所以是可实现的，可知状态是可达的。状态图中具备可达性的状态有：INITIALIZE， DEMAND， ACTIVE， COMPLETE， FINISH。
4 结语
使用UML描述图形简单明了，但无法分析和验证系统模型的一致性和准确性。使用UML+形式化方法进行该通用开发框架的建模，可以使系统架构的清晰，同时能够保证模型的正确性和健壮性。多工位制卡流水线设备控制系统建模一直是业界不断研究和探讨的课题，本文采用线性时序逻辑语法描述流水线整个制卡流程以及一个工位中的卡片状态，以提高流水线控制系统分析设计的准确性和安全性，为进一步形式化打下基础。下一步研究将通过全面形式化流水线建模，为流水型产品加工装备软硬件的组态化研究打下基础。
参考文献
[1]戎玫，张广泉.UML顺序图的一种形式化描述方法[J].重庆师范大学学报（自然科学版），2007（3）：528-532.
[2]丁明.基于线性时序逻辑的业务流程验证[J].西北大学学报（自然科学版），2012（2）：226-230.
[3]蒋慧，林东.UML状态机的形式语义[J].软件学报，2002（12）：2244-07.
[4]HUANG Xuemei. Modeling and Analysis for Hybrid Dynamic System of Production Line in Integrating Matlab Environment[J]. Modular Machine Tool & Automatic Manufacturing Technique， 2013， 5（5）：9-11.
[5]SEMANCO P， MARTON D. Simulation tools evaluation using theoretical manufacturing model[J]. Alta Polytechnical Hungarica，2013（2）：193-204.
[6]BECKERT， MEYERM， WINDTK. A manufacturing systems network model for thee valuation of complex manufacturing systems [J].International Journal of Productivity and Performance Management，2014（3）：324-340.
[7]LIJ. Modeling and analysis of manufacturing systems with par-allellines[J]. IEEE Transactions on Automatic Control，2004（10）：1824-1829.
[8]辛宗生，魏國丰.自动化制造系统[M].北京：北京大学出版社，2012.endprint
