[01247776]B方法与形式化软件开发技术研究

随着对软件开发过程研究的深入，人们认识到形式化方法是提高软件质量和可信性的重要途径。

虽然 形式化方法作为可信软件实现的重要技术已经取得了一定的成功，但是与面向对象技术相比，其实用性还存在一定差距。

而目前的软件开发，仍以非形式化软件开发方法为主流，基于形式化方法的高可信软件的开发基本处于实验室的试验阶段，不能满足高可信软件开发的需要。

为此，本研究以可信软件开发为研究对象，通过对可信软件的开发过程作系统的分析、研究，提出一套基于切片技术的面向对象与B方法相结合的新的软件开发模式，解决目前开发方法中的不足，使形式化软件开发技术真正走出实验室，为形式化软件开发的应用提供理论和技术指导，保障软件开发过程的可控性和目标软件的可靠性。

该项研究包括以下几个方面：（1）研究了B方法的形式化软件开发过程，给出了支持B方法的软件体系结构的开发模式，完成了面向对象技术与B方法相结合的软件开发框架。

（2）实现了使用B方法完成软件开发过程中的抽象规范模型到一个具体模型的转换，得出了软件系统的一个形式化设计模型，解决有效控制软件开发过程中的不可控和不精确等问题。

实现了类图、对象图、状态图、协作图、活动图等五种UML模型图的形式化描述，建立了UML模型图到B方法形式规约的映射关系，以充分发挥UML模型和B方法的各自优势，取长补短，既保留了利用UML进行系统分析设计时强大的系统建模能力和简洁明了的面向对象模型表示法，又能够形式化的对软件模型的求精过程进行验证。

重新定义了软件体系结构，增加了接口、角色等元素，并给出软件体系结构的形式化描述，以便能够精确描述软件体系结构中静态结构与动态交互行为，最终达到软件体系结构重用，提高软件开发的效率。

研究了基于B方法的面向对象软件体系结构的切片技术，提高软件体系结构的重用。在分析现有面向对象程序切片技术存在的系统依赖图构图复杂、容易出错、切片不精确等问题基础之上，引入波动效应和系统依赖图结合起来的方法对面向对象程序进行切片的方法。

本课题研究意义：由于该课题所提出的基于切片技术的B方法和UML相结合的可信软件开发模式是针对传统软件开发过程和开发技术容易导致软件失效的问题，其科学意义在于为从根本上解决软件开发过程中的不可控和不精确等问题提供一个新的思路和方法。

本研究提出的可信软件开发模式为保障软件开发过程的可控性和目标软件的可靠性提供新的解决问题的思路，增强我国软件产品的核心竞争力。

该项研究涉及形式化理论与软件工程等交叉学科的研究，所以，对于这些交叉领域学科的相互促进与发展也有重要意义。

社会经济效益，存在的问题：这项研究对于目前的IT行业是机遇，同时也是一项挑战。 要想当前的开发人员从传统的软件开发方法直接过度到形式化的软件开发过程，不是一朝一夕的工作，需要一个漫长的过程，在该领域还有一系列具体问题有待解决。

创见与创新：（1）系统性：从整个软件过程的规格说明、设计、代码实现和测试的角度开展了形式化方法的基础理论和相关技术的深入研究，提出一套基于切片技术的面向对象技术与B方法相结合的新的软件开发模式，解决目前形式化开发中出现的问题。（2）实用性：实现了UML模型图到B方法形式规约的全面的转换，降低了开发难度，扩展了形式化方法在软件开发中的实用度，同时提高软件的可靠性及可信性。 （3）交叉性：该项研究涉及形式化理论与软件工程等交叉学科的研究，旨在促进软件产品的竞争力和交叉学科间的相互促进与发展。

历年获奖情况：无。