形式化方法概貌

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.

依赖注入技术及其执行过程的形式化描述

依赖注入技术指由构件运行平台在运行期根据系统配置文件中定义的构件间的依赖关系,将被调用构件实例化,并注入到调用构件之中。本文在分析研究依赖注入技术的基础上,用完全格工具形式化地描述依赖注入的执行过程。

面向构件的系统开发及其形式化

回顾了软件构件与形式化方法的基本概念,介绍了软件构件的形式化,根据典型的面向构件的开发流程和基于形式化方法开发软件的特点,提出了一个基于形式化方法的面向构件的系统开发模型。针对目前面向构件的软件开发形式,提出了一些建议和方向。

形式化方法和对象技术的结合途径研究

形式化软件开发方法被认为是开发可靠的与高质量软件的一个良好途径 .本文首先给出形式化方法概述 ,并介绍两种分别代表面向模型和面向性质的形式规约语言Z和Larch .然后 ,重点讨论形式化方法与面向对象技术的结合 .

B方法和构件技术在软件开发中的应用研究

提出了一种基于B方法和构件技术的形式化开发方法,该方法结合构件技术和形式化方法,对软件开发的方法进行改进从而提高了软件的重用,很好地消除了系统的二义性、不完整性和不一致性,大大提高了软件开发效率.