原文传递
自动化集装箱码头系统分析、建模与验证
| 论文题名： | 自动化集装箱码头系统分析、建模与验证 |
| 关键词： | 自动化集装箱码头系统;系统分析;软件开发;信号传输;时间自动机模型 |
| 摘要： | 本文研究的对象是上海振华港机集团的自动化集装箱码头系统。自动化集装箱码头系统是包含有多种协同工作的运输设备，设备与控制中心之间有非常复杂信号通讯的实时系统。而在传统的软件开发方法中，需求及设计阶段的描述一般采用非形式化的自然语言来进行，这样不能精确地表达系统性质，不但在设计阶段很难发现系统中固有的缺陷，而且在实现阶段也不易被开发人员理解。为了解决这个问题，我们引入形式化的研究方法，对自动化集装箱码头系统进行分析、建模和验证，以提高整个设计的正确性，安全性以及可靠性。 本文主要讨论了如何将形式化方法运用于自动化集装箱码头系统开发，包括对系统的分析，对系统进行的形式化规约建模，以及形式化地描述系统的关键性质等。在章节中，本文详细分析了振华港机自动化集装箱码头系统及其工作流程，设计了卸箱过程中的信号传输机制，并对该过程中的关键因素进行抽象分析，建立相应的数学模型。再在此基础上对自动化码头系统中的岸桥（QC），低架桥平板车（TC），地面平板车（GC）和控制中心（CU）分别建立时间自动机模型，并撰写描述系统关键性质的形式化规约，包括可达性验证，安全性验证和活性验证。最后在模型检验工具UPPAAL中检验这些性质，以保证自动化码头系统能够较好地符合工程应用的需求。 |
| 作者： | 祖佺 |
| 专业： | 软件工程 |
| 导师： | 张苗苗;季向东 |
| 授予学位： | 硕士 |
| 授予学位单位： | 同济大学软件学院 |
| 学位年度： | 2009 |
| 正文语种： | 中文 |
检索历史
应用推荐
