| Safety critical control system is a kind of system which requires high reliability and safety.Its normal operation depends on correct function control logic and configuration data.Such configuration data is called safety critical data,and such function control logic includes the various safety critical function scenarios.Therefore,it is very important to use effective ways to ensure the accuracy of safety critical data and safety critical functional scenarios.Formal methods are used to find errors and defects in various data and functional scenarios of the system,so as to improve the system design and achieve the purpose of enhancing the reliability and safety of the system.The main research work of this paper are as follows:(1)Taking safety critical data as the research object,the data of railway signaling equipment such as point,railway signal,section and route are selected as the research cases.Based on the topology data structure of each safety critical data,the static rules that each safety critical data needs to satisfy are firstly described with natural language,and then Atelier B is used to establish formal model of the static rules that the data need to meet,and a static formal model is generated.Finally,ProB model checking tool and Graphviz visualization graphics software are used to verify and analyze whether each generated safety critical data satisfies the static rules.In the research process,considering the huge amount of data that has been generated,Epsilon scripting language which supports format of Z language is used to construct transferring model to achieve the data to be automatically imported into the formal model.(2)Taking the safety critical function scenarios as the research object,the functional logic flow of the level crossing control system with safety risk characteristics was selected as the research case,the functional design specification was analyzed,and each basic function scenario and safety scenario were obtained.The semi-formal model of each basic function scenario was first modeled by Simulink/Stateflow tool.Then,the Aterlier B modelling tool was used to obtain the formal model of each basic functional scenario,and the invariant was used to describe the safety attributes.ProB model checking tool was used to check whether the functional model satisfy the invariant,and interactive proof of the generated proof obligation was completed by combining with the interactive proof platform built in Atelier B.The above semi-formal model and formal model are used to generate the executable code.Based on basic functional scenarios and the defects that are exposed in the formal verification process,the scenario method and error estimate method of the software test are used to design the test cases.The BTC Embeded System commercial testing&verification platform is used to test the generated codes.The testing results show that the established semi-formal model has realized all the basic functions,but there are explicit defects that violate the safety attribute and implicit defects caused by inadequate modelling,and there is one basic function that has not been realized in the established formal model.Based on the test results,to some extent,the semi-formal modelling method is more likely to build a model with higher practicability,and the formal modelling method is more likely to build a model with higher safety.This paper has realized the modelling,verification and testing of safety critical data and safety critical functional scenarios,which provides a reference for how to improve the correctness of data,reliability,safety and practicability of the model in the process of system modelling and development. |
