基于问题模式的形式化软件规格说明生成方法

精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明.     

基于B方法的TCP协议形式化研究

协议的规格说明主要是以自然语言描述的,对其进行形式化的目的是精确描述协议,减少开发人员对协议规格说明理解的偏差.B方法可产生简明、精确、无歧义且可证明的规格说明.适合对协议进行形式化描述和一致性测试.本文详细地介绍了使用B方法对TCP协议进行形式化,并据此生成了测试用例,提高了TCP协议一致性测试的质量和可靠性.     

需求工程中的不确定性研究

1 引言用户需求一般用自然语言描述,是非形式化的,因而在生成确定的、形式化的需求规格时不可避免地会牺牲用户的部分需求。采取何种方法能尽量减少信息损失和不一致,从而使需求规格更接近于用户需求是软件开发中必须解决的重要问题。起初,在软件工程中这种转化是依靠软件开发者对用户需求的理解及自身知识完成的,使得生成的需     

安全苛求软件需求规格中的安全特性验证方法

针对自然语言描述的安全苛求软件需求规格中安全特性不准确、不一致等问题,提出一种基于UMLsec安全特性验证方法。该方法在UML需求模型类图和顺序图的基础上,为核心类的安全特性自定义构造型、标记和约束,完成UMLsec模型构建;之后,使用设计实现的UMLsec支持工具对安全特性进行自动验证。实验结果表明,该方法能准确描述安全苛求软件需求规格的安全特性,同时可以自动验证安全特性是否满足安全需求。     

面向系统能力的形式化分析和测试方法

国内软件业界实施系统测试时,大部分采用对系统规格说明描述的功能点进行逐一测试的方法,很少从系统能力的角度进行测试,难以充分说明系统软件产品满足系统能力需求的要求。同时,系统规格说明使用自然语言进行描述,存在语义不准确的现象,直接影响系统测试的质量。针对上述问题,提出了一种面向系统能力的形式化分析和测试方法。通过该方法,测试工程师可得到语义清晰的系统能力需求描述,并实施面向系统能力的系统测试,有效地提高系统测试的充分性和准确性,从而提高系统软件质量。     

一种基于状态模型的机载软件运行状态和方式的分析方法

随着软件在航空装备中使用越来越多,软件复杂性越来越高。现阶段采用自然语言描述的机载软件运行状态和方式,很难清楚地描述其中的逻辑关系和运行机制,给软件开发、测试等工作带来诸多困难。在结合相关标准中规定的软件运行状态和方式的基础上,建立了一种UML软件状态模型,并基于该模型给出了一些关于软件运行状态和方式的应用场景和方向。所阐述的方法可以帮助开发人员、测试人员更全面掌握软件状态,更好地改善软件质量,也可提高软件需求规格说明的可读性。     

使用Object-Z获取形式需求

针对软件需求描述中用UML描述的模型与形式需求说明相比不利于推理和验证的问题,使用统一过程建立用UML描述的需求模型并对其进行形式化,获得用Object-Z描述形式需求说明的方法和步骤,并结合实例进行论述. 提出利用形式方法验证和确认非形式需求规格说明的过程. 该研究为验证和确认非形式规格说明提供1种有效方法.     

Z和VDM规格说明的差异比较

实现软件开发过程各阶段的自动化是软件工程的重要目标之一。软件自动化的前提是形式,包括软件需求规格、软件设计规格和算法描述等的形式化。形式化软件规格说明不仅是对用需求,也是对软件系统的严格定义,在软件开发中有着相当重要     

用带时钟变量的线性时态逻辑扩充Object-Z*

Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。线性时态逻辑能够描述实时系统,但不能很好地处理连续时间关系,也不能很好地模块化描述形式规格说明。首先用时钟变量扩充线性时态逻辑,接着提出了一个方法——用带时钟变量的时态逻辑(LTLC)来扩充Object-Z。用LTLC扩充的Object-Z是一个模块化规格说明语言,是Object-Z语法和语义的最小扩充,其最大优点在于它能方便地描述和验证复杂的实时软件规格说明。     

软件工程(三)软件开发方法——软件需求分析(2)

结构化自然语言是介于形式语言与自然语言之间的一种语言。它虽然没有形式语言那样严格,但具有自然语言简单易懂的优点,又避免了自然语言的一些缺点。结构化自然语言的语法通常分为内外两层。外层语法描述操作的控制结构,如顺序、选择、循环等。这些控制结构将加工中各个操作连接起来,内层的语法一般没有什么限制。三、实例——CIMS规格说明书1.概述本规格说明书规定了对CIMS的需要。CIMS将用来对安徽省工业设备安装公司所有干部信息进行检索、统计、制表、增加、删除、修改以及内部调动等管理。     

一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。     

形式化语言RT-Z的合成及其应用

Z是一种确定相关数据特征的非常成功的形式化语言，却在构造动态行为方面的模型缺乏相应的功能；而Timed CSP是一种确定动态行为的功能强大的语言，但它没提供适当的结构来构造相关数据特征。文中通过形式化语言Z和过程代数Timed CSP合成一种新的形式化方法RT-Z，使得RT-Z在软件系统开发过程的需求定义和设计阶段能书写软件系统一致、简单的规格说明。     

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

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

两种形式语言:RSL与Z的分析比较

RSL(RAISE规格说明语言)和Z是目前广泛应用的软件规格说明语言,本文从软件开发生命周期的角度对两种语言进行了比较,提出了将不同规格说明语言结合形式地描述系统的设想。     

Integrating software specifications into intrusion detection

There exist a number of Intrusion Detection Systems (IDSs) that detect computer attacks based on some defined attack scenarios. The attack scenarios or security requirements in some of these IDSs are specified in attack specification languages that are different from software specification languages. The use of two different languages for software specification and attack specification may generate redundant and conflicting requirements. The advantage of using the same language for both functional specifications and attacks specifications is that software designers can address the two different issues without learning two types of languages. We present a method of integrating Abstract State Machine Language (AsmL) and Unified Modeling Language (UML) state charts that are extended finite state machine based software specification languages, with an open source IDS Snort. This work provides AsmL and UML users an IDS that they can use without knowing how to write Snort rules. We automatically translate attack scenarios written in AsmL and UML state charts into Snort rules with context information. The original Snort is modified so that it can use the rules automatically generated by the translator. Adding context information to Snort rules improves the detection capability of Snort. To show the efficacy of the presented approach, we have built a prototype and evaluated it using a number of well-known attack scenarios.     

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

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

Formal analysis of the Shlaer-Mellor method: Towards a toolkit of formal and informal requirements specification techniques

In this paper, we define a number of tools that we think belong to the core of any toolkit for requirements engineers. The tools are conceptual and hence, they need precise definitions that lay down as exactly as possible what their meaning and possible use is. We argue that this definition can best be achieved by a formal specification of the tool. This means that for each semi-formal requirements engineering tool we should provide a formal specification that precisely specifies its meaning. We argue that this mutually enhances the formal and semi-formal technique: it makes formal techniques more usable and, as we will argue, at the same time simplifies the diagram-based notations.At the same time, we believe that the tools of the requirements engineer should, where possible, resemble the familiar semi-formal specification techniques used in practice today. In order to achieve this, we should search existing requirements specification techniques to look for a common kernel of familiar semi-formal techniques and try to provide a formalisation for these.In this paper we illustrate this approach by a formal analysis of the Shlaer-Mellor method for object-oriented requirements specification. The formal specification language used in this analysis is LCM, a language based on dynamic logic, but similar results would have been achieved by means of another language. We analyse the techniques used in the information model, state model, process model and communication model of the Shlaer-Mellor method, identify ambiguities and redundancies, indicate how these can be eliminated and propose a formalisation of the result. We conclude with a listing of the tools extracted from the Shlaer-Mellor method that we can add to a toolkit that in addition contains LCM as formal specification technique.     

Using formal specifications to support software testing

Formal specifications become more and more important in the development of software, especially but not only in the area of high integrity system design. In this paper it is demonstrated, how, apart from the specification phase, further benefits may be drawn from formal specifications for checking the implementation against the specification. It is shown how the specification can be used for systematically deriving test input data and for automatically evaluating test results. The approach is illustrated using the specification language Z. The same principles may be applied to other specification languages. The approach allows a high degree of automation, drastically improving productivity and quality of the testing process.