研究了一个用于将集装箱从货船运输到码头的自动化系统。系统由控制中心及多种设备构成,并由控制中心选择合适的设备来运输集装箱。由于各设备是并发工作的,加之设备与控制中心间存在复杂的信号交换,故运用形式化方法清晰地对系统进行描述显得尤为重要。因此,应用模型检验工具UPPAAL,对自动化码头系统进行了系统建模和分析验证,从而确保了系统设计的效率和正确性。