形式化方法在机载电子硬件研制中的应用研究

详细设计规范是机载电子硬件适航性设计流程中的关键文档.通过对形式化方法特点分析,给出基于模型检验的设计规范提取步骤,以提高设计的正确性和完整性.以ARINC429总线传输模块设计为例,基于形式化方法完成正向设计过程.试验结果表明,基于形式化方法的设计流程能够有效帮助制定详细设计规范并在后期提高验证效率,进而缩减研制周期.     

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

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

基于RUP和VDM++的软件形式化开发方法的研究

形式化方法是软件开发过程中用于保证软件系统具有高度正确性和可靠性的一个重要手段。但形式化软件规范不直观,不容易被开发人员所接受。该文将较为直观地统一软件过程和VDM++形式化方法结合在一起,提出了一种软件形式化开发方法,并通过开发一个实际的文件设备记账系统说明了该方法的可行性与有效性。     

终止证明方法在形式化建模中的应用

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失...     

基于Web的网络旅游服务系统的形式化B开发

形式化B方法支持从规格说明到代码生成的全部软件开发过程。结合网络旅游服务系统模型，讨论了形式化B方法的具体运用，在分析服务器端和客户端状态表示的基础上，给出了该系统的抽象机模型及其精化过程。     

基于Web的形式化方法工具RRTChecker的研究与设计

形式化方法工具通常是在UNIX/Linux系统下设计开发的,难于使用阻碍了形式化方法的进一步推广.本文针对形式化方法RAISE,提出了一种研究和开发基于Web的工具的方法.该方法以原有的RAISE工具为基础,通过Shell管道拦截技术、ASP技术、ActiveX DLL技术及路径重写技术,将工具的所有功能集成整合到统一的、用户友好的Web界面上,用户可通过鼠标在浏览器中进行不同的操作.原有的RAISE工具的所有功能,在基于浏览器的集成化工具中得到全面支持.该方法也为开发其它形式化方法基于Web的工具提供了新思路.     

基于UML的软件形式化需求分析与验证

针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言（UML）模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。     

面向嵌入式系统的IPSec形式化建模

为了满足嵌入式系统在网络通信环境下的一些安全需求,通过考察嵌入式开发的系统环境,对比现存的一些网络安全问题的解决方法,采用选取适用的IPSec(网络层安全协议)模块,并使用形式化语言对其进行描述,以给有此类安全需求的嵌入式开发提供一个形式化的IPSec模型.同时,在协议的开发过程中引入形式化的方法也有利于保证协议的一致性.     

基于B方法的组件开发

现有的组件开发技术的规格说明是非形式化的,这导致了逻辑的非严密性和理解的歧义性,将会严重影响组件复用的效率。B方法是形式化方法之一,已经有功能强大的工具支持软件的形式化开发过程,它通过严格的数学推导和证明来保证软件设计和代码的正确性。为此,将B方法应用于学生信息管理系统的开发,提供了学生组件从需求规格说明、精化到最终实现的开发过程。通过对这一实例的研究可以看出,B方法增强了组件的规范性,对于提高组件复用的可靠性有重大的意义。     

一种形式化的组件化软件过程建模方法

为了解决当前软件过程重用方法中存在的问题,特别是由于缺乏对软件过程组件及其操作法则的精确定义所带来的重用中的低效率问题,介绍了一种形式化的组件化软件过程建模方法(componentized software process modeling,简称CSPM).CSPM提供了形式化定义可重用软件过程的机制,并且给出了将过程组件组合成过程模型的一系列操作法则.利用CSPM方法,能够以严格的方式对软件过程组件进行重用,并且有效地避免了传统非形式化建模方法中因歧义而有可能引起的潜在错误.CSPM还可以将对组装后的软件过程模型针对某些特定性质的验证问题转化成对其对应组件的一系列子验证问题,从而通过指数地减少需要搜索的状态空间规模,将原来在某些特定环境下不实用的验证问题简化成验证代价较小的一系列问题.     

基于相对重要性和熵修正的评估权重设置方法

为解决当前正式评价过程中评估权重设置不科学的问题,提出了基于相对重要性和熵修正的评估权重设置方法.该方法基于评价准则的相对重要性矩阵求得先验评估权重,根据每位评价员的评分情况对评估权重进行熵修正.对该方法的使用效果进行了仿真实验,并在该方法基础上设计和实现了正式评价系统.仿真结果表明,该方法能灵敏地根据用户偏好进行相应调整.探讨了正式评价系统在实施过程中遇到的问题和其解决方法.     

基于扩展CPN的OWL-S过程语义建模及分析方法研究

OWL-S过程语义的建模与分析是语义Web服务相关领域需要重点研究的问题。分析了目前OWL-S过程语义研究中存在的问题,提出了一种扩展的着色Petri网PM_ net(过程模型网,Process Model net)来对OWL-S的过程语义进行转化与分析。结合OWL-S过程模型元素的特点,PM_ nct对基本着色Pctri网的变迁和触发规则进行了扩展,使OWL-S的原子过程、组合过程和数据流等核心元素能够等价映射到PM net。同时说明了如何基于PM_ net对OWL-S的过程语义一致性进行分析,为OWL-S本体演化、语义Web服务组合和验证提供了合理的理论基础。     

基于软硬件协同形式验证的固件漏洞分析技术

为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。     

基于Pi-演算的Web服务组合的描述和验证

形式化方法对于建模和验证软件系统是一种有效的方法,所以对Web服务的形式化描述和验证是一个重要的研究方向．对于Web服务及其组合来说,保证其组合正确性以实现其服务增值是十分必要的．Pi-演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模．该文基于Pi-演算对Web服务及其组合进行形式化描述和建模．文中说明了Pi-演算与以前形式化方法的不同之处,分析了Pi-演算应用于Web服务组合需要解决的问题．讨论了Pi-演算与Web服务协议栈的对应关系,说明了利用Pi-演算建立Web服务组合模型的规则,指出了如何寻找代理和通道．最后建立了一个实际的模型,并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证．     

形式概念分析与软件过程改进

1 引言软件过程的改进是一个复杂的过程。影响软件过程改进的因素有很多,既有软件企业管理层对其意义的理解和倡导,也有软件过程实施当中数据的收集和分析。因为从理论、方法和技术上讲,后者涉及更多的富有挑战性的领域,所以数据的收集和分析(尤其是数据分析)更加直接地决定了过程改进的成功与否。比如,基于CMM的软件过程改进主要解决以下问题:     

Towards a formal definition of methods

The absence of a formal specification of methods permits application engineers to interpret method concepts in any way they want. Further, different CASE tool designers can implement the same method concepts in different ways. The approach to formal method specification described here is in three levels: the generic level, the method independent level, and the method level. The generic level provides a model of a method which can be instantiated to yield a method-independent view of methods. This view can, in turn, be instantiated to yield the formal method of interest. The attempt is to represent methods independently of any underlying way-of-working or paradigm, remove the process/product dichtomy by tight coupling of the process and product aspects of methods, and permit extensibility of methods. The formal specification can be used as a basis for building CASE tools, as an output to be produced by a CAME tool, and for defining development processes.     

工作流模型及其形式化描述

工作流是一个业务过程的全部或部分自动执行．为了实现工作流管理功能，我们必须将业务过程从现实世界中抽象出来，并用一种形式化方法对其进行描述，其结果称为是工作流模型．该文主要讨论工作流模型及其形式化描述问题．基于对现实世界业务过程的分析，该文提出一个三维工作流模型，它包含3个子模型：组织模型、数据模型和过程模型，分别从不同的侧面描述工作流的各种属性．文中详细论述各个子模型及其相互关系，并给出三维工作流模型的形式化描述．     

基于CCS的软件规范描述及实例研究

软件规范描述方法主要是软件工程化的UML方法与形式化方法二类方法。论文主要给出了基于CCS的软件规范描述,首先根据系统需求画出进程派生树和迁移图,再根据操作语义和系统约束条件得到进程表达式,并用Java语言实现了系统原型代码。笔者的工作证明了CCS具有细节化地描述系统内部状态,便于系统软件实现的能力;在手工转换进程迁移图到进程表达式的基础上,提出了自动转换的进一步研究思路。     

Integrated architectural modeling and analysis for high-assurance command and control system design

A Real-Time Architectural Specification (RAS) approach and its application to command and control (C2) systems are presented. Our objective is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into a practical and scaleable formal engineering method to support the design and development of highly reliable real-time distributed systems. The contribution of RAS is twofold: First, it provides a formal system that integrates system's timing requirements and requirements propagation into the process of architectural modeling and design in such a way that allows us to systematically enforce that the requirements are met in every step of the design process. Second, it offers an incremental and more scaleable approach for design modeling. These two features together make RAS a suitable model for the design of C2 systems. We further present an incremental method for verifying timing properties of an RAS model that helps to reduce the complexity of analysis both at a given design level and across different design levels. This revised version was published online in June 2006 with corrections to the Cover Date.