摘要
为保证列车运行安全和旅客生命财产安全,对车站联锁控制系统进行有效的分析、验证和测试是必不可少的,而形式化模型是联锁系统分析、验证和测试的基础。以计算机联锁软件的UML半形式化模型为基础,以事件确定有限自动机模型作为描述系统的形式化模型,研究UML2.0顺序图转换为事件确定有限自动机模型的方法。首先选取一组与交互行为相关的全局变量作为状态向量来分析和消解顺序图各个场景的消息以及不同场景间的同一消息的前后置状态向量值是否存在矛盾,从而得到一致性的需求场景;然后提取各对象的事件序列生成对应的事件确定有限自动机;最后通过组合系统中对象的自动机模型得到系统的事件确定有限自动机模型。该方法改善了安全苛求软件的设计与开发,为软件质量评估提供了技术支撑。
It is necessary to do analysis,verification and test of station interlocking system to ensure the safety of train running and people lives.Especially,the formalized model is the foundation of these works This paper studied the method transforming the sequence diagram（SD） into the event deterministic finite automata（ETDFA） model which is based on UML semi-formal model of computer interlocking software,and used ETDFA as the formal model to describe the system.Firstly,a set of global variables associated with sequence diagram＇s interaction were selected as the sate vector to analyze and eliminate the contradiction in pre-value and post-value of message in every scenario and the same message among multiple scenarios,and then based on the sequence event of each object,corresponding ETDFA model was generated.At last,by composing all objects＇ ETDFA model,system＇s ETDFA formal model was got.The method improves safety software＇s designing and development and provides technical support of software quality.
出处
《计算机科学》
CSCD
北大核心
2015年第1期193-195,226,共4页
Computer Science
基金
基于受控拉格朗日函数的多欠驱动度力学系统控制器设计(61164010)资助
