Research and Application of Memory Space Deterministic Verification of Embedded Operating System Software in Nuclear Safety Level I&C System

For the digital I&C(for short I&C) system of nuclear safety level, nuclear power standards put forward deterministic intrinsic characteristics requirements for embedded software. The verification of embedded operating system software in deterministic characteristics is the key point and difficulty of safety software verification. By analyzing the deterministic requirements of nuclear power standards, this paper focuses on the deterministic verification of key memory resources. Aiming at the dynamic changing stack area that is difficult to verify, this paper proposes a verification method combining static scheduling tree analysis and dynamic self-diagnosis, and verifies the correctness of the static analysis method itself to ensure the correctness of the method. This verification method ensures the certainty of the preset stack space usage of the embedded operating system, so as to prevent the system failure caused by stack overflow during the running of the program.