在众多保障软件可靠性和安全性的途径中,采用形式化方法对系统进行形式化验证和分析是被很多计算机科学家所认同的。形式化验证主要包括两类方法:一是以逻辑推理为基础的定理证明,另一是以穷尽搜索为基础的模型检测。二者相比,前者自动化程度弱于后者,但因其表达力较强,加之自动定理证明技术的日益进步,它依然有着较好的应用前景,值得人们对其进行深入探讨。目前大多数的程序验证过程是顺序地按每一条验证规则进行验证。由于验证过程中的并发构造特性没有被充分挖掘出来,这种顺序验证方法严重地制约了验证工作的效率,尤其在验证大型程序时愈发明显。所以,从提高验证过程的并发度的角度来研究提高程序验证的效率一件很有意义的事。软件行业是一个快速发展的行业,大量的新旧技术的交替造成了大规模的遗留系统。针对遗留系统的处理有两种方法,要么设计新的系统去替换,要么对其进行再工程。由于遗留系统存在技术陈旧、系统结构混乱、文档缺失和维护成本高等问题,越来越多的企业和组织采用新技术将遗留系统再工程到新的软件或硬件平台,以提高系统的可靠性、可重用性、可维护性和运行性能。任何先进系统最终都成为遗留系统,所以良好的系统结构设计方案和系统可扩展性在再工程中将显得越来越重要。早期系统大多数采用面向过程方法编程,而面向过程编程的特点是注重功能的实现,业务过程和系统的操作方法联系的比较紧,不利于系统的维护和升级。所以把注重功能实现的面向过程系统转换成注重结构设计的面向对象系统,以期利用面向对象的特征来提高系统的可扩展性的研究变得有意义了。任何事物之间都是有联系的,利用事物间的依赖关系开展有关理论与应用研究既有普遍的现实意义,也有潜在的学术价值。为此本文把依赖分析应用到了并行化程序验证策略和遗留系统改造中,主要完成了以下几项工作:1.提出了一种提取While程序控制结构的算法,用实验证明该算法的正确性,并对该算法做了简要的分析。2.在获取程序控制结构依赖关系的基础上,提出一种基于依赖分析的并行化验证策略,进一步提高程序的验证效率,并用实验证明了该方法的有效性。3.把依赖分析思想应用到由面向过程系统转换成面向对象系统的遗留系统改造过程中,提出了基于依赖分析的程序模块划分方法,改进了主域变量的识别方法,最后把该思想应用到了While程序转换成Java程序的实例中。