计算机软件的不断发展,应用软件的规模和复杂性越来越大,从而对计算机应用软件安全性和可靠性提出了更高的要求。软件测试是为了发现软件产品中的缺陷,并对发现的缺陷进行纠正的过程,是保证和提高软件质量的重要手段,在软件开发中起着不可替代的作用,其关键与核心是测试用例生成。软件可靠性是评价软件质量的重要指标,是软件产品固有的特性。软件测试中,针对测试用例的生成以及可靠性的计算成为研究的重点。本文采用模型检测的方法生成测试用例。首先是建立源程序的Petri网模型,针对建立的模型,利用本文规定的转化规则,将Petri网模型转化为模型检测工具SPIN的输入语言Promela,利用线性逻辑公式(LTL)描述源程序的属性。通过分析SPIN的运行结果,可以得出和描述的属性不相符的反例路径,由此产生测试用例。通过对不同属性的验证,最后得出源程序总的测试用例集。可靠性计算方面,本文采用的是Nelson模型,软件测试之后通过对结果的分析,可以计算软件的可靠性。最后用一个ATM-Bank系统的实例来说明本文方法的现实意义。