软件可靠性模型,对于软件可靠性估测起着核心的作用。软件可靠性模型是当前软件可靠性工程研究中的热点问题之一。程序正确性证明可以象证明数学定理一样证明程序是正确的,它对于可信计算具有重要意义。数学机械化思想是我国古代数学的精髓,不同于西方数学的公理化思想,我们可以运用机械化思想考察程序正确性证明。本文对软件可靠性模型和程序正确性证明进行了创新性和探索性研究。主要内容为:1.用分形几何的方法分析了软件失效时间序列,发现了其中的分形关系,提出了分形软件可靠性模型,并将其应用于软件可靠性的预测,其模型较简单,却实验结果良好。2.利用分形模型与ARIMA模型在分析时间序列线性和非线性方面的优势,提出了软件可靠性分形与ARIMA的混合模型,得到比一般的单个软件可靠性模型预测更好的预测效果。3.将数学机械化的吴方法应用于程序循环不变量的计算和发现,其性能好于Grobner基方法。4.将吴方法应用于递归程序的正确性证明,通过计算而不是推导的方法,验证了递归程序的正确性。