基于时间事件因果关系检测的工业软件的需求确认方法

尹玲 ,  陈小红 ,  安冬冬 ,  谢越

武汉大学学报(理学版) ›› 2024, Vol. 70 ›› Issue (3) : 302 -316.

PDF (3513KB)
武汉大学学报(理学版) ›› 2024, Vol. 70 ›› Issue (3) : 302 -316. DOI: 10.14188/j.1671-8836.2023.0208

基于时间事件因果关系检测的工业软件的需求确认方法

作者信息 +

Checking of Timed Casual Relation of Events for Requirements Validation of Industrial Software

Author information +
文章历史 +
PDF (3596K)

摘要

工业软件深度参与研发设计、生产制造、运营管理和维护服务等方面,软件的行为符合业务的需要至关重要。因此,工业软件的开发需要进行需求确认,即确认系统的行为满足利益相关者(应用方的操作人员,通常是生产和运维中涉及的各方面的工作人员)的要求。业务方面,利益相关者的期望通常表现为关心的事件间的因果关系。针对工业软件的时间融合于行为、复杂度高、规模大等特点,提出一种基于时间事件因果关系检测的需求确认方法,检测用UML/MARTE+CCSL模型表达的系统行为是否满足相应的时间事件因果关系。包括:定义时间事件因果关系表达利益相关者的期望;抽取模型的多图协作下的系统整体行为生成CCSL(clock constraint specification language)规约;结合模型检测技术和社区发现算法检测该行为规约是否满足时间事件因果关系。通过比较实验评估了方法的有效性和实用性,特别是引入社区发现算法处理规模大、复杂度高的规约效果显著。

Abstract

Industrial software is essential in product design, development, maintenance, and services. It is crucial to ensure that the software behaviors meet specific business needs. Therefore, industrial software development necessitates requirements validation, explicitly confirming that system behavior meets stakeholders' expectations(operators of applied companies). These expectations are often in the form of event casual relations with timing constraints. Industrial software is time-critical, large and highly complex. Considering these features, we proposed an approach to check event-causal relations with timing constraints on UML/MARTE+CCSL models for requirements validation of industrial software. Event casual relations with timing constraints are defined for expressing stakeholders’ expectations; CCSL(clock constraint specification language) specification is built for capturing the overall behaviors under the cooperation of multi-diagrams in the model; community detection algorithm is integrated with model checking techniques to accomplish the checking of CCSL specification against timed event-causal relations. The effectiveness and practicability of our approach are illustrated by comparison experiments, especially the benefits of dealing with large scale and high complexity by bringing in a community detection algorithm.

Graphical abstract

关键词

基于模型的系统工程 / 需求确认 / 模型检测

Key words

MBSE(Model-Based Software Development) / requirements validation / model checking

引用本文

引用格式 ▾
尹玲,陈小红,安冬冬,谢越. 基于时间事件因果关系检测的工业软件的需求确认方法[J]. 武汉大学学报(理学版), 2024, 70(3): 302-316 DOI:10.14188/j.1671-8836.2023.0208

登录浏览全文

4963

注册一个新账户 忘记密码

0  引 言

工业软件依托工业生产需求,将关键流程和知识以软件的形式封装,按需融入设计制造、经营管理、运维服务等流程。当前,我国工业软件产品主要集中在办公自动化软件等低门槛类型,在深度参与工业制造和企业运维的领域占有率较低[1]。深度嵌入工业制造和企业运维代替人完成部分工作,特别需要软件满足操作者的期望。以定制化为宗旨,深挖企业应用需求,满足操作者在开展生产、运营、维护服务等方面业务工作的具体需要,也是我国工业软件赢得市场的关键。需要在工业软件开发过程中高度重视和认真实施需求工程,包括需求捕获、需求分析、需求确认等。需求捕获和分析方面已有较多工作,但是,需求确认方面的工作很少。

工业软件面向复杂精细化的场景业务,通常复杂度高且规模大,宜采用基于模型的系统工程(Model-Based Software Development,MBSE)进行软件设计和开发 [2]。MBSE从需求阶段开始即以模型(而非文档)的不断演化、迭代递增实现工业软件的系统设计和开发。模型的抽象能力可以处理复杂场景的描述,满足高复杂性、不确定性等要求,支持设计、开发和验证等多项活动。因此,本文探索MBSE方案下的工业软件模型的需求确认的方法。

工业软件涉及的利益相关者众多,例如,企业应用方生产和运维中涉及到各环节的操作人员都是工业软件的终端用户,生产涉及的有关部门(例如环境、交通)的对接人员也是利益相关者。进行软件开发的工程师是软件厂商的开发人员,并不一定是工业领域应用方面的专家,因此在工程师与应用方领域专家交流并根据自己的理解构建了模型后,再跟利益相关者进行需求确认,可尽早发现问题,确保所开发的系统最终满足利益相关者的需要,提高开发效率和软件质量。模型是工程师在自己对需求的理解的基础上给出的解决方案,以怎么做(how)的视角描述系统。利益相关者关心的是系统运行的效果,他们的需求是做什么(what)的视角。两者之间存在差异,而且利益相关者通常不熟悉建模技术和建模语言,因此,如何从模型中提取信息并表达为利益相关者熟知的形式一直是基于模型的需求确认的研究重点。与利益相关者沟通的语言是自然语言(Natural Language,NL),将模型生成NL描述是需求确认工作的一大分支[3]

目前将模型生成NL描述的工作[3~9]不能支持工业软件需求确认的要求。工业软件有多形态时间需求密切融入行为的要求,例如,塑料成型工艺中注射行为的发生具有严格的时间要求并且刻画形式是塑料的加热温度。工业软件的应用场景多样,业务逻辑复杂,这些都对需求确认提出了更高的要求:1) 时间是多形态的并且密切融入系统行为,需求确认需要分析融入了时间需求的系统行为;2) 模型一般包含多个图,从不同视角建模,需求确认需要分析多图协作下的整体行为;3) 模型中通常包含很多设计考虑和内部实现细节,系统的行为是多个图上的大量元素复杂交互的结果。利益相关者不关心内部具体交互,为免陷入实现细节,应从模型中抽取系统的外在行为,即系统与外在环境的交互表现,用于给相关利益相关者进行确认。现有工作主要针对一般信息系统,强调对领域概念和业务流的确认,直接从图形翻译成自然语言描述,包含过多细节,缺少从图上元素到系统外在行为表现的抽取,也不支持图间的关系和跨图协作。

针对以上问题,本文提出了基于时间事件因果关系检测的工业软件的需求确认方法。针对多形态的时间需求与行为需求相融合的特点,定义时间事件因果关系描述表达利益相关者对系统行为的期望。以工程师构建的UML/MARTE+CCSL模型为输入,整合模型中多个图和图上的CCSL(clock constraint specification language)约束,生成描述系统整体行为的CCSL规约,用模型检测器UPPAAL检测该规约对时间事件因果关系的满足性,实现从模型的复杂细节到利益相关者关心的系统对外交互表现的抽取。根据模型检测结果生成用于需求确认的NL描述。

为了解决工程师难以对模型形式化以及模型检测技术在大规模系统上容易出现状态空间爆炸的问题,本文做了以下工作:1) 模板化CCSL规约和时间事件因果关系到UPPAAL的输入形式的转换,模板公开于Github(https://github.com/lyin-163/requirements-validation-experiment),使用时,只需要声明模板的实例即可,语法简单,工作量小;2) 引入社区发现算法COPRA[10],将CCSL规约拆分成多个组,并行进行模型检测再合并检测结果,避免空间爆炸。

1  相关工作

1.1 模型语言

工业软件开发面临诸多挑战,目前尚无解决所有问题的统一框架或平台,但是针对复杂系统工程问题的MBSE有很大潜力,已有成功应用[11]。UML(Unified Modeling Language)是MBSE中使用最广泛的建模语言。MARTE(Modeling and Analysis of Real-Time and Embedded system)是UML在实时嵌入式系统的扩展,提供了时间、硬件平台、资源等领域建模元素。CCSL最初作为MARTE的伴随规约语言提出,现已逐渐应用于各种有时间行为融合要求的系统的建模。

CCSL以时钟约束访问MARTE的多形态时间。一个时钟c=<I,≺,u>,包括时刻集合I,反自反、传递的二元关系≺(严格先于)和单位uc[i]∈I表示c的第i个时刻。逻辑时钟抽象地表达事件的发生情况,滴答一次表示一个时刻发生,也代表对应的事件发生一次。逻辑时钟不必遵循物理时间的匀速规律,事件发生则滴答;可以通过时钟关系为逻辑时钟关联物理时间。除≺外,还有3种时刻关系:≡表示同时,≼表示先于或同时,#表示不同时。时钟约束的语义建立在时刻的关系上,如表1所示。CCSL规约由时钟和约束构成。一个CCSL规约的一次运行是一个时钟滴答集合的序列,即序列的每个位置是一个时钟滴答的集合,表示在该时刻集合中的时钟滴答。具体哪些时钟滴答满足规约包含的所有时钟约束的语义(即时钟约束间取交)。

因此,本文选择UML/MARTE+CCSL作为输入模型,其优势见表2

1.2 系统行为的确认

需求确认需要利益相关者的紧密参与,因此研究的热点之一是如何从模型中抽取适合利益相关者确认需求的信息。现有工作可分为静态和动态两类:前者从静态模型中抽取结构信息,对领域概念进行确认[2~4];后者从动态模型中抽取行为信息,对系统行为进行确认[5~9]

关于系统动态行为方面的需求确认,相关工作可以分为三类:

1) 基于Control-Flow对应,例如Leopold等[6]提出的根据BPMN中活动和迁移的图形表示抽取活动之间关系的方法。这类方法可以很好地说明模型的结构,但弊端明显,缺少外在交互的抽取,每个活动间的关系都会映射为一个语句,生成的描述冗长且包含很多利益相关者不关心的细节。

2) 基于Case对应,关注某个活动或活动序列的运行,例如Dijkman等提出的日志统计方法[7],从BPMN的运行日志中查找特定数据的出现中总结数据出现的模式,提供某一活动运行的信息。这类方法可以生成形如“for most cases that contained the activity A, the throughput time was long”的描述,但是不考虑活动之间的关系。Fontenla-Seco等将日志分析与流程分析结合[8],弥补这一缺点。

3) 基于性质检测,检测模型是否满足某些性质来生成对系统行为的描述。目前这类工作较少,代表性工作为Mothia[9],在工程师定义的pattern和criteria的基础上,将一个活动图的活动组合的pattern抽取出来,判定它是否符合某一criteria。但是它的检测主要依靠图的结构关系,对模型动态行为的语义分析不够。

2  本文方法思路

以上工作都针对一般信息系统,受限于输入模型的表达能力和所采用的方法,缺少多形态时间的表达和时间需求的融入,也不支持对时间需求的定性和定量的分析。

本文关注系统动态行为方面的需求确认,与本文目标最贴近的代表性工作为Mothia框架[9]。Mothia查询输入模型的图中元素之间的关系是否满足一些条件,根据结果生成自然语言问题。由建模专家定义查询条件,支持Next、Always和All算子。这些算子有一定的时序语义,但是对多形态的时间需求和时间与行为融合的支持不够。工业软件的模型复杂、图多,图中元素也多,利益相关者很难从众多这样的问题中推得系统的全貌。并且,这样的问题包含很多利益相关者不关心的具体设计细节,也没有体现出利益相关者关心的方面。例如,对于本文驱动案例,机器人投递系统,利益相关者不关心具体的任务调度策略或者具体的传感器配置参数,而关心系统的外在表现(在提交投递请求后多久能收到反馈;机器人在接近目标位置时,能否安全地停下来而不发生碰撞等)。这些外在表现是内部设计细节交互作用的结果,任务分类的投递方式和配置参数会影响系统整体的运行表现(多久能收到反馈)。因此,需要从图形元素中整合出系统的行为,并抽取出利益相关者关心的方面,再生成需求确认问题,而不是就图形元素之间的关系直接生成需求确认问题。Mothia以单个图为单位查询,不支持跨图。而大规模工业软件多采用分布式开发,不同团队构建的图描述不同的模块或对象,同一模块或对象也可能由多个图从不同角度建模,需求确认需要考虑图间的协作。因此,工业软件的需求确认,首先要整合模型的所有图和约束,得到系统的整体行为,再构建利益相关者关心的系统外在表现的查询条件,检测系统整体行为是否满足查询条件,根据结果生成NL描述。

为此,我们提出如图1所示的方法。用CCSL规约作为整合模型的载体,将由图形表达的行为(明确的、无歧义的部分)表达为CCSL约束,得到的约束与模型中原有的伴随约束一起,构成CCSL规约。该规约即是整合模型得到的系统的整体行为,在CCSL的形式化操作语义基础上,以时钟滴答序列的形式给出所有可能的行为轨迹。目前,图中灰色背景框部分需要工程师和利益相关者完成,蓝色框图内部分已实现自动化。

以时间事件因果关系的形式组织和描述利益相关者对系统行为的期望。事件因果关系在需求文档的描述中占比最大,贴近利益相关者的思考方式[29]。以事件因果关系的形式组织需求确认问题,有利于利益相关者理解模型运行的效果,评估系统是否符合自己的期望,思考是否有遗漏的需求。工业软件与物理世界环境交互密切,交互的时间要求高并且度量多形态,针对这一需要,我们对事件因果关系在时间表达方面上进行了扩展。例如,机器人接近目标位置时能否安全地停下来不发生碰撞,表达为TargetDetectedstopped,即检测到目标(即TargetDetected事件发生)后,在40 cm内停下(即stopped事件发生)。

将利益相关者的期望表达为时间事件因果关系后,用模型检测技术检测是否被CCSL规约满足。CCSL规约是整合了多图交互协作和设计细节的系统整体行为,时间事件因果关系表达了利益相关者关心的外在表现,因此根据满足性检测的结果生成的需求确认问题(如表3所示),具有从包含设计细节的模型行为抽取利益相关者关心的系统行为外在表现的效果。

除了支持对内部细节到外在表现的抽取,模型检测技术的应用还可以带来形式化的其他优点。它是严格的、基于语义的,其中的形式化模型和性质的描述方法可以重用到其他的形式化分析和验证工作中做安全性验证、可靠性验证等等,方便将我们的工作与其他的需求分析、系统验证工作的作结合。但是,模型检测也有缺点:1) 形式化语言不易学习掌握;2) 时间成本高,如果模型规模大容易状态空间爆炸无法得出有效结果。

对于问题1),我们用模板的形式固化CCSL规约和时间事件因果关系到UPPAAL输入模型的转换,使用者无需掌握具体的UPPAAL的语法语义,只需要根据模板的参数说明声明实例即可。

关于问题2),在CCSL规约中增加某一时钟约束不一定会使状态空间增大。例如,在a≤b的基础上再添加a≡b(约束时钟ab必须同时滴答)会缩小状态空间。但是,一般情况,时钟和约束的增加会增加规约的复杂性,使得转换得的UPPAAL模型的状态空间增加。实验发现,时钟和时钟约束的数量与检测成本之间呈正相关,数量超过1 000后检测成本增加显著,数量达到3 000量级时,运行UPPAAL验证会提示内存耗尽,无法给出结果。为解决这一问题,我们将社区发现算法COPRA引入模型检测过程中。

3  时间事件因果关系的定义

事件因果关系的研究已广泛用于需求建模[30]、需求一致性检测[31]等方面。以上工作角度不同,但对事件因果关系的定义相同:事件为系统或环境中感兴趣的情况的发生(happening of interest),用来抽象状态的改变、条件的满足、特定情形的出现、动作的发生等等;事件因果关系有两种:蕴含,表示如果条件满足(即条件事件发生),那么效果事件发生;逻辑等价,在蕴含基础上进一步约束,条件不满足则效果事件不可以发生。

事件因果关系本身有一定的时序含义,效果事件不能比条件事件先发生。但是,没有明确效果事件是在条件为真时马上(或者说满足的同时)发生,还是满足以后发生,是否有发生时间的具体量化要求等。不足以描述工业软件中的多形态的并且与行为紧密融合的时间需求。因此,我们在其中融入多形态的时间需求,定义时间事件因果关系,见表4

时间事件因果关系中提供三类时间需求的表达:同时、重叠、严格先于。同时指条件和效果的时间约束期限一致,例如系统进入故障状态则一直发出报警声音直至维修人员开始维修,即故障状态结束立即进入维修状态。作用于事件上,表现为条件事件和效果事件的同时发生或条件满足则效果事件立即瞬时发生,如CR1。重叠指条件满足后,条件满足的状态与效果事件的发生在时间上有重叠。例如,系统就绪则可以接收投递请求,直到不再处于就绪状态。作用于事件上,表现为表示条件从不满足到满足这一状态改变的事件发生后,效果事件可以发生;效果事件发生在描述条件不再满足这一状态改变的事件发生前,如CR2;可以约束效果事件的发生次数,如CR3。严格先于关系适用于条件和效果都是瞬时动作的情况,例如,用户输入的投递请求不符合规则,则弹出错误信息。作用于事件上,表现为条件事件发生后效果事件发生,如CR4。

时间事件因果关系除了支持定性的时间需求,也支持定量的需求。例如CR5,约束效果事件在条件事件发生后的一段时间内必须发生,以多形态时钟p的单位量化。在蕴含关系和逻辑等价关系中融入时间需求,分别得到CR1~CR5和CR6~CR10的定义。效果事件可以取反,即条件满足则约束效果事件不能发生。结合时间需求后,定义为CR11~CR18。条件可以组合,提供析取和合取两种方式,如表4中CR19即为条件组合算子与CR4的结合。

4  方法实现

4.1 CCSL规约的构建和拆分成组

将输入模型中由图形表达的行为表达为CCSL约束,它与模型原有的伴随CCSL约束一起,构成描述系统整体行为的规约。我们以前的工作[26]给出了顺序图到CCSL的转换方法,文献[32]给出了活动图到CCSL的转换方法。本小节只给出状态图到CCSL的转换算法,见算法1

首先,遍历状态图,建立其结构化表示GSC=<S,T,P,L>,其中,S为状态图上顶点(Vetex)的集合,P={Kind,CB,CS,IT,OT}为S上函数的集合:Kind(s)指顶点s的分类,包括状态(细分为简单状态、组合状态)和伪状态。若s为状态,CB(s)为s包含行为的集合;若s是组合状态,CS(s)为s所包含的顶点的集合;IT为s的迁入迁移的集合,OT为s的迁出迁移的集合。T为迁移的集合,L={Kind,TR,

GR,AC,SV,TV}为T上函数的集合,Kind(t)为迁移的类型,包括耗时迁移、非耗时迁移和完成迁移;TR、GR和AC为迁移的触发、条件和动作;SV和TV分别是迁移的源顶点和目标顶点集合。

然后,遍历GSC,为每个顶点和迁移定义CCSL时钟。识别出状态机运行中状态和迁移的情况变化点作为感兴趣的事件,定义一个时钟。例如,为状态定义s.start,s.exit和s.left三个时钟,分别表达进入状态、退出状态和离开状态。状态中如果定义了行为,也为每个行为定义两个时钟分别表示行为的开始和结束。为迁移定义以下时钟:reached,表示状态机的运行到达该迁移的源顶点;begin,迁移开始执行;traversed,迁移正在执行;completed,迁移执行完,状态机进入其目标顶点。

最后,根据UML官方文档给出的状态机的语义添加时钟约束。

篇幅所限,以一个简单的状态图为例说明转换的正确性(图2)。状态图2(a)刻画的状态机运行的语义如图2(b)所示,图中的大括号表示其中的事件同时发生。根据UML官方文档对状态图语义的说明,图2(a)的合法运行序列共190条,篇幅所限,图2(b)只展示4条。根据CCSL的操作语义[33]可以得到规约的语义图2(d),并证得图2(c)与(d)语义等价。

COPRA可以从网络中识别出若干个可重叠的社区,本文用它对CCSL规约分组。算法2给出了基于COPRA的CCSL规约拆分算法。首先构建描述CCSL规约的拓扑关系的网络,节点为时钟,边为时钟约束。然后,调用COPRA(其实现方法见文献[10]),得到每个社区包含的节点。对于单节点社区,统计该节点与其他非单节点社区中节点关联的边数,将该单节点记入边数最多的社区(有多个相同,则随机选一个)。一个社区的时钟,加上原规约中这些时钟之间的时钟约束构成一个组。因此,每个组本质上也是CCSL规约。

拆分会造成信息丢失,但不一定会影响对时间事件因果关系的检测结果。如表5的例子,影响某一时间事件因果关系的时钟和约束都划分在同一组(图3,蓝色和黄色底色的节点分别为R1和R2所涉及事件对应的时钟),分别在两组上检测R1和R2的结果与在原规约上检测这两个关系的结果相同。这是理想情况,实际案例可能无法达到这样的拆分效果。第5节将通过实验量化评估拆分对检测结果准确性的影响。

4.2 CCSL规约和时间事件因果关系到UPPAAL的转换

CCSL与UPPAAL的语义在形式上不匹配:CCSL的语义是时钟滴答序列,而UPPAAL的语义是UPPAAL NTA状态迁移序列;一个规约的CCSL约束之间取交,映射到状态转换形式的语义上为同步积,而一个UPPAAL NTA内是自动机异步组合的。为解决这一问题,我们采用coincident instant mechanism机制,将CCSL规约运行的一步分成3个阶段,start→firing→end。在start阶段,时钟约束根据当前状态给出相关时钟的滴答要求;firing阶段,综合所有滴答要求,决定每个时钟在当前步是否滴答;end阶段,根据滴答决定更新时钟约束的状态。一个CCSL规约转换为一个UPPAAL NTA,包含6部分:全局声明、模型声明、逻辑时钟约束模版、物理时间关联约束模版、初始进程模版和逻辑时钟演变模版。在模型声明中声明模板的实例,各实例相互作用下的状态迁移模拟CCSL规约的运行。具体的转换方法、转换模板以及转换的正确性证明见我们的工作[33]表6以CR1的UPPAAL模板为例说明用UPPAAL形式化时间事件因果关系的思路。

基于CCSL到UPPAAL的转换,用LogicalClock表达时间事件因果关系里的事件。以表示CCSL时钟实际滴答情况的atk作为迁移条件,不更改滴答要求(cnt和mt)的值,因此,不影响模型本身的行为。

判定事件是否满足三种时序关系的方法如下:

• 同时:如CR1的观察者模板所示,记录每一步(即start?和end?之间)的时钟的滴答决定,条件事件和效果事件在同一步滴答则满足同时这一时序关系,否则不满足。

• 重叠,即效果事件e发生于条件的一对开始事件cs和结束事件ce之间。用两个观察者模板ObAL和ObIO表达:ObAL判断交替关系(条件的开始和结束交替发生);ObIO判断蕴含和匹配关系(e发生在一对cs和ce之间)。

• 严格先于,期限要求为条件满足之后的t on p时间内。在判断条件事件严格先于效果事件的基础上,添加计数x,在条件事件发生后计数p时钟的滴答次数,若观察到效果事件在pt次滴答内发生则满足,否则进入Violated状态。

以析取(ObDC)为例说明条件组合的表达。条件组合约束条件间的关系,与某一时间事件因果关系联合使用,因此本身没有TCTL表达式。条件组合可以嵌套,例如,要检测(c1c2c3)simultaneouse,声明以下实例:Disobj1=ObDC(c12,c1,c2); Disobj2=ObDC(c,c12,c3); CR1obj=ObIS(c,e); 然后检测:A[] ! CR1obj.Violated and E<> CR1obj.Satisfied。

4.3 并行检测及结果整合

每个UPPAAL客户端检测拆分得到的一组CCSL规约。如果时间事件因果关系cr j 涉及的时钟都在某一组CCSL Group i 中,则检测其UPPAAL NTA i 是否满足性质pj,否则不检测。Group i 的检测结果为{rij | rij ∈{0,1,na}, j∈{1,…,m}},rij =1表示经检测Group i 满足cr j; rij =0表示经检测Group i 不满足cr j; rij =na表示没在Group i 上检测cr j。如算法3所示,以少数服从多数,次数相同则小组服从大组的原则汇总整合各组检测结果成最终结果。从检测结果到NL描述,采用模板映射方式。我们为每类时间事件因果关系提供检测结果为真和为假两个NL模板,在生成NL描述时根据检测结果套用相应模板(代入具体的事件名称和时钟名称)。如表7所示,NL描述模板与时间事件因果关系的语义(表4)直接对应。

生成需求确认问题时,每条描述下设置选项,如图4所示。第1、2选项反映利益相关者认为模型的行为是否符合自己的期望。利益相关者是某一方面的专家,若问题不在他关心的需求范围,可选第3选项;若在,但认为描述得不清晰或者是内部设计细节而无法回答,可选第4选项。

5  实验和评估

5.1 研究问题

问题1 方法的效用如何?需求确认的最终目的是确认模型符合利益相关者的期望,方法的效用主要取决于生成的NL描述能否帮助利益相关者理解模型以及判断模型的行为是否符合期望。工程师和利益相关者共同参与需求确认,方法的效用还体现在工程师端,能否发现隐藏的缺陷,能否节省工作量提高工作效率等。因此,除了对生成的需求确认问题的客观量化分析,我们还通过问卷和访谈收集工程师和利益相关者的主观反馈,综合评估方法的效用。

问题2 方法的实用性如何,能否应用于大规模软件?调整CORPA算法的参数v可以控制拆分CCSL规约的粒度。我们通过实验量化分析引入COPRA算法拆分CCSL规约的效果,评估对结果准确性的影响。

5.2 实验设置

问题1 同一案例上分别应用本文方法和Mothia方法,从耗时、有效性和满意度等方面进行比较。实验参与人员分为工程师和利益相关者两组。工程师组包括1名工程师和3名计算机系大三学生。工程师是中银金科高级软件架构师,有多年软件架构和开发经验。3名学生学习过软件工程和面向对象的设计方面的课程。利益相关者组5人,为医院工作人员。我们从医生、护士、药房工作人员、IT部门系统运维人员和中层管理人员中各选1人。请利益相关者回答需求确认问题,工程师与利益相关者就回答展开讨论,完成需求确认。设计工程师和利益相关者的问卷如图5,用于收集反馈。

实验流程:

1) 以医院内投递机器人为例开展应用实验。工作人员(医生、护士、药剂师)提交投递药品或者小型医疗器械的任务后,后台管理系统根据各机器人的状态分配任务。机器人接受任务后,进行任务调度,自主避障、导航并完成投递。管理员可以在后台管理系统上查询机器人和任务状态、管理用户和机器人、查看投递任务完成报表。构建案例的UML/MARTE+CCSL模型作为输入,包括活动图5个,顺序图7个,状态图7个,伴随CCSL约束263个。

2) 在模型上分别应用本文方法和Mothia方法,得到需求确认文档。Mothia暂不支持MARTE和CCSL,动态视图只支持用例图和活动图。因此,在应用Mothia前,先去除图中的MARTE构造型和CCSL约束,然后将顺序图和状态图转换为活动图表达,转换方法参照文献[34]。两个方法均需要工程师给出查询条件(本文方法是时间事件因果关系的形式,Mothia方法是用Next、All等算子连接图形元素的形式)。本文方法应用流程如图6所示。案例模型、CCSL规约、待检测时间事件因果关系、生成的需求确认文档、反馈问卷等所有实验结果见Github。

3) 向参与人员介绍项目背景和展示模型后,请工程师组根据自己对模型的理解和分析人工提出需求确认问题,作为回答反馈问卷的比较依据。请利益相关者回答需求确认文档中的问题。最后,请两组参与人员填写反馈问卷(每人两份反馈,分别针对本文方法和Mothia方法的应用)。

4) 就收集到的反馈,组织两组参与人员访谈。讨论收集的需求确认问题的回答,制定模型修改计划。将实验作为一次实施经验,讨论在需求确认活动中应用本文方法的主观感受。

问题2 评估引入COPRA拆分CCSL规约对模型检测实施成本和结果准确性的影响。最理想的基准实验是在大规模CCSL规约上的模型检测。然而,当我们尝试在驱动案例的CCSL规约上模型检测时,由于规模太大(3 038个约束),无法在有限时间内得到结果。因此,选择在3个比较小的例子,digital filter(DF) [25],switch control system(SC)[26]和rail-road crossing problem (RRC)[33],进行实验,每个例子一个CCSL规约和2个待查时间事件因果关系,通过比较未拆分和拆分后的检测成本和结果,推测在大规模规约上引入COPRA拆分的效果。

5.3 实验结果和讨论

问题1 表8对本文方法和Mothia方法在生成的问题数目、耗时等方面进行比较。以案例模型为输入,本文方法共生成274个需求确认问题,其中95个是跨图的(涉及两个或以上的图中的元素),覆盖18个功能点。Mothia方法共生成3 215个问题,也覆盖了这18个功能点,不支持跨图。本文方法支持跨图,因此,生成的问题对需求的描述更全面。两者生成的问题主要区别在于:1) 对于同一个功能点,本文方法比Mothia方法生成的问题数目少。例如,处理投递请求的功能,本文方法生成了32个问题,而Mothia方法生成了815个问题。2) 切入点不同,形式不同。本文方法从用户关心的业务逻辑出发,形式多样(18种时间事件因果关系);而Mothia从图形元素之间的关系出发,并且受限于查询算子的形式,生成的问题主要表达为模型的图形上的某一事件(或活动)发生后另一事件(或活动)会发生,或者某一事件(或活动)一直发生。3) Mothia方法包含更多内部设计细节,如问题“Can FormTaskList be the next action to be executed after the action PullUsrTasks?”利益相关者并不关心在处理投递请求时系统内部会调取用户的任务和形成任务列表以及它们之间的关系,这样的问题不应放入需求确认文档。本文工作则具备从交互和细节抽取整体行为外在表现的能力。耗时方面,本文方法使用的模型检测方法比较耗时,尽管规约拆分和并行检测改善了这一问题,单条描述的生成时间依然比Mothia方法长。但是,Mothia方法的问题数量多,因此总耗时更多。

如上一节讨论的,方法的效用需要综合考虑,除了表8中生成的问题本身相关的量化数据,还要考虑生成的问题在实际需求确认活动中使用的效果。我们设计了有效性指标和满意度两个指标,分别从利益相关者和工程师两个角度来评估。

有效性指标EF是在文献[9]提出的Efficacy指标的基础上进行设计的。文献[9]的Efficacy指标定义为#Pass+#Fail#Total-#NE,它没有考虑选项c(是关心的领域但是描述不清晰或属于内部设计细节,难以回答是否满足期望),以及利益相关者对反馈问卷的回答。这些方面都是方法效用的正面或负面反映,应纳入评估,本文设计的EF如下:

EF=#Pass+#Fail+#PM+#IN-#NE(#SN*#Total)-#DK+EU¯+HP¯

其中,#Total为生成的问题总数,#SN为利益相关者人数。统计所有利益相关者对需求确认文档的回答:#Pass,#Fail,#DK,#NE分别为选项a,b,c,d被选择的总数。统计所有利益相关者的反馈问卷:#PM和#IN分别为回答Q1和Q2列出的问题总数。EU¯HP¯分别为Q3和Q4得分平均值,各选项记值权重分为(非常,0.85),(中等,0.7),(一点,0.5),(很难,0.25)。

综合考虑节省的人工和生成的问题是否符合工程师的需要,满意度指标SF设计为:

SF=#SQ-0.5*(#NQ+#MQ)#EN*#Total+CS¯

其中,#EN为工程师人数,统计所有工程师的反馈问卷得到#SQ,#NQ和#MQ,分别为回答Q1、Q2和Q3列出的问题总数,#SQ-#NQ-#MQ#EN*#Total代表工程师对生成的问题的质量的评估,CS¯为Q4得分平均值,即应用方法需求确认所节省的人工。

表8所示,本文方法在有效性EF和满意度SF上都优于Mothia方法。本文方法检测模型工程师表达的时间事件因果关系实例并根据结果生成需求确认问题,工程师给出的时间事件因果关系实例表达了他认为需要向利益相关者确认的事件间的关系,即选取了系统的外在表现或交互而不是内部设计细节作为事件。因此,一个问题,要么不是该利益相关者关心的方面(选项c),要么利益相关者对它有明确的判断(可以或者不可以,选项a或b),很少被回答d选项。而Mothia方法生成的问题中,由于包含了大量的内部设计细节,选项d被选的比例很高。本文方法得到工程师组反馈问卷的回答中,#SQ:(#NQ+#MQ)为71∶29,而Mothia方法的为16∶84,可见本文方法可以更好地表达工程师的想法。另外,在利益相关者的反馈问卷中,本文方法得到的#PM和#IN也高于Mothia方法。因为,Mothia方法生成的需求确认问题是对模型的元素在图形上的关系的描述,更像是模型的“旁白”。而本文方法生成需求确认问题是在工程师经过思考给出的时间事件因果关系的基础上的,更适合用于探讨对需求的理解,有些可能是利益相关者还没有思考明确的,有些问题还启发出了更多原来需求确认文档中没有考虑到的需求,例如,“CMSAcceptCancel后的CabinEmpty的1次内,TakeoutGoods一定发生。”这一需求确认问题启发药房工作人员提出,尚未放入药品到机器人舱中的投递请求,如果用户取消投递并且系统同意后,应该通知药房工作人员取消备药。本文方法生成的需求确认文档,也帮助工程师发现了一些模型的问题,例如CR14(RtCancelReject,TakeoutGoods.start,NotifyDelivery,1)的检测结果为0,即“RtCancelReject发生后的NotifyDelivery的1次内,TakeoutGoods可以发生。”但是,对于已经在投递途中的药品,若系统拒绝取消投递的请求,在进行派送确认前应不允许将其取出。

综上,生成的需求确认问题的量化评价、工程师和利益相关者的主观反馈和在需求确认活动中所起到的作用,都证明了本文方法用于需求确认的有效性。

问题2 为量化评估拆分CCSL规约进行并行检测带来的影响,定义评价指标OB如下:

resultConsistency=0Pc(crj)P
timeRatio=executionTimegroupsexecutionTimespec
confidence¯=Average(confidence(crj))confidence(crj)=ONOONO+ZNO
OB=confidence¯×resultConsistencytimeRatio

其中,ONO,ZNO的计算方法见算法3c(crj)=1表示拆分前后检测结果一致,c(crj)=0表示不一致。

网格搜索参数v的取值,OB变化曲线如图7所示。DF例子收敛最快,RRC最慢,这里的收敛指v值的增加不再改变拆分结果。DF最小(整个CCSL规约只有14个约束),RRC最大(整个CCSL规约1 521个约束),规约越小收敛越快。观察收敛点v值下的拆分效果(表9):对小例子(例如DF)进行拆分并行检测在时间成本节省方面的作用不明显;随例子规模增大,拆分后并行检测的结果准确性稍有降低,但在时间节省方面的提升显著。由此推论,CCSL规约越大,拆分并行检测的收益越大。事实上,在驱动案例的整个规约上模型检测无法得到结果,拆分后并行检测可以,这也体现了本文方法的实用性。

6  结 语

本文提出了一种基于时间事件因果关系检测的工业软件的需求确认方法。以软件的UML+MARTE/CCSL模型为输入,分析图内行为和图间协作,整合多图协作下的系统的整体行为,描述为将多形态时间需求融入系统行为的CCSL规约;定义时间事件因果关系,从利益相关者关心的系统的外在表现出发,组织并构建待检测的性质;基于CCSL的形式化语义,通过CCSL到UPPAAL NTA的转换,利用模型检测技术检测CCSL规约是否满足性质,完成整体行为到外在交互表现的抽取。根据检测结果生成需求确认问题,供工程师和利益相关者进行需求确认。为应对CPS系统的大规模和高复杂性特点带来的挑战,引入了社区发现算法COPRA降低检测的复杂性,避免状态空间爆炸。通过案例研究和比较实验展示了方法的有效性和实用性。

作为还在起步阶段的工作,目前仅提供半自动化支持工具,大规模案例研究也需丰富。未来在完成全部自动化后,将探索更多大规模案例。方法改进方面,下一步研究工作包括:提供状态图外的UML其他动态视图到CCSL转换的规则。结合自然语言处理技术,从需求文档中自动生成利益相关者关心的时间事件因果关系。在目前方法基础上添加推荐算法,根据利益相关者的角色和兴趣等有针对性地推荐需求确认问题。针对CCSL规约描述系统行为的特点,改进社区发现算法,降低拆分引起的信息丢失,提高检测准确性。

参考文献

[1]

王海成. 从国家战略高度重视国产工业软件产业高质量发展[J]. 中国发展观察2021(14):13-18. DOI:10.3969/j.issn.1673-033X.2021.14.006 .

[2]

WANG H C. The high-quality development of Industrial Software: A focus of national strategic importance determination [J]. China Development Observation2021(14):13-18. DOI:10.3969/j.issn.1673-033X.2021.14.006 (Ch ).

[3]

BERTOLINO ADE ANGELIS GDI SANDRO Aet al. Is my model right? Let me ask the expert[J]. Journal of Systems and Software201184(7): 1089-1099. DOI: 10.1016/j.jss.2011.01.054 .

[4]

DALIANIS H. A method for validating a conceptual model by natural language discourse generation[DB/OL]. [2023-10-12]. DOI: 10.1007/bfb0035146 .

[5]

MEZIANE FATHANASAKIS NANANIADOU S. Generating natural language specifications from UML class diagrams[J]. Requirements Engineering200813(1): 1-18. DOI: 10.1007/s00766-007-0054-0 .

[6]

KLUZA KZNAMIROWSKI MWIŚNIEWSKI Pet al. Generating descriptions in Polish language for BPMN business process models[DB/OL]. [2023-10-12]. DOI: 10.1007/978-3-030-61534-5_32 .

[7]

LEOPOLD HMENDLING JPOLYVYANYY A. Supporting process model validation through natural language generation[J]. IEEE Transactions on Software Engineering201440(8): 818-840. DOI: 10.1109/TSE.2014.2327044 .

[8]

DIJKMAN RWILBIK A. Linguistic summarization of event logs — A practical approach[J]. Information Systems201767: 114-125. DOI: 10.1016/j.is.2017.03.009 .

[9]

FONTENLA-SECO YLAMA MBUGARÍN A. Process-to-text: A framework for the quantitative description of processes in natural language[DB/OL].[2023-11-12]. DOI: 10.1007/978-3-030-73959-1_19 .

[10]

AUTILI MBERTOLINO ADE ANGELIS Get al. A tool-supported methodology for validation and refinement of early-stage domain models[J]. IEEE Transactions on Software Engineering201642(1): 2-25. DOI: 10.1109/TSE.2015.2449319 .

[11]

GREGORY S. Finding overlapping communities in networks by label propagation[J]. New Journal of Physics201012(10): 103018. DOI: 10.1088/1367-2630/12/10/103018 .

[12]

杨元龙, 何庆林, 吴炜, . 基于MBSE的船舶动力工程总体设计方法研究[J]. 中国舰船研究202318(5): 11-21. DOI: 10.19693/j.issn.1673-3185.02799 .

[13]

YANG Y LHE Q LWU Wet al. Study on the overall design method of ship power system engineering based on MBSE[J]. Chinese Journal of Ship Research202318(5): 11-21. DOI: 10.19693/j.issn.1673-3185.02799 (Ch ).

[14]

BROMAN DDERLER PEIDSON J C. Temporal issues in cyber-physical systems[J]. Journal of the Indian Institute of Science201393(3): 389-402.

[15]

MALLET F. MARTE/CCSL for modeling cyber-physical systems[DB/OL].[2023-11-12]. DOI: 10.1007/978-3-658-09994-7_2 .

[16]

MALLET FVILLAR EHERRERA F. MARTE for CPS and CPSoS[DB/OL].[2023-11-12]. DOI: 10.1007/978-981-10-4436-6_4 .

[17]

尹玲, 陈小红, 刘静. 信息物理融合系统的时间需求一致性分析[J]. 软件学报201425(2): 400-418. DOI: 10.13328/j.cnki.jos.004540 .

[18]

YIN LCHEN X HLIU J. Consistency analysis of timing requirements for cyber-physical system[J]. Journal of Software201425(2): 400-418. DOI: 10.13328/j.cnki.jos.004540 (Ch ).

[19]

陈小红, 刘静. 基于环境的多形态时间需求建模方法[J]. 计算机学报201336(1): 88-103. DOI: 10.3724/SP.J.1016.2013.00088 .

[20]

CHEN X HLIU J. Modeling software timing requirements: An environment based approach[J]. Chinese Journal of Computers201336(1): 88-103. DOI: 10.3724/SP.J.1016.2013.00088 (Ch ).

[21]

BARIŠIĆ ARUCHKIN ISAVIĆ Det al. Multi-paradigm modeling for cyber⁃physical systems: A systematic mapping review[J]. Journal of Systems and Software2022183: 111081. DOI: 10.1016/j.jss.2021.111081 .

[22]

MOHAMED M ACHALLENGER MKARDAS G. Applications of model-driven engineering in cyber-physical systems: A systematic mapping study[J]. Journal of Computer Languages202059: 100972. DOI: 10.1016/j.cola.2020.100972 .

[23]

LEE E A. The past, present and future of cyber-physical systems: A focus on models[J]. Sensors201515(3): 4837-4869. DOI: 10.3390/s150304837 .

[24]

SVEDA MHALFAR P. Cyber-Physical information systems for enterprise engineering[DB/OL].[2023-11-12].

[25]

MALLET FDE SIMONE R. Correctness issues on MARTE/CCSL constraints[J]. Science of Computer Programming2015106: 78-92. DOI: 10.1016/j.scico.2015.03.001 .

[26]

ZHANG MDAI FMALLET F. Periodic scheduling for MARTE/CCSL: Theory and practice[J]. Science of Computer Programming2018154: 42-60. DOI: 10.1016/j.scico.2017.08.015 .

[27]

ZHANG Y RMALLET FCHEN Y X. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Frontiers of Computer Science202014(1): 105-129. DOI: 10.1007/s11704-018-7054-8 .

[28]

WANG J YHUANG Z QHUANG X Wet al. Multiclock constraint system modelling and verification for ensuring cooperative autonomous driving safety[J]. Journal of Advanced Transportation20202020: 8830752. DOI: 10.1155/2020/8830752 .

[29]

YIN LMALLET FLIU J. Verification of MARTE/CCSL time requirements in promela/SPIN[C]//2011 16th IEEE International Conference on Engineering of Complex Computer Systems. New York: IEEE Press, 2011: 65-74. DOI: 10.1109/ICECCS.2011.14 .

[30]

CHEN X HYIN LYU Y Jet al. Transforming timing requirements into CCSL constraints to verify cyber-physical systems[C]//International Conference on Formal Engineering Methods. Cham: Springer, 2017: 54-70. DOI: 10.1007/978-3-319-68690-5_4 .

[31]

HU MXIA JZHANG Met al. Automated synthesis of safe timing behaviors for requirements models using CCSL[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems202342(12): 5127-5140. DOI: 10.1109/TCAD.2023.3285412 .

[32]

IQBAL M Z, ALI S, YUE Tet al. Experiences of applying UML/MARTE on three industrial projects[DB/OL]. [2023-11-12]. DOI: 10.1007/s10270-014-0405-5 .

[33]

SHARMA RBISWAS K K. Using norm analysis patterns for automated requirements validation[C]//2012 Second IEEE International Workshop on Requirements Patterns (RePa). New York: IEEE Press, 2012: 23-28. DOI: 10.1109/RePa.2012.6359965 .

[34]

DALPIAZ FFERRARI AFRANCH Xet al. Natural language processing for requirements engineering: The best is yet to come[J]. IEEE Software201835(5): 115-119. DOI: 10.1109/MS.2018.3571242 .

[35]

FISCHBACH JHAUPTMANN BKONWITSCHNY Let al. Towards causality extraction from requirements[C]//2020 IEEE 28th International Requirements Engineering Conference (RE). New York: IEEE Press, 2020: 388-393. DOI: 10.1109/RE48521.2020.00053 .

[36]

GARCES KDEANTONI JMALLET F. Transforming CCSL partially-ordered traces into UML interaction diagrams[DB/OL].[2023-12-04]. DOI: 10.1109/seaa.2011.47 .

[37]

尹玲. 基于时钟约束和信号约束的信息物理融合系统的建模、分析与验证[D]. 上海: 华东师范大学, 2016.

[38]

YIN L. Modeling, Analysis and Verification for Cyber-Physical Systems Based on Clock and Signal Constraints[D].Shanghai: East China Normal University, 2016 (Ch).

[39]

KULKARNI D R NSRINIVASA C K. Novel approach to transform UML sequence diagram to activity diagram[J]. Journal of University of Shanghai for Science and Technology202123(7): 1247-1255. DOI: 10.51201/jusst/21/07300 .

基金资助

国家自然科学基金青年基金(61802251)

国家自然科学基金青年基金(61603242)

国家自然科学基金青年基金(62302308)

AI Summary AI Mindmap
PDF (3513KB)

0

访问

0

被引

详细

导航
相关文章

AI思维导图

/