PAR方法在构建高可靠管理信息系统中的应用研究

论文摘要

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

论文目录

• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 管理信息系统概述
• 1.2 管理信息系统的可靠性
• 1.3 软件可靠性研究现状
• 1.4 本文研究内容
• 1.5 本文创新
• 1.6 本文结构
• 第二章 PAR 方法概述
• 2.1 软件可靠性与形式化方法
• 2.2 软件形式化的国内外研究现状
• 2.3 PAR 方法
• 第三章 NCRE 管理信息系统的需求与设计
• 3.1 需求说明与形式化方法
• 3.2 部件技术
• 3.3 NCRE 管理信息系统需求规约的形式化描述
• 3.4 NCRE 管理信息系统系统设计
• 3.5 NCRE 管理信息系统数据库表结构
• 第四章 高可靠NCRE 管理信息系统的实现
• 4.1 NCRE 管理信息系统的APLA描述
• 4.2 基于关系代数的数据库操作
• 4.3 NCRE 管理信息系统核心算法形式化推导
• 4.4 用APLA 描述的NCRE 管理信息系统的自动转换
• 第五章 总结
• 参考文献
• 致谢
• 攻读硕士学位期间参与的课题