软件开发的形式化方法

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

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

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

软件开发中的形式化方法

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

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

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

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

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

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

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

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

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

形式化与可视化结合的FDOOM软件开发方法

It is an important issue in Software Engineering that combines the formal development method with the vi-sual development method. This study is based on the transform method and rules between the UML model and the RAISE model.We developes a new software development Method FDOOM (Formal Development based on Object Oriented Modeling) that combine the UML with the RAISE together. And there is a demo in the end.     

形式化方法Designware、B的比较

用形式化方法开发软件是提高软件可靠性和开发效率的革命性途径。Designware、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规格描述的正确性.通过实例分析验证了该方法的可行性.     

操作系统形式规约与验证综述

操作系统(OS)作为信息时代关键基础设施, 广泛应用于军事、工业、医疗等核心领域。其可靠性与安全性直接决定关键领域运行稳定, 漏洞易致系统崩溃、数据泄露等严重后果, 因此构建系统化安全保障体系具有重要理论与工程价值。以\"形式规约-形式验证-工程落地\"为框架, 梳理近十年该领域研究成果, 剖析技术路径与实践应用。在形式规约层面, 明确基于迁移系统等数学结构描述系统功能的模型规约与基于线性时序逻辑(LTL)定义安全、活性需求的性质规约的差异, 从功能正确性和安全属性两个方面进行阐述, 其中, 功能正确性涵盖任务管理调度、内存分配回收、异常中断处理、任务间通信与文件系统读写一致性, 安全属性聚焦访问控制的BLP模型与BIBA模型、分离内核多域隔离、信息流无干扰与无泄漏理论。在形式验证层面, 阐述依托霍尔逻辑验证程序一致性的推理证明、基于LTL与计算树逻辑(CTL)验证时序属性的模型检测、属性验证标准化流程3类核心方法, 并以首个通过机器证明实现功能正确与信息流无干扰的seL4微内核为案例, 揭示理论到工程的转化路径。在工程应用上, 总结汽车领域控制器局域网(CAN)总线通信验证、智能手机Android系统组件间通信鲁棒性检测的成果。本文的系统性梳理旨在为相关领域的研究奠定基础, 为大语言模型提供数据集支持, 并为最终的技术工程落地提供参考。     

面向对象软件规格语言的设计

本文提出一种面向对象软件的形式描述语言JOOSL,用它可描述面向对象软件需求规格、概要设计和详细设计。从描述方法角度看,需求规格和概要设计的描述在很大程度上相同,这就反映了OO开发模型中需求和设计之间的重叠。在这些描述中用抽象方法描述数据和操作;详细设计中确定算法细节和数据的表示。JOOSL 认为对象是一种抽象的状态机,继承是行为特性的共享。     

轨道交通控制软件中基于场景的需求分析方法

针对轨道交通控制软件的形式化方法,在实际工程应用中存在形式化建模和系统级场景验证困难的问题.提出一种面向轨道交通领域的形式化建模和需求确认及验证方法.通过非形式化、半形式化到形式化规约三步演化过程,为形式化规约构建提供模板.在对需求的确认和验证中,根据形式化规范建立需求模型,导出相关图表,基于此检查领域专家关注的场景....     

基于形式化方法的测试驱动开发研究

对测试驱动开发中测试用例的自动生成和管理问题进行了研究,并时现有方法进行了分析和比较.给出了一种基于形式化方法的测试用例生成和管理方案.该方案通过形式化语言描述软件规约,并通过相应工具生成和管理测试用例,从而提高了测试驱动开发的效率.最后给出了该方案在极限编程各个开发阶段的应用.     

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.