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

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

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