计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
2期
222-225
,共4页
联锁软件%UML%顺序图%FSP%有限状态机
聯鎖軟件%UML%順序圖%FSP%有限狀態機
련쇄연건%UML%순서도%FSP%유한상태궤
Interlocking software%UML%Sequence diagram%FSP%Finite process machine
有效地测试、分析和验证计算机联锁软件是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础.以联锁软件的UML非形式化模型为基础,以有限状态机模型为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为有限状态机模型的方法.首先将场景的UML顺序图转化为FSP进程代数模型,然后通过合并不同对象的进程代数模型,得到系统的有限状态机模型.最后以接车进路用例为例生成系统的有限状态机模型,以验证该方法的可行性和有效性.
有效地測試、分析和驗證計算機聯鎖軟件是保證列車運行安全和旅客生命財產安全的重要手段,而形式化模型是繫統測試、分析和驗證的基礎.以聯鎖軟件的UML非形式化模型為基礎,以有限狀態機模型為繫統形式化模型描述的數學工具,研究UML順序圖(場景)自動轉化為有限狀態機模型的方法.首先將場景的UML順序圖轉化為FSP進程代數模型,然後通過閤併不同對象的進程代數模型,得到繫統的有限狀態機模型.最後以接車進路用例為例生成繫統的有限狀態機模型,以驗證該方法的可行性和有效性.
유효지측시、분석화험증계산궤련쇄연건시보증열차운행안전화여객생명재산안전적중요수단,이형식화모형시계통측시、분석화험증적기출.이련쇄연건적UML비형식화모형위기출,이유한상태궤모형위계통형식화모형묘술적수학공구,연구UML순서도(장경)자동전화위유한상태궤모형적방법.수선장장경적UML순서도전화위FSP진정대수모형,연후통과합병불동대상적진정대수모형,득도계통적유한상태궤모형.최후이접차진로용례위례생성계통적유한상태궤모형,이험증해방법적가행성화유효성.
