软件开发的形式化方法

随着计算机及软件系统逐步渗透到社会生活的方方面面,对软件可靠性、安全性和保密性的要求也越来越高．本文阐述了形式化方法的定义、重要性及主要研究内容。着重讨论了形式规约方法,以及演绎证明和模型检测等形式验证方法。     

有限构模器的扩展及其在形式化方法中的应用

规约在软件开发和验证中占有重要地位,对于以一阶逻辑为基础的规约,可以利用有限模型构造技术对其执行并测试,文中研究规约中某些特性的处理,包括存在量词以及二元关系析传递闭包,对已有的一个构模工具进行扩充,发现了文献中的若干错误。     

形式化方法B及其程序规约机理

用形式化方法开发软件是提高软件可靠性和生产效率的革命性途径,是实现软件自动化的关键。文章针对B方法,介绍了其产生的历史背景,分析了其程序规约机理,并结合实例给出了B方法中抽象机的具体运用,对该方法的特点进行了评述。     

软件开发中的形式化方法

1形式化方法 随着软件系统复杂度的不断增长,开发正确、可靠的软件,已成为一个巫解决的问题。形式化方法是解决此间题的一个有前途、有希望的技术,它建立在严格的数学基上,其目标是希望能使系统具有     

形式化方法在软件开发中的应用

形式化方法是把概念、判断、推理转化成特定的形式符号后,对形式符号表达系统进行研究的方法。是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。形式化方法就是用符号化的数学变换把需求分析给准确的表述出来,这样可以确保和需求的一致性,并能用于分析和验证应用程序。     

基于形式化方法的软件开发技术

形式化方法作为一种以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，能够极大地提高软件的安全性和可靠性。本文从形式化方法的研究内容、分类以及发展等方面出发，对基于形式化方法的软件开发的基本思想作了介绍，分析了使用形式化开发软件系统的优势和可靠性.     

基于形式化方法的软件开发技术

形式化方法作为一种以数学为基础的方法,能够清晰、精确、抽象、简明地规范和验证软件系统及其性质,能够极大地提高软件的安全性和可靠性.本文从形式化方法的研究内容、分类以及发展等方面出发,对基于形式化方法的软件开发的基本思想作了介绍,分析了使用形式化开发软件系统的优势和可靠性.     

面向对象模型与形式化方法

本文在分析面向对象和形式化方法两种重要系统建模方法的基础上,论述了两种方法的关系,指出二者互补、组合的优越性,概述了各种领域里的组合应用,并进一步设想未来的发展方向可能是二种方法的优点的活用和统一。     

一种并发系统的规约方法

提出了并发系统的一种规约方法．这一方法可用于对并发系统进行建模和对模型的验证．将形式化工具融入到一种二维的规约方法中,这样就能使形式化工具更易于应用到并发软件的开发过程中．此外,还提出了一种并发系统的形式化抽象模型．     

Formal Methods of Analysis of System Properties

A review of using formal methods of specification and verification of software and hardware systems is given and an approach and formal methods are proposed that make it possible to solve the so-called feature interaction problem arising in telecommunication systems.     

基于Event-B的软件工程形式化方法综述

在当今泛在计算和软件定义的大趋势下,形式化方法逐步成为指导软件需求定义、分析软件设计方案、验证软件制品正确性的重要方法,渗透到软件工程的全寿命周期.Event-B作为一种构造即正确的方法,为软件工程形式化方法的应用提供了支撑.本文对现有的基于Event-B的软件工程形式化方法进行了分类阐述,主要分为Event-B控...     

结构化方法、面向对象方法和形式方法的比较与结合

结构化方法、面向对象方法和形式方法是三种不同的软件开发方法。本文对这三种开发方法进行了对照比较,讨论了它们的互相结合,并提出了将其结合在一起的集成方法的设想。     

A Contract-based Approach to Specifying and Verifying Safety Critical Systems

Light-weight formal method has been regarded as an important approach to development of component-based safety critical systems. The paper proposes an approach which can formally specify and verify the contract of static structure, dynamic behavior and refinement of component systems based on UML 2.0 superstructure. As results, the correctness of static contract can be obtained via type checking of interfaces and connectors. Dynamic contract can be verified through determining the cooperativeness of integrated components, whose contracts are depicted with interface protocol state machines and their semantics models, namely contract automata. The refinement relation between high level component and its implementation will be guaranteed through defining the alternating simulation between contract automata of components at different levels.     

基于Z规格的UML模型形式化转换及验证

统一建模语言(UML)所建立的模型的正确性无法通过其本身进行形式化验证,为解决这个问题,根据UML模型的静态性质和动态模块行为两个方面提出结合形式化规格说明语言的模型形式化方案,以此为基础提出将UML目标模型转化为Z规格说明的形式化方法,并用Z-EVES工具形式化检测Z规格描述的正确性.通过实例分析验证了该方法的可行性.     

Prospec: Support for Elicitation and Formal Specification of Software Properties

Although formal verification techniques have been demonstrated to improve program dependability, software practitioners have not widely adopted them. One reason often cited is the difficulty in writing formal specifications. This paper introduces Prospec, a tool to assist practitioners in formally specifying software properties. Prospec uses property patterns and scopes. Previous efforts at providing tool support for property specification have not provided convenient abstractions for specifying properties that include multiple events or conditions. A taxonomy of composite propositions is introduced to address this issue by defining relations among propositions and providing graphical abstractions that can assist in specification and validation of properties. This paper shows how composite propositions can enhance the specification pattern system by helping practitioners consider subtleties of behavior in sequences and concurrency through directed questions and visual abstractions. The paper introduces an elicitation and specification process to define patterns, scopes, and composite propositions.     

基于Hoare逻辑的密码软件形式化验证系统

在Hoare逻辑理论和ACSL语法规范的基础上,设计一种针对密码软件的形式化验证系统,由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL中RC4算法的软件实现为例,对其功能正确性、保险性和信息流安全性进行验证,结果表明,该系统具有较高的自动化水平,可在一定程度上降低形式化验证方法的复杂度。     

形式化方法在高中算法教学中的应用研究

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR（Partition And Recur）方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。     

Formal hardware verification methods: A survey

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.