购买
下载掌阅APP,畅读海量书库
立即打开
畅读海量书库
扫码下载掌阅APP

3.1.2 基于形式规约语言

在基于形式规约语言的嵌入式软件建模及测试技术中,有代表性的是RTRSM、CSP、TCSP、Z语言、TTCN-3语言和ATLAS语言等。实时嵌入式软件的建模应当支持事件驱动、状态迁移描述、复杂动态交互行为和严格时间限制等领域特征。

嵌入式软件系统的需求建模规约语言RTRSM(Real-time Requirements Specification Model)以扩充的层次并发有穷状态机HCA为核心,以支持合成的模板为基本组成单元,利用转换有效期和事件预定机制来描述时间限制,具有较强的时间限制描述能力,能自然而直接地支持交互行为的建模,可执行且具有良好的形式语义。RTRSM通过模板来支持系统的分解,其具体表现形式为包括接口和数据定义的表格以及与状态图等价的形式化的规则集。

CSP(Communication Sequences Processes,通信序列进程)是Hoare于1978年提出的一种能够对具有并发关系的系统进行建模的形式化语言,它基于顺序通信,主要通过进程事件的集合和进程的轨迹来描述进程的行为,可以通过并发、选择、递归等来描述进程之间的关系。在CSP的基础上加入时间因素形成TCSP(Timed CSP,时间通信序列进程)描述语言。这种语言具有良好的形式化基础,语法语义定义良好,对带时间的并发进程的表达清晰简洁。

Z语言是由英国牛津大学程序研究组(Programming Research Group,PRG)开发设计的。Z本身是一个书写规格说明的语言,或者说是一种表示方法。IBM公司利用Z语言对其用户信息控制系统(CICS)进行规格说明的重写并获得了成功,使软件开发费用降低了9%,对Z语言产生了极大的影响。Z语言是基于一阶谓词逻辑和集合论的形式规格说明语言,具有精确、简洁、无二义等优点,有利于保证程序的正确性,尤其适合无法进行现场调试的高安全性系统的开发。它的另一个主要特点是可以对Z规格说明进行推理和证明,这种特点使得软件开发人员或用户能够很快找出规格说明的不一致、不完整之处,从而提高软件开发的效率。随着技术的不断发展,出现了Z的一些扩展语言,如Object-Z和Real-Time Object-Z等。一种基于Z规格说明的软件测试用例自动生成技术如图3-2所示,其具体做法是:通过对软件Z规格说明的分析,找出描述软件输入、输出的线性谓词;将上述线性谓词转换成相应的线性不等式组,并求解该线性不等式组得到相应的区域边界顶点;找出区域边界附近的点,经过输入、输出逆变换得到测试用例。此外,还有利用Z规格说明进行软件测试和度量的方法,但该方法需测试人员具有丰富的测试经验和深厚的数学基础才能完成,而且由于是手工测试,测试的效率比较低。由于Z语言基于数学的概念,过于抽象、简明,因此用它编写的形式规格说明过于抽象、难懂,而软件开发和测试人员习惯于非形式方法,缺少基于形式方法的训练。由于Z语言尚缺乏自动化工具的支持,且基于Z语言的形式规格说明的正确性证明费时费力,因此限制了其工程应用。

图3-2 基于Z语言的测试用例自动生成

TTCN-3(Testing and Test Control Notation 3)是一种基于文本的测试描述语言,它由TTCN(Tree and Tabular Combined Notation)改进、扩展而来,在形式方面有较大改进,内容方面统一了原来混乱的概念和定义,简化了表示方法。TTCN-3适用于各种交互系统的描述,目前已广泛应用于协议测试、Web服务测试和基于CORBA的平台测试等领域。当前测试领域主要对TTCN-3采用图形表示,然后将图形转换为代码描述;图形通过MSC(Message Sequence Chart)来表示,通过MSC能很好地表达系统与其交联环境的通信行为。TTCN-3通过模块来完整描述测试套件,模块包括定义部分和操作部分,定义部分给出测试组件、测试端口、数据类型、变量、常量、函数以及测试用例,控制部分则进行一些局部定义以及调用测试用例并控制其执行顺序。通过基本的MSC图可以描述测试用例中表示的测试动作,而通过HMSC(High-Level MSC)可在更高的层次上组织这些基本MSC表示的测试用例。上述分层次的表示方法可以很好地表达较为复杂的测试过程,图3-3给出了构建一个TTCN-3测试套件的思路。

图3-3 TTCN-3测试套件建立思路

ATLAS语言是国际测试标准ABBET(广域测试环境)和SMART(标准的模块式航空电子设备维修与测试)定义的UUT描述语言。它采用面向信号的描述方式,描述了UUT的测试需求在特定的ATS上解释执行的过程。

ATLAS有两个较为成熟的版本,ARINCStd626(由ARINC领导,1976年发布)和IEEEStd716(由IEEE设立的SCC20(Standard Coordinating Committee 20)领导,1985年发布)。随着在工程应用中的实践,ATLAS给出了一种面向信号设计ATS的有效方式,但也暴露了很多问题,比如:

·版本变化太多,不同版本之间发生了显著的变化;

·语言过于冗长,关键字过多;

·语言的更新周期长,跟不上需求的变化和新技术发展的步伐;

·开发工具昂贵,培训费用高,支持文档少;

·随着新技术的不断引入,ATLAS体系变得庞大、杂乱,出现了信号定义模糊、相似信号的属性难以区分、同一术语重复定义、关键字定义重复等问题。

上述问题限制了ATLAS的进一步发展,SCC20意识到这个问题,开始把各种软件新技术应用到ATLAS的升级版本中,对ATLAS进行变革,推出了ATLAS2000。ATLAS2000是多层次结构的语言,其基础由内核和原语组成,用于创建测试应用需求。ATLAS2000语言体系的模块化结构能够封装可复用的测试单元,这样的结构使用户能够开发和描述基于底层单元的复杂测试需求。 LcpvN6En9tHYBzqwdU5gDNwy77U3bdQoG/v2pYm6rukTI7T0nr0/2f8/cdRCw28z

点击中间区域
呼出菜单
上一章
目录
下一章
×