基于UPPAAL的集装箱码头系统的设计、建模与验证.pdfVIP

学兔兔 l 匐 化 基于UPPAAL的集装箱码头系统的设计、建模与验证 Designing，modelling and verifying a container terminal system using UPP从 L 胡学青’，张学舟 ，祖 俭 HU Xue．qing。。ZHANG Xue—zhou ，ZU Quan (1．宿州学院机械与电子工程学院，宿州234000 2．同济大学软件学院，上海201804) 摘 要：研究了一个用于将集装箱从货船运输到码头的自动化系统。系统由控制中心及多种设备构成， 并由控制中心选择合适的设备来运输集装箱。由于各设备是并发工作的，加之设备与控制中 心间存在复杂的信号交换，故运用形式化方法清晰地对系统进行描述显得尤为重要。因此， 应用模型检验工具UPPAAL，对自动化码头系统进行了系统建模和分析验证，从而确保了系 统设计的效率和正确性。 关键词：自动化集装箱码头；形式化方法；模型检验；时间自动机；UPPAAL 中圈分类号：TP27；U691 文献标识码：A 文章编号：1 009-01 34(201 3)04(上)-01 02-04 Ooi：1 0．3969／J．issn．1 009-01 34．201 3．04(上)．32 0 引言 运输集装箱。每个集装箱包含堆场的目标位置信 集装箱码头系统是通过各种设备将集装箱从 息，且每条GC轨道对应堆场的固定区域，故易知 货船运输到码头的系统。本文研究的是上海振 哪台GC将投入工作。算法计算并对比每台TC的卸 华港机有限公司 (ZPMC)旗下的自动化集装箱 箱时间，找出用时最短的TC。 码头系统 (ACTZ)。该系统由4台岸桥起重机 SHIp (QC)、5台低架桥平板车 (TC)和7台地面平板 口“ 车 (GC)组成。此外，引入控制中心 (CU)来控 制设备的运转。为避免设备间的碰撞，每台设备 都被设计在各自轨道上运行。轨道以三维方式安 装，以减少空间占用。 本文设计了一个调度算法，由CU执行，以 图1 ACTZ的布局 选择合适的设备运输集装箱。设备通过PLC信号 下面，将详述序号为C的集装箱的卸载过程。 与CU通信。当CU收到某设备发来的信号时，会 假设已选定序号为q、t、g的Qc、TC和GC参与运 作出判断并回发信号，触发设备的下个动作。由 输。用P(q)表示QC[q]从船上提箱的位置，P(q一t) 于各设备是并发工作的，加之设备与控制中心间 表示QC[q]将集装箱传给TC[t]的位置，P(t一g)表示 存在复杂的信号交换，故本文运用形式化方法为 TC[t]将集装箱传给GC[g]的位置，P(g)表示GC[g】 ACTZ建模和分析，来确保系统设计的正确性。