论文部分内容阅读
随着社会对信息技术的依赖性日益增长，在至关重要 (critical systems) 系统中如何提高应用软件的可靠性成为一个紧迫的问题。目前，软件开发的形式化与自动化方法被认为是提高软件可靠性和正确性的有效方法。
在这种背景下，本文探讨了形式化方法在高可靠管理信息系统(MIS)中的应用。本文以薛锦云教授提出的一种实用的软件形式化开发方法PAR及其支撑平台(PAR平台)为基础，设计和实现了管理信息系统中的一个典型实例——全国计算机等级考试(NCRE)管理信息系统。在开发NCRE管理信息系统的过程中，我们用PAR方法提供的Radl语言形式化描述该系统的需求规约、对其中的核心算法进行了形式化推导或证明、用PAR方法提供的Apla语言描述抽象程序，利用在Apla嵌入的关系代数技术实现数据库查询操作。通过上述大量实际的工作，我们实现的NCRE管理信息系统可靠性得到了显著的提高。
本文创新之处体现在以下几个方面：
①深入探索了PAR方法在高可靠MIS中的应用。PAR方法在算法程序开发方面应用较多，本文首次将其应用到MIS中，设计和实现了NCRE管理信息系统。经过实践检验，PAR方法在提高软件可靠性方面很有成效。
②实现了MIS的半自动开发，提高了软件开发效率。本文采用Apla描述抽象程序，再通过PAR方法的支撑工具转换成可执行语言C++，节约了编写代码时间，提高了效率。
我们的研究证明：将PAR方法应用于管理信息系统开发，既降低了软件开发的复杂度，又提高了软件本身的可靠性和正确性。