PDF《面向嵌入式实时软件的需求规约语言及检测方法》

Vol.

15, No.11 ?2004 Journal of Software 软件学报1000-9825/2004/15(11)1595 面向嵌入式实时软件的需求规约语言及检测方法 ? 舒风笛 1+ , 毋国庆

2 , 李明树

1 1 (中国科学院 软件研究所,北京 100080)

2 (武汉大学 计算机学院 计算机科学系,湖北 武汉 430072) An Embedded Real-Time Software Oriented Requirements Specification Language and Checking Methods SHU Feng-Di1+ , WU Guo-Qing2 , LI Ming-Shu1

1 (Institute of Software, The Chinese Academy of Sciences, Beijing 100080, China)

2 (Department of Computer Science, Computer School, Wuhan University, Wuhan 430072, China) + Corresponding author: Phn: +86-10-82620803, E-mail: [email protected] Received 2004-04-01;

Accepted 2004-06-11 Shu FD, Wu GQ, Li MS. An embedded real-time software oriented requirements specification language and checking methods. Journal of Software, 2004,15(11):1595~1606. http://www.jos.org.cn/1000-9825/15/1595.htm Abstract: Aiming at the requirements specification and related checking of embedded real-time software, a visual modeling language, RTRSM* (real-time requirements specification model*), which is compositional and based on hierarchical and concurrent finite state machine, is proposed. It uses state transitions with duration and scheduled events to describe timing constraints, and can support the description of interactivity and timing constraints effectively. Additionally, RITL (real-time interval temporal logic), a kind of prepositional temporal logic, is presented to make up for RTRSM*'

s defect description of global system properties, which is the drawback of operational specification languages. Interpreted over timed state sequences, RITL is able to deal with the description of both point-based and interval-based metric temporal properties, and supports the property description of RTRSM* models naturally and comprehensively. The verification and validation of the resulted requirements specification, especially issues with respect to the reachability graph of RTRSM* models with finite system states and the simulation execution of the specification, are also explored. Key words: embedded real-time software;

requirements specification language;

requirements specification checking;

reachability graph 摘要: 针对嵌入式实时软件需求规约及其检测问题,提出了基于层次并发有穷状态机的可合成的图形化建模语 ? Supported by the National Natural Science Foundation of China under Grant Nos.69873035,

60273026 (国家自然科学基金);

the K.C. Wong Education Foundation, Hong Kong, China (香港王宽诚教育基金) 作者简介: 舒风笛(1976-),女,湖南邵阳人,博士,主要研究领域为需求工程,形式化理论和方法;

毋国庆(1954-),男,教授,博士 生导师,主要研究领域为软件工程,需求工程,软件形式化理论;

李明树(1966-),男,博士,研究员,博士生导师,主要研究领域为智能软件 工程,实时系统.

1596 Journal of Software 软件学报 2004,15(11) 言RTRSM*(real-time requirements specification model*),利用转换有效期和事件预定机制来描述时间限制,能够较好 地支持系统交互性和实时性的建模.为弥补 RTRSM*作为操作性规约语言不便于性质描述的问题,提出了命题时序 逻辑 RITL(real-time interval temporal logic).该语言以时间状态序列为语义模型,具有基于区间和时间点的量化时间 属性描述功能,能自然、全面地描述 RTRSM*模型性质.介绍并讨论了基于两种语言的规约检测方法和技术,主要包 括系统状态空间有穷的 RTRSM*模型状态可达图的相关问题和规约的模拟执行. 关键词: 嵌入式实时软件;

需求规约语言;

需求规约检测;

可达图 中图法分类号: TP311 文献标识码: A 形式化需求规约语言有助于准确而无二义性地理解和描述目标系统,支持规约的形式化检测,但它又应具 有一定的表达能力,能自然地对现实世界实体进行建模并支持领域特征描述.嵌入式实时软件(embedded real-time software,简称 ERS)的主要领域特征为事件驱动、 具有复杂动态交互行为和严格时间限制.操作性规约 语言便于描述外部刺激、系统动作和状态等建模实体,却不适合于性质描述;

而单纯的描述性形式系统,如逻辑, 则正好相反.许多研究工作将两者结合起来,得到的软件需求规约(software requirements specification,简称 SRS) 包括用操作性规约语言描述的系统模型及用断言式语言描述的期望模型满足的性质.SRS 正确性的检测内容 主要包括一致性、完备性等独立于具体应用的性质和用户需求的确认. 与ERS 的需求规约及其检测相关的代表性工作包括:基于状态转换的 Statecharts[1] 、SCR[2] 、时间自动机 (timed automata,简称 TA)[3] 、时间转换系统(timed transition system,简称 TTS)[4] 、TPTL[5] 、XYZ[6] 等多种时序 逻辑,Modechart/RTL[7] 、TTM/RTTL[8] 等双语言框架,以及相应的原型化和形式化检测方法和工具,如基于 Statecharts 等的 Statemate[9,10] ,形式化验证工具 SPIN[11] 、PVS[12] 等.这些研究各有其侧重点.Harel 提出的 Statecharts 面向复杂、交互式系统,通过引入状态的层次、并发和广播机制对传统状态转换图进行扩充,简洁且 高度结构化,具有良好的形式化语义,但其时间限制描述能力较弱;

Timed Statecharts[13] 较之传统的 Statecharts,时间限制描述能力得到加强,但其形式过于复杂.实时UML[14] 是在基本UML 基础上引入了起源于ROOM(real-time object oriented modeling)[15] 的便于设计复杂嵌入式系统的结构,其描述单一对象行为的状态图 与传统的 Statecharts 没有本质区别,主要通过交互图和活动图进行时间限制建模.此外,虽然已有一些 UML 形式 化语义和验证研究[16~18] ,但仍不成熟,尤其是时间限制方面.Modechart[7] 强调的是控制和实时的描述,没有转换 操作机制.TA 和TTS 为较为成熟的实时模型,分别主要通过时钟变量和转换的上下时限来支持时间限制的描 述,但两模型对于反应性的支持不够自然和直接,且其分析机制较为复杂.对于逻辑语言而言,也没有任何一种 单独的逻辑可以说绝对优于其他逻辑[19] . 针对ERS 的需求规约及其检测问题,我们提出了需求建模语言RTRSM*(real-time requirements specification model*)及其性质描述语言 RITL(real-time interval temporal logic).前者继承了 Statecharts 的层次并 发状态和广播通信机制,通过增加转换有效期和事件预定机制来描述时间限制,能够较好地支持交互性、实时 性和一定数据计算的建模,图形化且具有严格形式语义.RITL 为基于区间限制的命题时序逻辑,能够支持 RTRSM*模型的性质描述,尤其是时间性质.两种语言共同组成了适合于 ERS 的需求描述符号系统. 本文首先给出了两语言的语法和语义,举例说明了 RTRSM*的时间性质描述机制,介绍并讨论了相应规约 检测方面所做的工作,包括模型系统状态可达图的构造算法及相应性质验证,规约一致性和完备性检查方法,两 语言的 PVS 语义嵌入及规约的模拟执行等.

1 需求建模语言 RTRSM* 1.1 RTRSM*概述 RTRSM*以RTRSM[20] 的模板为基本描述单元,每个模板对应一层次并发有穷状态机 HCA,其具体表现形 式为包括数据和接口定义的表格、 状态转换图及其等价的规则集.HCA 继承了 Statecharts[1] 的层次和并发状态, 即状态包括基本状态和实际为状态机的超状态,后者又分为与、或状态.模型所有状态构成一个以初始状态为 舒风笛 等:面向嵌入式实时软件的需求规约语言及检测方法

1597 根的树型结构. 定义 1(HCA 的规则). HCA 中的每条转换对应于一条形式如下的规则: 源状态, 触发事件(事件属性)=>

目的状态, WHEN 卫士条件, DO 操作 D 其中,非负整数 D 为转换有效期,缺省为 0.含义为:当源状态活跃、 触发事件发生且卫士条件为真时,该转换可执 行,而在成为可执行后 D 时间单元内,该转换只要有效(源状态活跃且卫士条件满足),可且必定实际执行(D 为0则立即执行).转换的执行过程是:退出源状态,执行操作(可包括:变量赋值,系统内外部通信指令的发送和事件 的预定、取消等[21] ),然后进入目的状态,具有原子性和瞬间性. 默认转换的源状态为空,目的状态非空,D 为0,卫士条件缺省为真,无触发事件,一旦进入该转换所在超状 态,则立即执行.对于其他转换,源状态、触发事件和目的状态非空,其他项可选.源状态和目的状态必须为兄弟. 定义 2(转换的一致性). 两转换一致,当它们相同或源状态正交(不存在祖先关系)且操作中无变量写冲突. 对于一个转换集合 T,若其中任何两转换都一致,则称 T 一致. RTRSM*不允许不确定性.允许可能存在的不确定性便于建模,但可能隐藏错误,且判断一个确定行为是否 可接受比证明所有可能的不确定行为都可接受要容易.可将允许的多种情况抽象统一,正体现了规约能且正好 能区分系统所期望行为与其他性质.RTRSM*通过顺序执行以下优先级原则消除可能存在的不一致:高层转换 具有高优先级;

外部事件触发的转换优先级最高,被延迟转换的执行优先级最低. 1.2 时间限制的描述 嵌入式实时系统的时间限制反应在外部刺激(包括时间的流逝)及系统反应上,基于 RTRSM*,前者可描述 为能触发状态转换的事件,后者则为相应由当前系统状态所决定的转换的实际执行,由于其瞬间性,即为其目的 状态的进入.RTRSM*采用隐含时间信息,利用事件及其预定机制和转换有效期来描述.Statecharts 的理想同步 假设[1] (系统总比外部环境动作更快,在收到刺激后马上作出反应)能简化系统需求的分析,但该假设并不总能被 满足,且不便于充分、完全地描述实际中常见的以时间段形式给出的时间需求.RTRSM*转换带有有效期,能有 效克服以上两点.下面通过对经典的铁路交叉路口系统(railroad crossing system,简称 RCS)[22] 的特例――标准 RCS――稍加修改,来说明如何用 RTRSM*来描述时间段形式的时间需求. 用软件来控制一个通常打开的铁道口控制门.由探测器

1 检测火车的临近:当火车经过探测器

1 时,该探测 器发送通知 near;

火车在经过该探测器后,至少

300 个时间单元后才到达该路口.探测器

2 检测火车是否通过该 路口,若通过则发送通知 passed.火车通过路口与经过探测器

1 最多相隔

500 个时间单元.控制器在接收到 near 消息后

100 个时间单元时向门发送关闭的控制命令 lower,并在接收到 passed 消息后

100 个时间单元时向门发 送打开的控制命令 raise.门的 关闭和打开各需 20~50 个和 100~200 个时间单元才能完成. 根据火车调度方案,从一列火 车离开铁道口到下一列火车到 达探测器

1 至少间隔

100 个时 间单元.在该例中,门的关闭和 打开都是持续动作,作为状态 来描述,其时间需求以常见的 时间段形式给出.若转换是一 旦满足则立即执行,虽然所........