B方法在软件开发和学习中探讨.docVIP

B方法在软件开发和学习中探讨 　　0.前言 　　事实证明，形式化方法在软件开发的过程中以精确的数学语义为基础，能精确描述系统规范， 严格验证规范的性质， 从而更好地保证软件的一致性和可靠性。其B方法的设计目的更是为了规范软件开发的流程和可靠性，其开发的思想也值得在其他学习领域借鉴。本文在阅读相关文献的前提下，消化形式化方法的概念和B方法开发软件的基本思路和方法，并参考B方法的开发思想对当前本人的研究工作进行探讨。 　　1.形式化方法概述 　　形式化方法是基于数学方法来描述目标软件系统性质的一门技术，它用严格的数学符号和数学法则对目标软件系统的结构与行为进行有效地综合、分析和推理，它为系统的说明、开发和验证提供了一个框架，利于发现目标软件系统需求中的不一致性、不完整性、不确定性等方面的问题。目前流行的形式化技术有：有穷状态机、Petri网、Z语言、B方法。 　　1.1形式化方法在软件开发中的作用 　　首先是对软件要求的描述。软件要求的描述是软件开发的基础，比如说一般非形式化的描述很可能导致描述的不明确和不一致。如果描述的不明确和不一致导致设计、编程的错误，将来的修改所要付出的代价就非常大。形式化方法则要求描述的明确性，而描述的不一致性也就相对易于发现。 　　其次是对软件设计的描述。软件设计的描述和软件要求的描述一样重要。形式化方法的优点对于软件要求的描述同样适用于软件设计的描述。对于简单的系统，形式化的描述有可能直接转换成可执行性程序，这就简化了软件开发过程，节约资源和减少出错的可能性。 　　另外，形式化方法可以用于程序的验证，以保证程序的正确性。 　　1.2 B方法 　　B方法的开发从早期就是与工业界的实际应用一起进步的，在其发展过程中，人们就已经用它作为工具开发了一系列关键性的应用软件系统。一个早期的重要应用是巴黎地铁列车的信号系统，这一系统为减少刹车距离、提高整个地铁系统得安全作出了显著的贡献。B发展到今天，B方法所用的符号和方法支持大部分的软件过程：需求分析、规格说明、软件设计、实现和维护，以及分层软件的逐步构造的确认和验证是B方法的指导性原则。B方法对实际大型软件的开发起了很重要的作用。 　　使用B方法开发时，首先需要建模，用B的表示来描述系统变量的主要状态、属性及其在操作中的转变，为系统的实现书写规格说明，在此基础上逐步求精，直到产生一个系统的完整实现。该方法通过一组计算机辅助工具支持规约到实现的全过程开发工作，是一种广谱语言。B-Toolkit包含自动及交互的理论证明工具、一套软件开发工具：AMN类型检验器，规约动画，证明法则生成器，规约和代码生成器。所有开发工具都由一个公共平台支持：B-Tool。最后。通过模式匹配和规则重写机制，对形式化对象生成程序。B语言中结构化的机制像其他面向对象方法一样，增强了信息隐藏和数据封装，严密的部件接口控制确保了大型开发中各个部件的独立开发。 　　2.基于B方法的软件开发过程 　　B方法的设计目标是作为一种实用的软件形式化方法。作为其先驱的Z 和VDM 等方法，主要关注软件规范说明的描述和性质证明， 没有特别考虑支持基于它们的软件开发过程， 也没有考虑最终代码的自动生成等问题。而B方法则希望支持从规范说明到代码生成的整个软件开发周期。使用B方法开发软件，提倡从更抽象的描述层次开始进行开发， 先用抽象机描述软件系统的抽象结构和抽象功能， 而后对其进行逐步精化。B方法并不严格区分软件的抽象规范、设计和实现之间的差异， 软件规范及其后续的逐层精化都统一用抽象机描述。B方法支持采用从抽象到具体的逐步构造、逐步验证的分层开发方法进行软件开发。 　　3.B方法开发思想精髓及在学习中的应用 　　3.1 B方法开发思想之规范和精化 　　规范和精化是B方法在软件开发中的前提和重要工作，也是该方法的精髓所在。通过，不断的规范和精化，不断精确描述系统的需求，从一个概要的模型逐渐形成一个精确的软件模型，一个可靠、一致、经过严格验证的模型，为设计开发打下重要的基础。 　　3.2规范与精化在学习设计中的启示 　　从上面描述可知，B方法的开发思路适用于大多数的软件系统开发设计，即使B方法的具体技术不大适用，但是其开发思想中的规范和精化肯定有借鉴可可取之处。以本人接下来的研究工作涉密终端基本安全基线的监控方案的研究为例，要设计一个符合涉密终端安全需求的基本安全基线的监控管理系统。在这里仅是参考B方法的开发思想进行设计，由于对B方法的细节并没有掌握，因此没法用B方法对系统规范和精化。 　　首先是规范描述该系统。根据监控系统工作流程如下：当用户尝试访问预定义好的涉密文件和系统关键文件时，系统自动判断用户权限，禁止或者允许其对文件进行操作，同时记录用户的行为，记录在本地日志的同时上报服务器，使得有规范的管理和约束用