计算机科学 ›› 2015, Vol. 42 ›› Issue (1): 193-195.doi: 10.11896/j.issn.1002-137X.2015.01.043

• 软件与数据库技术 • 上一篇    下一篇

基于场景的联锁软件形式化模型生成方法

董昱,高雪娟   

  1. 兰州交通大学自动化与电气工程学院 兰州730070,兰州交通大学自动化与电气工程学院 兰州730070
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受基于受控拉格朗日函数的多欠驱动度力学系统控制器设计(61164010)资助

Method for Generating Formal Interlocking Software Model Based on Scenario

DONG Yu and GAO Xue-juan   

  • Online:2018-11-14 Published:2018-11-14

摘要: 为保证列车运行安全和旅客生命财产安全,对车站联锁控制系统进行有效的分析、验证和测试是必不可少的,而形式化模型是联锁系统分析、验证和测试的基础。以计算机联锁软件的UML半形式化模型为基础,以事件确定有限自动机模型作为描述系统的形式化模型,研究UML2.0顺序图转换为事件确定有限自动机模型的方法。首先选取一组与交互行为相关的全局变量作为状态向量来分析和消解顺序图各个场景的消息以及不同场景间的同一消息的前后置状态向量值是否存在矛盾,从而得到一致性的需求场景;然后提取各对象的事件序列生成对应的事件确定有限自动机;最后通过组合系统中对象的自动机模型得到系统的事件确定有限自动机模型。该方法改善了安全苛求软件的设计与开发,为软件质量评估提供了技术支撑。

关键词: 计算机联锁软件,事件确定有限自动机,顺序图,场景分析

Abstract: 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 methodtransforming 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 genera-ted.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.

Key words: Computer interlocking software,ETDFA,Sequence diagram,Scenario analysis

[1] 张曙光.高速铁路系统生命周期安全评估体系的研究[J].铁道学报,2007,9(2):20-26
[2] The European Committee for Electro-technical Standardization.EN 50126 Railway Applications-the Specification and Demonstration of Reliability,Availability,Maintainability and Safety(RAMS)[S].UK:BSI,2002
[3] CENELEC.EN 50128 Railway Applications:Communi cations,signaling and processing systems-Software for railway control and protection systems[S].UK:CENELEC,2001
[4] CENELEC.EN 50126 Railway Applications:The specification and demonstration of Reliability,Availability,Maintainability and Safety(RAMS) [S].UK:CENELEC,1999
[5] IEC.IEC61508 Functional Safety of electrical/ electronic/programmable electronic safety- related systems-part3:software requirements[S].UK:IEC,2000
[6] IEC.IEC61508 Functional Safety of electrical/ electronic/programmable electronic safety- related systems-part7:Overview of techniques and measures[S].UK:IEC,2006
[7] 王曦,徐中伟,梅萌.基于模型检测的软件安全性验证方法[J].武汉大学学报,2010,6(2):156-160
[8] Haxthausen A E,Peleska J.Formal Development and Verifica-tion of a Distributed Railway Control System[J].IEEE Transactions on Software Engineering,2000,6(8):1546-1563
[9] Garmhausen V H,Campos S,Cimatti A.Verification of a safety-critical railway interlocking system with real-time constraints[J].Elsevier Science of Computer Programming,2000(36):53-64
[10] Yang Shuang-hua,Yang Li-li.Automatic safety analysis of control systems[J].Journal of Loss Prevention in the Process Industries,2005,8(3):178-185
[11] Bozzano M,Villa-orita A.The FSAP/NuSMV-SA Safety Analy-sis Platform[J].Software Tools for Technology Transfer,2007,9(1):5-24
[12] Koh K Y,Seong P H.SMV model-based safety analysis of software requirements[J].Reliability Engineering & System Safety,2009,4(2):320-331
[13] 赵志熙.计算机联锁系统技术[M].北京:中国铁道出版社,1999:20
[14] Booch G,Rumbaugh J,Jacobsn I.UML用户指南[M].邵维忠,译.北京:机械工业出版社,2001:59-78
[15] Kim H,Russell M.Learning UML 2.0[M].California:O’ Reilly,2006:1-286
[16] 张琛,段振华.应用UML2.0模型的测试用例生成方法[J].西安交通大学学报,2011,5(8):18-23

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!