摘要

多工位制卡流水线设备控制系统是一种相当复杂的计算机控制软件,要求能够使用工业控制机或PC机等一般计算机设备控制流水型设备的各工位的生产和协作,保证产品在各工位间传送、加工过程流畅,出错率低。本文采用形式语义及方法对金融领域卡片生产设备的通用系统服务框架进行研究和建模,以确保建立一个稳定、可移植性强的通用开发框架,通过这个通用开发框架,可以迅速高效地开发出针对某一特定机型的计算机控制软件。本文将使用线性时序逻辑语法对多工位制卡设备控制系统进行形式化语义描述和建模,主要针对整个制卡流程以及在卡片在一个模块中的状态这两个方面进行建模。通过形式语义的动作推理,验证了本模型是动作是可实现的,状态是可达的,为进一步的全面建模研究工作奠定了基础。

全文