Document Testing Method And Application Of Brake Control System Based On Model Checking

With the increasing complexity of the train control system requirements document,the traditional document testing method is gradually difficult to meet the requirements in terms of problem discovery and testing efficiency.Model checking is a formal verification technology used to verify the correctness of a finite concurrent system.It is an effective means to improve system reliability.This paper focuses on the shortcomings of traditional testing methods,combines model checking with software testing,and based on the formal modeling and verification of documents,the document test items are generated by counterexamples,which improves the automation level of document testing.The size of the state transition matrix increases exponentially with the complexity of the system.To solve this problem,this paper introduces the hierarchical structure into the state transition matrix to make it more expressive.First,a formal modeling of the demand document for the train brake control system is performed to effectively mitigate the state space explosion problem caused by the increase in the number of states and events.Based on the extended modeling method,the symbolic coding and property description rules of the system modeling are proposed,and the specification verification is performed based on the BMC technology.The reliability of this method is proved by modeling the actual project.The size of the LTL formula is a key factor affecting the scale of the BMC conversion formula.This paper first uses the equivalence of the LTL formula to simplify the property formula,then uses the on-the-fly conversion algorithm and the equivalence and reachability of the state in the automaton to compress the size of the automaton again to alleviate the problem of space explosion.On this basis,using the Garakabu II solver to formally verify the model and attributes,the counterexamples detected by the model are used as test cases of the requirements document,in order to effectively reduce the design workload of document test items.