基于UPPAAL的LKJ-15系统模式转换功能建模与验证研究  

Research on Modeling and Verification of Mode Transition Function of LKJ-15 System Based on UPPAAL

作　　者：李建雄 吉志军 罗飞豹 LI Jianxiong;JI Zhijun;LUO Feibao

机构地区：[1]中国铁道科学研究院集团有限公司通信信号研究所,北京100081 [2]北京华铁信息技术有限公司,北京100081

出　　处：《铁道通信信号》2023年第5期60-66,共7页Railway Signalling & Communication

基　　金：中国铁道科学研究院集团有限公司科研课题(2019YJ062);中国铁道科学研究院集团有限公司通信信号研究所科研课题(2021HT04)。

摘　　要：模式转换是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.

关 键 词：LKJ-15系统 形式化建模 自动机理论 模式转换 建模验证 

分 类 号：U284.48[交通运输工程—交通信息工程及控制]