摘要
模式转换是LKJ-15系统的重要功能。为了保证模式转换功能安全,提出利用形式化建模工具UPPAAL对该功能进行建模与验证。首先分析LKJ-15系统各种模式转换条件,建立模式转换信息交互网络;之后使用UPPAAL建立模式转换功能模型;最后对模型进行仿真和BNF语句验证。结果表明:该模型满足LKJ-15模式转换的功能要求,其安全性得以验证,为系统开发和应用提供了理论保障。
The mode transition is an important function of the LKJ-15 system.To ensure the safety of the mode transition function,this paper models and verifies the mode transition function based on the formal modeling tool UPPAAL.Firstly,various mode transition conditions of the LKJ-15 system are analyzed,and a mode transition information exchange network is built.Secondly,the model of mode transition function is established by UPPAAL.Finally,this model is simulated and verified with BNF statement.The results show that the model meets the functional requirements of LKJ-15 mode transition,and its security is verified,which provides a theoretical guarantee for the development and application of the system.
作者
李建雄
吉志军
罗飞豹
LI Jianxiong;JI Zhijun;LUO Feibao
出处
《铁道通信信号》
2023年第5期60-66,共7页
Railway Signalling & Communication
基金
中国铁道科学研究院集团有限公司科研课题(2019YJ062)
中国铁道科学研究院集团有限公司通信信号研究所科研课题(2021HT04)。