面向自然语言需求的验证性质生成方法

安全关键系统和软件的安全性、可靠性需要形式化验证来保障,使用形式化验证的前提是从自然语言需求文本中提取相关验证性质并将其转化为形式化规约,这已成为当前形式化验证领域研究的热点和难点.当前的形式化规约提取工作大多针对英文需求,较少针对中文自然语言需求.此外,由于AADL具有强大的表达能力和完善的验证机制,已成为航空航天领域的主要建模语言之一,而现有的工作较少考虑如何从需求中提取AADL模型的验证性质.为了解决上述问题,本文提出一种面向自然语言需求的AADL模型验证性质自动生成方法,从自然语言需求中提取验证的相关性质,并将其转化为AADL模型验证工具AGREE可识别的形式化规约.首先,定义了模式定义语言(Contract Pattern Language,CPL),将需求划分为不同模式,并给出由固定句型和占位符组成的需求模板;其次,通过自然语言处理技术解析需求文本,获取替换需求模板中占位符的原子命题,以便生成完整的形式化规约;最后,设计并实现了相关工具,并将其用于工业界实际案例来说明该方法的可用性和有效性.

SRLtoRadl生成系统及其范畴论语义

形式化软件规约技术是保证软件质量和提高软件生产率非常有用和重要的手段,但是形式化软件规约的获取是需求工程中一项相当困难的任务.本文针对问题需求自动化转换为形式化规约这个重要问题,研究从结构化需求语言SRL到形式化规约语言Radl自动生成系统及其高可靠性理论.为此,设计了一种受控自然语言-结构化需求语言SRL来描述问题需求;使用基于规则的方法,将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl;在该方法的指导下,设计并实现了从结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl;进一步,使用范畴论框架建立了SRLtoRadl生成系统生成过程的语义模型.实际效果表明该系统能有效的生成高质量形式化软件规约Radl.

计算机联锁软件的Z规格说明

计算机联锁软件是一种典型的安全关键软件,具有非常复杂的联锁控制逻辑和以失效安全为核心的安全需求。形式化其安全需求是一件十分必要,也是一件十分艰巨的任务。本文使用形式化规格说明语言———Z语言来描述其安全需求,生成形式化规格说明。形式化规格说明不仅有助于提高计算机联锁软件的质量,而且也有利于将来对它进行更严格的测试。

基于Z语言的形式化需求分析

介绍了形式化方法和形式化规格说明语言Z语言,利用Z语言对软件需求进行了严格定义,在严格的数学基础上进行软件开发,以获得更好的软件性能.利用形式化方法的需求分析,有助于发现需求中隐含的不一致性、二义性和不完整性,对其进行更深入精确的理解,从而进行规范化管理.

基于交易中间件的客户 /服务器系统的形式描述

基于交易中间件的客户 /服务器系统是一种典型的分布式事务处理系统，深入研究这种系统的一般模型，有助于深刻理解这种软件的特征与性质，有助于提高系统的正确性和可靠性。文章根据该系统的抽象模型对它的主要“构件”和“操作”的功能进行抽象的分析；并用规范语言 Z对这种体系结构的模型进行了系统的形式化描述。

形式化方法在核事故评价系统中的应用

核事故评价系统针对核事故发生后第一时间对其进行评价和预测分析,软件可靠性要求高.形式化方法具有严格数学基础,是软件开发最为重要的理论工具.本文首先用UML对系统进行分析建模,采用形式化语言对系统功能进行严格规约描述,提高系统开发的可靠性.

基于企业流程的需求形式化验证技术

需求验证是为了确保需求规格说明具有良好特性(完整性、一致性、无二义性)而对需求规格说明进行的一种审查活动。目前广泛使用的需求验证技术存在着两个问题:难以处理大型、复杂的需求文档;审查过程需要相当长的时间。该文所研究的基于企业流程的需求形式化验证技术,通过对需求文档中企业流程各活动之间的逻辑关系进行验证,从而发现其中的不一致性和二义性。

软件需求定义语言NDRDL的设计

本文概述了软件需求定义语言ＮＤＲＤＬ的设计目标及设计原则，并讨论了一些语言基本成分，如数据流图、控制流图、实体关系图等的设计。文中采用个人帐目管理系统（ＰＡＭＳ）作为示例。

从BPMN模型导出组合服务的代数规约

针对应用规约自动测试BPEL表示组合服务时需要解决BPEL服务的规约生成问题,提出了一种从BPMN模型导出BPEL规范定义的组合Web服务的由代数规约语言CASOCC-WS表示的代数规约方法。首先,定义从BPMN模型转换成基调的规则和从BPMN结构转换成正则表达式的规则,设计由正则表达式导出构成公理的项的算法;然后,提出根据所得的项人工书写公理的启发式规则;最后,实现一个从BPMN模型导出组合服务基调的工具原型。案例研究表明,该方法可以解决BPEL服务的代数规约生成问题。

一个面向网络并行环境的需求规约语言

提出了一个面向网络并行环境的需求规约语言ＯＯＲＳＬ。ＯＯＲＳＬ支持面向对象的分析方法，可以定义并行成分一进程，可以使用前后断言来表达用户的功能需求，允许将非形式化和半形式化的需求定义嵌入形式化的需求定义中。因此，ＯＯＲＳＬ语言是一个半形式化的语言，它为网络并行环境下的软件自动化和软件形式化开发提供了支持。介绍了ＯＯＲＳＬ的设计思想和主要语法成分，给出了一个实例。

一种嵌入式实时系统软件的形式化开发方法

领域特征突出的嵌入式实时系统软件开发,既需要严格地保证可靠性又要充分反映实时和交互行为特征,针对这种需要,该文提出了一种从需求分析到体系结构建模直至使用组件技术实现软件的形式化开发方法。文章在介绍了目前的各软件工程领域以及各软件开发阶段中的形式化模型和工具的现状和特点后,引入需求分析的模型和体系结构建模的描述语言,分析其长处和不足,最后对该方法与移动组件结合的前景进行了展望。

基于企业流程的需求形式化说明语言

需求说明是对需求分析结果所进行的文档化工作,其工作结果—需求规格说明在系统开发、测试、质量保证、项目管理中起着重要的作用。现有的需求规格说明绝大多数是采用自然语言来编写,由于自然语言在严密性上的缺陷,从而导致需求规格说明普通存在着三个严重的问题:模糊性、不准确性和不一致性。该文提出的基于企业流程的需求形式化说明语言,是以四元组作为描述机制,不仅能描述各活动之间的逻辑关系,而且能表达活动对信息流的操作形式,即将控制流和数据流合为一体。

一个面向对象的需求规格说明语言——SEURSL

提出了一种从建模到实现的完整的面向对象开放方法，它以Ｃｏａｄ／Ｙｏｕｒｄｏｎ方法为基础并对它进行了改进，改进后的方法能够有效地描述系统的功能和行为；同时给出了支持这种方法的需求规格说明语言———ＳＥＵＲＳＬ的规范化定义。

一种基于形式化规则的航电需求规范化方法

随着航空电子显控系统的日趋繁杂,如何正确分析航空电子显控系统的原始自然语言需求成为需求分析领域中急需解决的问题.本文基于形式化转换规则的需求规范化方法,对航空电子显控系统的原始自然语言需求进行规范化分析与研究.工作主要包括:对于不同的自然语言需求,符号化定义需求语句结构.针对自然语言需求语句当中经常出现的歧义、模糊、不可验证等问题,根据不同的需求语句模式设计出不同的转换规则.同时,为实现自然语言需求到规范化需求的自动转换过程,本文借助Stanford Parser词法分析器,输出不同需求语句的语法树,并结合相应的转化算法输出规范化需求语句.最后通过实例验证了基于形式化转换规则的规范化方法在航空电子显控系统的自然语言需求领域中具有较好的有效性和实用性.

网络实时系统的一种活动性描述语言

介绍了ADL,它是一种基于网络实时系统的活动性描述语言,一种描述并发处理中时态和功能行为的新的形式规格说明符号。ADL专用于计算机网络,是DOR IS的一种形式语言扩充。它组合了状态机活动(ASM)的图形符号和基于模型的活动功能行为(AFB)符号;提供了关于ASM的抽象语法和静态、动态语义。最后通过一个小实例说明该语言是如何解释指定网络实时系统的。

面向业务平台原理及其在软件工程中的作用

为了解决业务应用系统软件工程中需求变更带来的系统研发滞后,以及业务人员同软件开发人员沟通带来的沟通偏差等问题,面向业务平台将业务应用系统分离为系统层和业务层。在业务层,业务人员使用业务设计器直接进行需求建模,系统层业务引擎负责执行业务模型。这样使系统适应变化能力增强,是随需应变的解决之道。