Synchronization And Deterministic Modeling And Verification Of Nuclear Reactor Shutdown Logic Based On SCADE

The reactor protection system is one of the most important systems of nuclear power plants.When the parameters related to reactor safety reach the threshold,emergency shutdown and safety special systems are triggered to ensure the safety of nuclear power plants.Reactor protection system security software may cause major nuclear leakage accidents,so the software must have high reliability and security.The manual code development of traditional software,the workload is huge,and it is easy to make mistakes,it is difficult to meet the high reliability of nuclear power security software security requirements.Previous foreign countries,there are also development methods for constructing logic through PLC ladder diagram and then manually translating into C code.Although V&V work is carried out to verify and confirm the software,it still can’t completely meet the software security requirements.Formal modeling is one of the important methods for the development of safety-critical systems.SCADE,a high-security application development environment developed by Estelle,France,provides a model-based formal modeling method with a strict mathematical theoretical foundation to achieve clear and unambiguous expression of system function requirements.Compared with traditional manual coding development,it greatly reduces the probability of ambiguity and ambiguity in the code,and can realize the logical trace of the requirements.SCADE provides high-security software developers with two development methods:data flow and security state machine.It can fully implement software function logic and provide model verification method,which greatly improves the correctness and security of the model.The ability to generate certified high-quality C code provides a complete process for critical software development.The fly in the ointment is that the SCADE tool has no time concept,and there is no targeted verification of the actual timing and delay problems.This paper studies the RTS software of reactor protection system development method based on SCADE.Based on RPR system research,it uses SCADE data flow modeling,static checking,functional testing,coverage analysis,formal verification and code generation tools to stop RPR.Based on the research of SCADE defects,this paper proposes a synchronization model and deterministic verification method for shutdown model of distributed RPR system.Synchronization verification of distributed RPR system was carried out by introducing the simulink tool.main tasks as follows:(1)According to the development status and future trends of nuclear reactor protection system,the structure,function and characteristics of the three generations of reactor protection system are introduced.At the same time,the V&V process of nuclear power safety software development is briefly described,the model development route is determined.and the shutdown is analyzed.The logic determines the software modeling requirements.(2)Explain the deterministic and synchronic mechanism of the SCADE tool.This paper introduces the deterministic and synchronic requirements of distributed RPR systems,and illustrates the shortcomings of SCADE for the synchronization design of distributed RPR systems.The SCADE uses the data flow modeling method to model the shutdown logic of nuclear reactor RPR systems and The submodel is system integrated.(3)Model deterministic verification,using SCADE tools to verify the consistency of the model and requirements by manually writing test cases for coverage analysis and formal verification.Synchronization verification of distributed RPR system mainly introduces simulink tool,adds delay to the input end,conducts comparative test,and finally verifies the synchronization of the model.(4)Through the SCADE KCG component,the certification level C code is generated for the built model,the characteristics of the SCADE generated code are briefly described,and the code is transplanted to the VS to simply run the test,which proves that the SCADE code is maintained under the requirement of high security.Availability.