Software Reliability Model Based On Fractal And Mathematic Mechanization Of Program Correctness Proof

Software Reliability Models (SRMs) are the kernel of software reliability estimation and prediction. They are the key of software reliability engineering research. Software test can find errors, but can not find errors absent. And program correctness proof can guarantee this and it is very important to dependable computing. Mathematic mechanisation is soul of ancient mathmatics of China, which is different from western mathematic axiomzation. We can apply mathematic mechanisation to program correctness proof.In this thesis, new methods and analyses are explored and investigated for software reliability models and program correctness proof, which are described as follows:1. Apply fractal geometric methods to analysis of software failure time series, and discover self-similarities. We propose a fractal software reliability model, and use it to predict software failures and validate its efficiency.2. Fractal model and ARIMA model have their respective advantages in linear and nonlinear component of time series. We propose hybrid model of fractal and ARIMA and its efficiency is superior to other models.3. Apply Wu's method of mathematic mechanisation to computation of program loop invariant and its efficiency is superior to Grobner base method.4. Apply Wu's method to recursive program correctness proof and prove its correctness through computation method instead of logical deduction method.