An Research for Formal Verification of Safety-Critical Software

摘要：

　　A verification methodology is presented for railvayinterlocking system which is regarded as a safety-critical system.The methodology utilizes UML to model the function requirement and LTL to verify the safety requirements of the specification.The device specifications of railway interlocking system are modeled with UML,then translate into FSM.The safety specification is translated LTL and analyzed with NuSMV.We try to show the feasibility of improving the reliability and reducing revalidation efforts when designing and developing a decentralized railway signaling system.

关键词： Safety Critical Software FSM LTL UML

作者: Weigang Ma Xinhong Hei

作者单位: Key Laboratory of Computer Networks and Information Security(Ministry of Education), Xidian Universi School of Computer Science and Engineering, Xian University of Technology, Xian, 710071, China

会议类型: 国际会议

会议名称: 2012 2nd International Conference on Computer Application and System Modeling(2012第二届计算机应用与系统建模国际会议)(ICCASM-2012)

会议地点: 沈阳

会议语种:英文

页码: 836-839

在线出版日期: 2012-07-27（万方平台首次上网日期，不代表论文的发表时间）