B语言和方法与Z、VDM的比较

1 引言形式化方法是建立在严格数学基础上的软件开发方法。软件开发的全过程中,从需求分析、规格说明、设计、编程、系统集成、测试、文档生成直至维护各阶段,凡是采用严格的数学语言、具有精确的数学语义的方法都称为形式化方法。形式化方法的一个重要研究内容是形式规格说明,即用具有精确语义的形式化语言书写的程序功能描述,它是论证程序是否正确的依据。形式化方法需要形式规格说明语言的支持,也可以说形式化方法的关键在于形式规格说明语言。形式规格说明语言提供了一个称为语法域的记号系统和一个称为语义域的目标集合,以及一组精确地定义哪些目标系统满足哪个规格说明的规则。根据对目标软件系统进行说明的方式分三种规格说明语言:     

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

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

通用嵌入式系统软件测试平台的设计

仿真测试是嵌入式软件系统测试阶段的一种有效测试方法,探讨了通过在PC机上仿真模拟ARM嵌入式系统,对嵌入式系统软件进行仿真测试的通用测试平台的设计。该平台可以在不做大幅度修改的情况下对不同的嵌入式系统软件进行各种测试。重点介绍了仿真模拟器、测试管理器和测试平台专用工具链的设计,提出了一种测试管理器的实现模型,并进行了详细的描述。     

面向方面分布式系统形式化规格说明语言

分布式系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要面向方面软件工程方法的支持,而形式化方法能保证分布式系统的正确性。本文对分布式规格说明语言Ocsid进行了面向方面的扩展,讨论了面向方面的Ocsid的框架结构、语法要求、方面的联结和功能接口。定义了面向方面的Ocsid规格说明语言中叠加和组合的形式化描述,该形式化描述覆盖了各个精化阶段,使精化体系的各个独立视点被协调地组合,并能形式化地验证规格说明的时态属性和系统行为。本文的工作针对的是分布式系统的形式化规格说明,提出了面向方面Ocsid的形式基础和方面扩展,其基本思想同样适用于更一般的情况。     

基于本体的服务构件描述研究与实现

面向服务架构(SOA)是实现企业自动化的未来发展趋势,用面向服务思想架构企业应用更强调如何通过基于构件的软件开发(CBSD)快速满足企业多变的业务需求,构件的描述方法是构件库管理和构件分类检索的基础.通过对服务构件的语义描述方法与传统构件描述方法的比较,引入了本体建模的思想,对青鸟构件库系统构件分类描述规范和OWL-S规范进行了扩展,提出了一种基于本体的服务构件描述方法.这种服务构件语义描述方法支持面向服务的语义检索,提高了服务检索的查全率和查准率,为实现基于语义Web Service的SOA网构开发奠定基础.     

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

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

通用测试系统资源描述模型研究

面向信号软件结构是通用自动测试系统软件的发展方向,面向信号软件中使用的是虚拟资源,系统必须通过测试资源描述进行资源配置,才能驱动测试设备完成测试任务.分析了测试资源描述的设备模型、适配器模型、系统配置模型以及测试系统资源配置过程,并在实践中进行了应用.     

面向软件行为和多视点的需求建模方法

提出一种面向软件行为和多视点的需求建模方法,包括建模步骤和建模语言.其中目标系统根据问题域以及视点源被划分成视点.视点在需求模型中以实体的方式存在,每个视点通过从需求规格说明中提取的场景来描述,作为需求模型基本组成单位的场景模型则通过基本的行为复合而成.分析了基于行为和多视点的需求建模过程,讨论了需求建模语言:行为描述语言的语法和语义,并给出相关实例分析以及所实现的建模工具简介.     

一种基于扩展I*框架和UML的面向Agent需求建模方法

以分布式电子商务系统为研究背景，提出了一种基于扩展I^*建模框架和UML的面向Agent需求建模方法．该方法将需求工程划分为早期需求获取和后期需求规格说明两个阶段：在早期需求获取阶段，在I^*策略模型中引入服务依赖概念，用于描述组织背景中Agent的意图和Agent之间的依赖关系，同时描述系统内部Agent和分布式环境中其他Agent之间的依赖关系；在后期需求规格说明阶段，采用扩展的UML在Agent抽象层次上建立统一的需求模型．该方法还为早期需求获取平滑过渡到后期需求规格说明提供了统一的模型映射规则．从而保持模型的一致性．     

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

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

基于LabVIEW的脉冲涡流检测实验系统

针对目前商用脉冲涡流检测系统由于价格昂贵、可扩展性差等不足而难以在实验室应用的问题,设计了一套基于LabVIEW的脉冲涡流检测实验系统.系统软件采用LabVIEW编程,实现了激励方波的产生,检测信号采集、处理与显示,数据保存与回放等功能.利用该系统对Q235钢板圆孔缺陷进行检测实验,结果表明系统各项功能运行正常,检测信号特征与理论预期一致.系统具有操作简单、易修改、可扩展性好等优点,能有效地满足在实验室条件下进行脉冲涡流检测的要求.     

基于测试需求的互操作性测试用例生成方法

网络化应用将成为未来软件技术发展的主导模式。为了保证网络化应用之间能够有效地协同工作,必须对其进行互操作性测试。互操作性测试具有测试需求复杂易变、测试用例设计困难的特点,因而需要消耗大量成本。为此,提出一种基于测试需求的互操作性测试用例生成方法。该方法采用模型驱动的测试思想,以测试需求模型描述互操作性测试需求,以状态图描述各被测应用的规格说明,通过两者的结合生成满足测试需求的测试用例。     

Generating test data from state‐based specifications

Although the majority of software testing in industry is conducted at the system level, most formal research has focused on the unit level. As a result, most system‐level testing techniques are only described informally. This paper presents formal testing criteria for system level testing that are based on formal specifications of the software. Software testing can only be formalized and quantified when a solid basis for test generation can be defined. Formal specifications represent a significant opportunity for testing because they precisely describe what functions the software is supposed to provide in a form that can be automatically manipulated. This paper presents general criteria for generating test inputs from state‐based specifications. The criteria include techniques for generating tests at several levels of abstraction for specifications (transition predicates, transitions, pairs of transitions and sequences of transitions). These techniques provide coverage criteria that are based on the specifications and are made up of several parts, including test prefixes that contain inputs necessary to put the software into the appropriate state for the test values. The test generation process includes several steps for transforming specifications to tests. These criteria have been applied to a case study to compare their ability to detect seeded faults. Copyright © 2003 John Wiley & Sons, Ltd.     

实时多任务软件高可靠性测评方法

为了克服传统可靠性测试方法在验证高可靠性指标时测试持续期太长的困难,针对实时多任务软件的特点,提供了一种融基于体系结构的系统可靠性建模、最大熵原理、贝叶斯统计推断为一体的多级高可靠性测评方法。数值仿真表明,该方法在不降低验证测试置信水平的基础上,能有效缩短验证测试持续期。     

A Case Study on Applying a Tool for Automated System Analysis Based on Modular Specifications Written in TRIO

An effective means for analyzing and reasoning on software systems is to use formal specifications to simulate their execution. The simulation traces can be used for specification testing and reused for functional testing of the system later in the development process. It is widely acknowledged that, to deal with the complexity of industrial-size systems, specifications must be structured into modules providing abstraction mechanisms and clear interfaces. In our past work, we defined and implemented a method for simulating specifications written in the TRIO temporal logic language, and applied it to functional testing of time-critical industrial systems. In the present paper, we report on a case study with a tool that analyzes TRIO specifications by taking advantage of their modular structure, so as to overcome the well-known state-explosion problem and make the proposed method really scalable. We discuss the fundamental operations and the algorithms on which the tool is based. Then, we illustrate its use in a realistic case study, inspired from an industrial application. Finally, we comment on the overall results in terms of usability of the tool and effectiveness of the approach, and we outline future improvements.     

从用户需求到软件规约：一种问题变换的方法

研究的目的是在获取用户需求和领域描述的基础上规约出对软件规格的描述.提供了一种实现从用户需求到软件规约的平滑和可推理的变换方法.在深入研究问题框架方法的基础上,采用Hoare 的通信顺序进程语言CSP及Lai的最弱环境演算符实现了整个问题图的变换,且导出的软件规格是具有高抽象粒度的程序代码模型,能够被FDR模型检测工具所验证.该工作为实现嵌入式软件开发从需求到软件代码、文档的自动转化及验证等奠定了理论基础.此外,把该理论与模型检测工具FDR联合起来会有助于提高嵌入式软件开发的效率和准确性.     

一种基于内置合约检查和可配置接口的软构件测试技术*

从构件使用者和开发者的角度分析构件及构件化软件的测试,利用B. Meyer的合约化软件设计思想作为构件测试的理论基础,并在其上面进行了扩展与改进,提出了一种基于内置合约检查和可配置接口的构件测试技术。该方法的优点是：当构件被部署到新的系统环境中时,能够自动测试其服务端是否遵守彼此之间合约,并验证自身在运行阶段履行其所声明的义务的能力;利用可配置接口,可以根据所部署环境和特定系统的需求,动态地选择测试强度;当构件集成出现问题时,能够从抛出的异常信息定位到出错的位置。     

Exhaustive property oriented model-based testing with symbolic finite state machines

We advocate a fusion of property-oriented testing (POT) and model-based testing (MBT). The existence of a symbolic finite state machine (SFSM) model fulfilling the properties of interest is exploited for property-directed test data generation and to create a test oracle. A new test generation strategy is presented for verifying that the system under test (SUT) satisfies the same LTL safety conditions over a given set of atomic propositions as the model. We prove that this strategy is exhaustive in the sense that any SUT violating at least one of these formulae will fail at least one test case of the generated suite. It is shown that the existence of a model allows for significantly smaller exhaustive test suites as would be necessary for POT without reference models. As a corollary, the main theorem also generalises a known result about SFSM-based conformance testing for language equivalence. Our approach fits well to industrial development processes for (potentially safety-critical) cyber-physical systems, where both models and properties representing system requirements are elaborated for development, verification, and validation.     

综合模块化航电软件系统测试方法研究综述

现代飞行器系统中开始广泛采用综合模块化航电IMA(Integrated Modular Avionics)体系架构,IMA中软件系统的高质量要求对传统的航电软件测试方法提出了新的挑战。对目前基于ARINC653的IMA软件的系统级测试中的基本测试方法进行了综述分析,主要内容包括:首先给出了基于ARINC653的IMA体系结构描述,并对其架构中最重要的系统可配置性进行了分析;然后阐述了总的系统测试策略,以及不同级别的IMA软件系统测试过程;最后简要说明了IMA系统测试环境的通用要求。