PCNN has been widely used in image segmentation. However, satisfactory results are usually obtained at the expense of time-consuming selection of PCNN parameters and the number of iteration. A novel method, called grayscale iteration threshold pulse coupled neural network (GIT-PCNN) was proposed for image segmentation, which integrates grayscale iteration threshold with PCNN. In this method, traditional PCNN is simplified so that there is only one parameter to be determined. Furthermore, the PCNN threshold is determined iteratively by the grayscale of the original image so that the image is segmented through one time of firing process and no iteration or specific rule is needed as the iteration stop condition. The method demonstrates better performance and faster compared to those PCNN based segmentation algorithms which require the number of iterations and image entropy as iteration stop condition. Experimental results show the effectiveness of the proposed method on segmentation results and speed performance.

There is increasing pressure on providing a high degree of assurance of operation system’s security and functionality. Formal verification is the only known way to guarantee that a system is free of programming errors. We study on formal verification of operation system kernel in system implementation level and take theorem proving and model checking as the main technical methods to resolve the key techniques of verifying operation system kernel in C implementation level. We present a case study to the verification of real-world C systems code derived from an implementation of μC/OS – II in the end.