摘要
有效地测试、分析和验证计算机联锁软件是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。以联锁软件的UML非形式化模型为基础,以有限状态机模型为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为有限状态机模型的方法。首先将场景的UML顺序图转化为FSP进程代数模型,然后通过合并不同对象的进程代数模型,得到系统的有限状态机模型。最后以接车进路用例为例生成系统的有限状态机模型,以验证该方法的可行性和有效性。
It is an important way to make sure the safety of train running and passengers' life and property by effectively testing, analyzing and validating computer interlocking software. Formal model is the foundation of system testing, analyzing and validating. Based on interlocking software's UML informal model, using finite state machine model as the mathematical tools to describe system formal model, this paper studied the method to traverse the UML sequence dia- gram or scenarios to finite state machine model. Firstly the UML sequence diagram was traversed to FSP process ma- thematical model, and then systematic finite state machine model was obtained by merging all objects' process math- ematic models in the UML sequence diagram. Finally, the case of controlling of entry routes was used to generate systematic finite state machine model to invalidate the feasibility and effectiveness of this method.
出处
《计算机科学》
CSCD
北大核心
2014年第2期222-225,共4页
Computer Science
基金
基于受控拉格朗日函数的多欠驱动度力学系统控制器设计(61164010)资助
关键词
联锁软件
UML
顺序图
FSP
有限状态机
Interlocking software, UML, Sequence diagram, FSP, Finite process machine