Formal Modeling And Verification Of OTN Protection Switching System

The application of OTN(Optical Transport Network)technology in the field of communication greatly improves the transmission speed of information and reduces the bit error rate.OTN ensures that information transmission is not interrupted through the protection switching system,so the reliability of the protection switching system needs to be guaranteed.In the optical transport network,the protection switching system needs to meet the requirements of different application scenarios based on the APS(Automatic Protection Switching)protocol.This requires verifying that the design follows the APS protocol and meets the needs of the scenario during the system design phase.However,during the design phase of the protection switching system,few people pay attention to the formal definition of this stage,and the protection switching system fails to meet the requirements and agreements.A large part of the reason is that the definition of the requirements is ambiguous or missing.Traditional modeling methods,including flowcharts,state diagrams,and timing diagrams,cannot solve the ambiguity and omission of requirement definition,which makes huge hidden dangers in the subsequent development of system.Moreover,for increasingly complex systems,verification of systems has become increasingly difficult due to state space explosion problems.A formal method is proposed based on two-dimensional table structure to define system requirements,which can minimize the ambiguity and omission of demand definition.The basic idea of the method is derived from the state transition matrix,the first row of the table structure named source states row,representing the all possible states of the corresponding system;the first column is the target states column,which represents the target states that the system may reach from corresponding source state.The position determined by the intersection of the source state and the target represents the action that the system will meet under certain conditions in the current source state.For the verification of STF model,the method of boundary model checking is adopted.The STF model and the properties to be verified are symbolized and input into the SMT solver for verification.Thereby completing the formal modeling and verification process of the embedded software system.Then,based on the existing automaton state compression algorithm,this paper proposes a state compression algorithm based on STF model.Based on the STF model,this method can compress the large STF model into a smaller STF model through simple matrix transformation.The time taken for symbolic coding and property verification on the basis of the compressed STF model is reduced to some extent.Finally,the SMT solver Z3 and UPPAAL tool are used to verify the effectiveness of the algorithm.