自動化集裝箱碼頭系統(tǒng)分析、建模與驗證.pdf

1、本文研究的對象是上海振華港機集團的自動化集裝箱碼頭系統(tǒng)。自動化集裝箱碼頭系統(tǒng)是包含有多種協(xié)同工作的運輸設備，設備與控制中心之間有非常復雜信號通訊的實時系統(tǒng)。而在傳統(tǒng)的軟件開發(fā)方法中，需求及設計階段的描述一般采用非形式化的自然語言來進行，這樣不能精確地表達系統(tǒng)性質，不但在設計階段很難發(fā)現(xiàn)系統(tǒng)中固有的缺陷，而且在實現(xiàn)階段也不易被開發(fā)人員理解。為了解決這個問題，我們引入形式化的研究方法，對自動化集裝箱碼頭系統(tǒng)進行分析、建模和驗證，以提高整個設

2、計的正確性，安全性以及可靠性。 本文主要討論了如何將形式化方法運用于自動化集裝箱碼頭系統(tǒng)開發(fā)，包括對系統(tǒng)的分析，對系統(tǒng)進行的形式化規(guī)約建模，以及形式化地描述系統(tǒng)的關鍵性質等。在章節(jié)中，本文詳細分析了振華港機自動化集裝箱碼頭系統(tǒng)及其工作流程，設計了卸箱過程中的信號傳輸機制，并對該過程中的關鍵因素進行抽象分析，建立相應的數(shù)學模型。再在此基礎上對自動化碼頭系統(tǒng)中的岸橋（QC），低架橋平板車（TC），地面平板車（GC）和控制中心（CU）