基于切片技术的可信软件开发过程的B方法的研究

As the research on software development processing has been deepened gradually, people realize that the formal methods is one of the important ways to improve quality and reliability of software. The formal methods as an important technology realizing credible software is successful to some degree, but its practicability is not enough when compared with the object-oriented technology. The research object of the topic is the credibility of the softwre development.Based on our many years research results of formal theory, B methods and B tools of evaluating and using, UML modeling techniques and tools, the novel development methods combining UML and B methods will be studied deeply at the first place.Then, the model technology of current formal specification, refinement and validation will be analyzed while the process of trustworthy software development will be systematically discussed. At last, the novel method of software development processing of object-oriented program based on formal B methods using slicing technology will be put forward on the shortcoming of current formal methods in order to take sufficient advantage of two methods mentioned above. The critical purpose to run this research is to help the formal software development technology out of the laboratory, to provide theoretical and technical guidance and demonstration in formal software development and make the software development processing controllable and safe in order to secure the reliability of software, which can help enhance software product competition ability and promote the development of software industry. The study belongs to crossover study,which is related to computer science, mathematics and systems engineering science. The study can help enhance both software product competition ability and disciplines.

随着对软件开发过程研究的深入，人们认识到形式化方法是提高软件质量和可信性的重要途径。虽然形式化方法作为可信软件实现的重要技术已经取得了一定的成功，但是与面向对象技术相比，其实用性还存在一定差距。本项目以可信软件开发为研究对象，在我们多年形式化理论、B方法和B工具测评与使用、UML建模技术等方面的研究成果基础上，通过对目前形式化软件开发方法中存在的实际操作性差等问题的分析，深入UML与形式化结合研究、突破形式化规约、精化和模型验证技术等，通过对可信软件的开发过程作系统的分析、研究，提出一套基于切片技术的面向对象与B方法相结合的新的软件开发模式，解决目前开发方法中的不足，使形式化软件开发技术真正走出实验室，为形式化软件开发的应用提供理论和技术指导，保障软件开发过程的可控性和目标软件的可靠性。该项研究涉及形式化理论与软件工程等交叉学科的研究，旨在促进软件产品的竞争力和交叉学科间的相互促进与发展。

随着对软件开发过程研究的深入，人们认识到形式化方法是提高软件质量和可信性的重要途径。虽然形式化方法作为可信软件实现的重要技术已经取得了一定的成功，但是与面向对象技术相比，其实用性还存在一定差距。 按照项目研究计划，我们以可信软件开发为研究对象，在我们多年形式化理论、B方法和B工具测评与使用、UML建模技术等方面的研究成果基础上，通过对目前形式化软件开发方法中存在的实际操作性差等问题的分析，深入研究了UML与形式化结合、形式化规约、精化和模型验证技术等问题，讨论了可信软件的开发过程，最终提出了一套基于切片技术的面向对象与B方法相结合的新的软件开发模式，获得了较好的研究成果。相关研究工作已在发表在学术期刊上、国际会议和学术专著上，并申请了7项软件著作权。该项研究可以帮助解决目前开发方法中的不足，为形式化软件开发技术真正走出实验室以及形式化软件开发的应用提供理论和技术指导，最终能保障软件开发过程的可控性和目标软件的可靠性。该项研究涉及形式化理论与软件工程等交叉学科的研究，旨在促进软件产品的竞争力和交叉学科间的相互促进与发展。

内容获取失败，请点击重试