信息物理系统中组件的时间行为可组合研究综述

陈 博，刘 翀，3，陈 辉，陈香兰，3 ，李 曦，3

1(中国科学技术大学 软件学院，江苏 苏州 215123)

2(华为信息技术有限公司，深圳 518000)

3(中国科学技术大学 计算机科学与技术学院，合肥 230027)

1 引 言

为了更精确地认识与改造世界，新一代的嵌入式系统必须将计算世界与物理世界作为一个紧密交互的整体来进行认识，实现一个集计算、通信与控制于一体的深度融合的理论体系与技术框架，即信息物理系统(Cyber Physical Systems，CPS).与传统嵌入式系统(Embedded System，ES)不同，CPS充分考虑计算部件与物理环境的深度融合，通过将设备智能化连接，实现物理环境与计算系统之间的精确感知与高效协同.CPS通常被应用在安全关键的场景中，需要对环境进行实时监测，计算反馈信息，最终实现自动化的控制与管理，是一种具有异构性、实时性的复杂系统.CPS与传统ES的工作方式相近，但传统ES通常由简单的计算过程和物理环境两部分组成，如灯光控制系统、水温控制系统等，其计算部分通常执行顺序的、简单的周期性任务，并将处理结果反馈至外部的单一环境.而CPS中的计算过程通常由复杂的调度机制进行多任务的调度执行，实现对复杂外部环境的控制与管理[1].如典型的汽车电子控制系统由多个电子控制单元(Electronic Control Unit，ECU)及处理ECU之间通信的总线组成，其上实现了多种子系统，如牵引力控制系统，车身稳定控制系统等.对类似系统进行设计与实现是一个复杂的系统工程，而其中，如何在设计过程中保证CPS的实时性与正确性是关键的核心问题.

近些年，研究人员在CPS的开发方法上取得了丰硕的研究成果，但尚缺乏对这些成果进行梳理、总结的综述.基于此，本文将以CPS中最为关键的组件时间行为可组合问题为核心内容，回顾组件化软件开发的发展历程，对组件行为抽象、组合操作的发展脉络进行梳理，并介绍近年为提升组件时间行为的可预测性、可组合性所提出的3种实时编程模型.最后，指出未来的若干研究方向.

2 组件化软件开发方法

为了保证CPS中功能与非功能属性的正确性，通常采用基于组件化(Component-Based Development，CBD)的开发方法对系统进行建模、分析及功能的验证[2].图1给出了基于软件工程中V模型的组件化软件的开发流程，与传统软件开发流程相同的是，开发过程都从需求分析到最终的代码生成.而不同的是，组件化软件的开发过程以模型为中心，首先建立需求模型，继而逐步定义子系统模型，并通过不断精化的方法对系统进行开发，最终通过组合各子系统模型的方式对整体行为进行描述，并通过确认与验证(Validation & Verification，V&V)的方式对系统的功能属性/非功能属性进行验证，最终生成具体的执行代码.因此，通过基于组件的开发方法对具有安全关键的CPS进行实现将涉及到组件的时间行为抽象、时间行为精化，以及时间行为的组合与验证等具体技术细节.本章将首先介绍组件化软件的基本概念，然后引出组件组合的几种方法.

图1 基于V模型的组件化软件开发流程

2.1 组件化软件开发

组件是对功能单元的一种封装，可以看作“黑盒功能抽象”，其通过接口向外部环境提供服务，也可称为“软件组件(software component)”，表达了组件隐藏内部功能，同时向外提供服务的软件形式.

在计算机的若干概念定义中，典型的定义形式如遵循Wengerzai在1987年给出的描述[3]：“当事物满足了某些属性，则它就是某种类型的特定事物(something is an A if it has properties a1，a2，and a3)”.例如，当某语言支持对象、类及继承三种属性时，则该语言就是面向对象语言.因此，本文借鉴文献[4]给出组件化软件的普适定义1.

定义1.当软件架构满足如下属性，则可以将该软件定义为组件化软件：

·是一个可以独立进行开发的软件单元；

·支持与第三方软件单元进行组合；

·外部环境无法直接读取组件内部的状态信息；

上述定义首先描述了组件应该是一个独立开发的个体，与外部环境和其它组件具有明确的功能界限划分.其次，组件进行了功能隐藏，封装了自身的行为特征，并通过接口向外提供服务.接口表明了组件向外部环境所提供服务的保证(Guarantee，如服务的时间、服务的类型等)，以及组件对外部环境所产生行为的期望(Assumption)，同时可以与其它组件通过组合操作来实现系统的整体功能.最后，组件是一个自给自足的个体，其它组件(或外部环境)只能通过接口向其请求服务，并得到计算结果.外部环境也不能显式的获取组件的状态信息.

其次，针对组件的定义，Szyperski给出的描述为[4]：“组件的本质是用于组合的”，表达了对组件最本质的概念阐述.同样，Meijler给出组件的两个主要设计思想[5]：重用性与可组合性，两者息息相关.其中，重用性描述了组件在多个场景下的可重用能力，也可以理解为抽象化的程度，表达了当组件的功能定义过于宽泛，即其功能定义过于抽象，则在一些场景下将导致组件重用灵活性的缺失，而当组件的功能定义过于具体，则易增加组件组合操作的复杂性.

在编程语言的实现层面，如JavaBeans/CORBA/COM /.Net等编程语言都通过组件对功能进行封装，并给出了静态、动态属性的组合规则.NeXTStep语言[6]定义了复杂的组件组合操作，将多个对象封装在某nib文件中，同样体现了组件的组合过程.再如TinyOS操作系统[7]下的应用开发，该操作系统定义了clock/LED/Timer等多种资源组件，并由调度组件(scheduler component)协调执行上层的任务组件，其开发过程也将组件的组合过程看作是对系统的配置.

综合而言，组件是一种提供功能封装，支持组件组合操作与精化的软件设计思想.接下来，本文将给出组件行为抽象的一般方法，并给出组件组合的操作方法.

2.2 组件的组合操作

组件的组合操作是组件之间行为组合的计算过程.为方便叙述，本文通过标签迁移系统(Label Transition System，LTS)建模组件的个体行为，再将多个模型进行组合，形成系统的整体模型.借鉴文献[8]的描述，分别给出了3种典型的组件组合语义，首先给出迁移系统的定义.

定义2.迁移系统TS是一个六元组，其中，S是状态集合，S0∈S是非空的初始状态，I是输入事件序列，AP是状态标签，L：S→φ(AP)是标签函数，将一组状态与一组标签进行关联，→∈S×I×S是系统中从一个动作的输入到下一个状态的迁移关系.

定义4.将迁移系统的可达性描述为：如果在迁移系统TS中，对于输入符号序列δ=i1i2i3…，存在一个有限的执行序列rδ=s0i0s1i1s2…iks′，则可以定义状态s′是可达的.

两个迁移系统的组合为TS1‖TS2，其状态集合为笛卡尔积S1×S2.首先给出两个TS：

TS1=〈S1，S0，1，I1，→1，AP1，L1〉TS2=〈S2，S0，2，I2，→2，AP2，L2〉

具体的组合方法与迁移系统的迁移条件→1·2相关.依据不同语义，具体分为如下3种组合方式：

·同步组合(synchronous composition)：同步组合要求迁移系统仅当TS1和TS2在有一致的输入符号时才进行迁移.在该语义下，如图2所示，将TS1与TS2的同步组合表示为TS1∩TS2=TS1∩2，计算过程为：

图2 组件的组合语义

TS1∩2=

其中：

·S1∩2=S1×S2；S0，1∩2=S0，1×S0，2；

·I1∩2=I1∪I2；AP1∩2=AP1∪AP2；

·L1∩2()=L1(S1)∪L2(S2)；

·<，i，>∈→1∩2；

并且满足如下条件：

∈→1，∈→2；

·并发组合(parallel composition)：并发组合规则要求迁移系统仅当TS1和TS2在有一致的迁移动作时进行迁移.如图2中TSsr‖TSpsp，在该组合语义下，TS1与TS2的同步组合表示为：TS1‖TS2=TS1‖2，计算过程为：

TS1‖2=，其中：

·S1‖2=S1×S2；S0，1‖2=S0，1×S0，2；

·I1‖2=I1∪I2；AP1‖2=AP1∪AP2；

·L1‖2()=L1(S1)∪L2(S2)；

·<，i，>∈→1‖2；

并且满足如下条件：

1)i∈I1∩I2，∈→1，∈→2(TS1与TS2均进行迁移，输入符号被双方接收)；

2)i∈I1I2，∈→1，s2=s2′(只有TS1进行迁移，输入符号只有TS1接收)；

3)i∈I2I1，∈→2，s1=s1′(只有TS2进行迁移，输入符号只有TS2接收).

·信道组合(channel composition)：具有通信语义的迁移系统表示为，其中C是一组进行数据传输的通信信道.系统在信道组合语义下，不仅在TS1和TS2有相同输入/输出的情况下进行状态迁移，同时也在有消息发送(c!)和接收(c?)的过程时进行迁移.则有：→∈S×(I∪C!∪C?)×S，其中，c!属于集合{c!| c∈C}，以及c?属于集合{c?|c∈C}，信道组合如图2中组件a┥┝b┥┝c的组合过程.针对具有通信语义的迁移系统可以描述为：

TS1=〈S1，S0，1，I1，C，→1，AP1，L1〉TS2=〈S2，S0，2，I2，C，→2，AP2，L2〉

其组合模型为TS1┥┝TS2为：

TS1┥┝2=

其中：

·S1┥┝2=S1×S2；S0，1┥┝2=S0，1×S0，2；

·I1┥┝2=I1∪I2；AP1┥┝2=AP1∪AP2；

·L1┥┝2()=L1(S1)∪L2(S2)；

·<，i，>∈→1┥┝2；

同时需要满足如下条件：

1)i∈I1，→1(S2=S2′)；

2)i∈I2，→2(S1=S1′)；

3)∈→1，∈→2′，其中i=ε，

或：

4)∈→1，∈→2′，其中i=ε

本文罗列了上述3种典型的组件组合操作方法，通过3种不同语义对组件的行为进行组合.这也是基于组件化软件开发的基础.

2.3 组件的可组合性

对组件行为进行抽象并给出抽象后组件的组合方法，可以对系统的整体行为进行描述.在此基础上，需要给出判定规则描述何种条件下组件是可组合的.当前，相关研究小组相继提出一些形式化方法用于建模系统的交互行为，并验证组件的可组合性.典型的，Lynch提出I/O自动机模型[9]，通过建模组件的接口行为来分析交互过程.接口自动机是另一种显示表达组件接口时序行为的形式化模型[10]，对外部环境行为进行定义，在一定程度上可以被看做接口模型，而IO自动机类比看作是组件模型.继而，Alur与Lynch等将时间语义加入到自动机模型中，提出了时间自动机[11]、时间I/O自动机等模型.

·一组状态集合，也可以表示为StS；

·一组签名(动作)sig(A)，也可以表示为ΣS；

·step(A)⊆states(A)×acts(sig(A))×states(A)，描述对于给定的某个状态a，对于输入事件π，系统将产生迁移(a，π，a′) ，也可以表示为→S.

对于具有可兼容性的自动机Ai：i∈I，其构成组合后的自动机A=∏i∈IAi为：

states(A)=∏i∈Istates(Ai)；start(A)=∏i∈Istart(Ai)；

sig(A)=∏i∈Isig(Ai)；part(A)=∪i∈Ipart(Ai)；

I/O自动机的可组合性描述为：在组件具有兼容性的前提下，组合后形成的整体模型中，组件的原有属性保持不变.在组合时，可通过组件的笛卡尔积(product)进行计算.

·VP是一组状态集合；

·τP⊆VP×AP×VP是一组迁移过程.

定义9.接口自动机P和Q是可兼容的，当条件成立：

定义10.接口自动机P和Q的笛卡尔积(product)为P⊗Q：

·VP⊗Q=VP×VQ

接口自动机的组件P和Q在可兼容的前提下，当如下条件满足时，则组件是可组合的：对于P⊗Q，存在一个合法的环境E使得illegal(P，Q)×VE在(P⊗Q)⊗E系统中，非法状态illegal(P，Q)不可达的.

3 组件的时间行为建模与验证

前面给出了基于迁移系统的组件组合操作方法用于建模系统的整体行为.在此基础上，需要给出组件行为可组合性的形式化定义，以此指导对组件可组合性的验证.本节将对组件行为可组合的形式化定义进行阐述与归纳.

3.1 时间行为的可组合

可组合性是组件化软件重要的性质之一，描述了组件之间行为的兼容能力.传统的CBD方法更多关注组件接口值域的可组合性，描述了两个组件在组合时，需要满足两个组件接口的值域要求.如图3的例子中，组件P1的输入值x和y，同时对其输入进行约束，要求当x=0时，y值也需要等于0，以此产生z值.而在x不等于0时，则对y值无限制.本文给出两个组件的组合行为P1||P2，为了满足整体的输入条件，组合后给出的约束条件为x≠0，以此保证z值的正确输出.组合过程也可以看作是对值约束行为的一种精化.

图3 约束行为的组合

针对组件的可组合性，Baldovin在其博士论文中从两个角度给出了较为普适的定义[17].其一描述了组件的个体功能在组合后的保持性，定义为组件的组合性(compositionality)，是一种基于自底向上(bottom-up)的视角对组件化软件的解决方案.其二描述了组件在组合后的整体行为是否能够满足系统的功能要求，描述为组件的可组合性(composability)，可以看作是一种自顶向下(top-down)的解决方案.该定义给出了组件化软件可组合的通用性描述，具有普适性.但针对CPS中组件的可组合性，考量的不仅仅是功能属性，更重要的是系统的非功能属性(时间行为，功耗等).需要在非功能属性上给出更为细粒度的定义，描述特定属性的可组合性.Edward Lee在文献中提出可组合性具有层次化、异构性的特征[18]，其关注于信息物理系统中多种计算模型(Model of Computation，MOC)的组合，如数据流模型/进程代数模型/同步反应模型等模型组合.其研究小组设计并实现了仿真建模工具Ptolemy，针对每种模型给出其行为类型系统用以验证各模型之间的可组合性.Kopetz在文献中定义组件的可组合性是其行为的可保持性[19]，即，在组件组合前后，组件的个体功能保持不变.基于该定义，Kopetz给出了系统中架构可组合的形式化描述：“子系统(sub-system)所具有的属性，在系统组合之后，该属性仍然得到保持，则系统的架构是可组合的”.本文在表1中罗列了几个典型的组件时间行为可组合的定义.

表1 典型的组件可组合形式化定义

另一个重要的研究工作是宾夕法尼亚大学Insup Lee小组的相关工作[20-22].主要关注实时嵌入式系统的层次化可调度、可组合的问题.在该工作中描述组件具有层次化的特性，系统可以看作分区(partitioned)的架构.因此，该模型下的可组合问题演变为：首先建立个体组件的时间行为模型，然后通过全局调度器对组件之间的时间需求进行可组合(可满足)验证.基于此，通过增量式(incremental)的开发方法进行具体实现.清华大学的王博对嵌入式可组合软件进行了阐述[23]，描述可组合具有广义和狭义的概念，并分析嵌入式可组合软件应具备的特征.其次，为了从执行语义上对时间行为的可组合性进行分析，Henzinger等人基于逻辑执行时间编程模型(Logical Execution Time，LET)[24]定义了Giotto编程语言，并给出了针对分布式系统的、具有时间行为可组合性的编程方法.在开发过程中，将分布式节点看做资源提供者(Supplier)，并通过功能的集成(Integrator)对系统进行设计实现.其针对分布式环境下时间行为的可组合性，给出两方面描述：1)接口兼容性(interface compatible)：描述了在分布式环境下，分配至某节点的功能模块Ps，h可以在其提供者S的时间接口Ts，h内执行完成；2)时间安全性(time-safety)：满足如下条件时，功能模块Ps，h是安全的：①读取某任务输出端口的时间点(或总线消息)不早于任务计算的时间(或传输)；②写入任务端口的时间点(或传输)不晚于任务开始执行的时间.

近些年，工业界同样受惠于模型驱动开发的方法优势.典型的如针对汽车电子系统进行建模开发的EAST-ADL方法，其基于Autosar架构建立整车的需求模型[25]，并逐步分解为子系统需求，并通过sysML语言对各子系统进行模型的设计与实现.再如早期针对航空领域进行模型定义的AADL建模语言[26]，其从建模工具到分析工具都逐渐变得成熟，若干工作已经将其应用于无线通信或机器人等领域.在AADL中定义组件/包/子系统等系统元素，并通过连接器等方式对系统进行组合行为的配置.Bardaro等人[27]给出了基于AADL对ROS机器人进行实现的开发方法.Li等人[28]给出AADL转换为时间自动机的方法，并给出规则用于验证模型的可组合性.

3.2 组件模型

当前，已有相关研究提出多种组件模型来对系统行为进行建模及分析.本小节分别概述几种典型的系统模型，包括，基本组件模型、组件之间的交互行为BIP模型、接口事件模型及框架模型等.

3.2.1 基本组件模型

Kopetz给出分布式实时系统中组件的概念性描述[29]，根据不同场景，将组件分为闭合组件(close component)与开放组件(open component).通过接口与外部进行通信，具体定义了4种接口：服务提供、服务请求、配置计划以及诊断与管理接口.同时定义任务、状态、报文、节点以及簇等基本系统元素，并通过Linking Interface[30]描述其可组合性.Joseph Sifakis研究小组的相关工作[31-33]定义了系统的抽象模型BIP(Behavior Interaction Priority，BIP)，具体为：行为模型(Behavioral Model)：组件个体的行为，不因环境的上下文而改变，提供给环境的保证(guarantee)及对环境的期望(assumption).交互模型(Interaction Model)：组件之间的通信行为，具体描述了系统在架构上的约束，通常可由一组连接器(Connector)及相关属性进行建模；优先级(Priority)：用于建模交互行为中的优先关系.该模型较好的从顶层给出系统行为语义，抽象了系统的结构与行为.在该描述下，组件的基本概念定义为：

定义11.原子组件(Atomic Component)包含如下元素[32]：

·一组端口p={p1，p2，…，pn}，端口的名字描述与其它组件的同步事件行为；

·S={s1，s2，…，sn}是组件的状态集合；

·本地的数据变量V；

·执行原子操作的迁移过程(s1，p，gp，fp，s2).

图4是一个原子组件结构，包括两个端口in和out，变量x，y，和状态empty以及full.在状态empty中，接收到同步事件empty后，当守卫条件0

图4 原子组件的结构

3.2.2 接口事件模型

为了建模组件接口的多种行为，Thiele等人[34]给出一种抽象-自适应接口(adaptive interface)模型用于描述组件的接口行为，同时，给出了支持组件独立设计、增量式开发的组合规则.文中将接口行为划分为4种类型(周期、偶发、抖动及突发的)：

假设组件A与B存在交互(A⟺B)，组件A输出周期为T1(抖动为J1)的周期性事件，组件B的输入事件为最小到达间隔时间为T2的偶发性事件，两个组件的输出输入行为在时间语义上不一致.如图5所示，文献中通过“构造”事件的相关行为来对接口事件的可组合性进行建模及分析.如上述示例中，通过T2=T1-J1构造两者之间关系.

图5 接口事件之间的转换关系

Richter等人[35]也给出接口模型用于描述组件的接口行为.具体将组件抽象为(X，Y，T，ψ)，其中X为输入行为，Y为输出行为，T是计算函数，Y=T(X)，ψ(X)是对输入行为的约束.则两个接口G与H进行组合时，当满足如下条件时，接口是可组合的：

上述关系描述了当两个组件在组合时，接口的保证(Guarantee)可以满足另一组件接口的假设(Assumption)，则接口是可组合的，该文工作从接口事件行为的角度进行建模，给出接口可组合的通用规则.

3.2.3 系统框架模型

最为典型的系统模型如liu在文献中给出的实时系统模型[36]，系统由任务模型task，资源模型resource，以及调度模型scheduler组成.具体将系统建模为：通过调度器的调度方法在资源上对任务进行执行.基于此基础，文献[37]给出了一个分布式实时系统下的系统模型，具体包括如下元素：任务task，调度策略scheduler，计时定时器timer及用于任务间通信的信道channel，给出了组件可组合的规则定义，并通过UPPAAL工具[38]进行建模及验证.文中定义：当所有实时任务是可调度的，则组件是可组合的.基于时间计算树逻辑(Timed Computation Tree Logical，TCTL)给出了可组合性的验证查询语句：

E<> Task.executing

3.3 时间行为确定的编程模型

编程模型描述了程序执行的行为抽象.在传统的基于进程/线程理论的编程模型中，进程作为系统调度的执行单元，通过协调线程流完成任务的执行.进程/线程模型从多任务的角度描述任务的并发行为，可以高效的对多任务系统进行调度.但固有的优先级抢占等机制，使得正在执行的任务易被抢占导致执行时间变得不确定(输入、输出行为的抖动).因此，在进程/线程的编程范式下，CPS中组件的任务执行行为变得不确定，对组件的时间行为可组合判定变得困难.

为了使任务的时间行为变的确定，相关研究提出了不同的编程范式以提高系统响应时间的可预测性[39].典型的编程模型有物理执行时间模型(Physical Execution Time，PET)、有界执行时间模型(Bounded Execution Time，BET)、零执行时间模型(Zero Execution Time，ZET)以及逻辑执行时间模型(Logical Execution Time，LET)等，从不同执行行为角度对时间属性进行限定.

3.3.1 物理执行时间模型

PET模型被应用于早期简单的控制系统中，如单或多处理器架构的控制系统.类似系统的计算时间通常为常量并有准确的I/O处理时延，由较低级的编程语言进行实现，该类系统不具备并发性即多组件的协作能力.如图6所示，任务在时间段[0，1]之间完成数据输入，在之后的8个时间段完成任务的计算，并在时间段[9，10]完成任务结果的输出.

图 6 编程模型的逻辑语义及任务的真实调度执行情况

PET模型适用于任务的执行时间可确定的计算平台，比如周期性任务执行，其计算时间可确定，因此输入输出时间容易计算，并能够获得较高的吞吐量.但较为明显的缺点是缺少可组合性，即当系统复杂性逐步增加时，如何集成化的开发整体系统变得困难，甚至在早期多个PET组件之间通信过程的传输时间、延迟时间等都较难计算.

3.3.2 有界执行时间模型

随着底层硬件架构处理能力的增强，针对实时嵌入式系统的多任务应用随之增多.同时，需要准确的度量多任务环境下任务的执行时间以保证任务计算结果可以在截止时间之前完成输出.有界执行时间BET模型从多任务的场景出发，定义有界执行时间为其任务的执行周期，因此在实现中，能够保证任务的“输入-计算-输出”能够在有界执行时间BET之内完成，即能够保证多任务系统的正确性及实时性.如图6中任务的执行片段，任务的周期为10个时间单元，在时间段[0，1]过程中，由于有高优先级任务在运行，则任务等待至[1，2]期间进行任务的输入，之后在[3，4]时间段执行任务的计算，在[5，7]被其他任务抢占，并继而在[6，8]期间完成任务的计算并输出，同样，在时间段[10，20]期间进行了另一个周期的任务执行.

有界执行时间模型可以保证任务执行的实时性，典型的如基于传统的RM/EDF调度方法，并利用WCET分析工具进行多任务的可调度性分析，以判定是否满足时限要求.但从执行过程来看，该模型仍然缺乏可组合性.

3.3.3 逻辑零执行时间模型

为了增强组件的可组合性，相关研究试图关注组件的输入与输出行为，为了加强并保证组件是输入确定的(input-determined)，即：对于给定的任务输入序列，可以确保有相同的计算结果的输出(结果与时间)，某种程度上也将该类系统称为“同步反应式系统(Synchronous Reactive Systems)”.模型基于“同步假设(Synchronous Assumption)”，其中同步描述任务的输入与输出是同步的，任务的输入-计算-输出时间在模型角度可看作零时间.

该模型下，可以有效的保证系统的输入输出的实时性，在一定程度上对系统的可组合性进行了基础性的保证.但该模型从“同步假设”的角度出发，在实际操作中，任务的输入/计算/输出时间不能保证在零时刻内完成，因此，需要通过语言结构、编译器支持进行同步假设的实现.在简单的任务环境下，可以正确的实现模型的语义，但在复杂的环境下的一些技术问题，如分布式环境下的通信行为、节点时钟同步等，都给ZET模型的应用带来难度.

3.3.4 逻辑执行时间模型

实时控制系统与物理系统相交互，其I/O行为尤为重要.同样，出于考量系统I/O行为的时间属性的目的，学术界提出逻辑执行时间模型LET对任务的时间属性进行抽象.其中任务的输入与输出是在特定的时间点进行完成.如图6示例中，任务在[1，2][11，12]时间段进行数据的输入，在[2，8][12，18]间进行任务的执行，并在[8，9][18，19]时间段进行任务的输出.与其它编程模型最大的区别在于，LET编程模型中任务的输入输出是有时间要求的、是确定的.即使任务过早的计算完成也并未执行数据的输出，而是等待输出时间点到达后再进行输出.LET模型通过时间的确定，强化了输入输出行为的可组合性.

3.4 组件的精化

如前所述，一些增加时间语义的典型形式化方法(如时间自动机、时间Petri网、Event-B等[40])均已被应用于CPS的建模与精化.本节将对精化部分进行阐述.

组件化开发方法中的精化(Refinement)过程描述了系统的需求规约(specification)与系统实现(implementation)之间的转换过程.在对两个模型之间是否存在精化关系进行判定时，典型的如使用替代模拟(alternating simulation)的方法[41]进行检查.该方法中，在对输入有条件限制的情况下，如果最终实现模型允许输入的集合是规约需求中所定义集合的子集，则实现模型将被用于较小的环境或范围中.可描述为，组件P精化了组件Q，则Q的输入可以被P所模拟，而对于P的输出可以被Q所模拟，保证了精化后的组件可以在更多的外部环境中使用.

定义12.替代模拟(alternating simulation)[41]：对于系统的需求规约S=(StS，S0，Σ，→S)精化了规约T=(StT，T0，Σ，→T)，可以表示为S≼T，且存在二项关系R⊆StS×StT，并有(s0，t0)，并且存在状态集合(s，t)∈R，并且满足如下的条件：

定义13.精化关系[41]：当规约P和Q之间存在关系P≼Q时，表明两者具有精化关系.

为了说明精化过程的具体实现，如图7示例，machine-2在两个方面对machine-1进行精化实现.其一，machine-1中从状态s2迁移至s1的条件为tea!，在machine-2的具体实现中，舍弃了对tea!事件的处理，即，精化后的实现模型具有更少的行为输出；其二，在状态S2上进行了不变量的紧致操作，将y≤6变为y≤5.通过可达性分析得出，在输入动作上，machine-2可以模拟machine-1，而在输出动作上则具有相反的特征.

图7 糖果机示例的一种精化关系实现

另一种精化检查的方法是通过前向或后向模拟[42]来建立具体模型和抽象模型之间的关系.如果能够推导出精化后具体模型中状态与抽象模型中状态存在一定的二元关系，事件也存在一定的二元关系，则可以称两者之间是存在精化关系的.形式化描述为如下：

r∈T↔S

其中，r是二元关系，具体模型中状态及事件集合为T，抽象模型中状态及事件的集合为S.

模型检查中典型的难点是状态爆炸问题，在对精化关系进行检查时，更多采用组合精化的方法以避免状态爆炸问题.其含义为，为了检查组件的组合行为Q1‖Q2‖…‖Qn精化P1‖P2‖…‖Pn，只需要分别验证Q1精化了P1，Q2，精化了P2…Qn精化了Pn即可.也就是将组合后的精化检验分解成多个独立的精化检验过程，减少空间的搜索.如下为基本模式：

4 面临的挑战与研究展望

组件的时间行为可组合问题已经得到了广泛的关注并取得了一系列研究成果，但仍然存在一些具有挑战性的问题亟待进一步解决.从组件化软件开发的角度来看，首先需要建立顶层的时间行为需求模型，并将需求模型逐步转化为底层的具体实现.因此，如何建立上层的时间需求模型，上层的需求模型(如端到端的时间约束)如何逐步分解、转化为实现层的任务级时间约束(任务的周期、截止时间等)，并在分解为各组件之后，如何分析、验证多个组件(子系统)之间的时间行为是可组合的，仍然是CPS开发过程中的核心问题.具体的，相关的挑战如下：

1)组件时间行为可组合的形式化定义

组件可组合性相关研究的基础在于对可组合性的形式化定义，从而可以明确需要具备可组合性的属性、含义以及度量方法等.只有在此基础上，才能有针对性的提高组件的可组合性.在现有的组件可组合的形式化定义中，最为基本的定义是从组件的行为角度出发，描述组件在组合之后，如果各组件原有的行为不受影响，则组件是可组合的.该广义的定义指导了最初的组件化软件的设计及组合操作的实现.但针对于具有安全攸关的CPS(无人驾驶、智能制造等)，其行为变得复杂，类似系统中组件行为的可组合需要保证任务调度、执行时间、执行顺序等行为在组合前后的一致性.因此，与传统的组件化软件的可组合定义相比，如何更为进一步明确的给出组件在时间行为可组合的形式化定义，是亟待解决的核心关键点.

2)组件的时间行为可组合验证

在组件化开发框架中，需要通过形式化的方法和工具对组件的可组合性进行验证(verification).在现有的工作中，典型的形式化分析工具，如时间自动机、Petri网、B语言、Z语言等已被广泛应用.同时也有相应工具的扩展，如时间接口自动机、时间petri网等，都从不同的角度对系统行为进行建模.然而在已有的工作中，相应的形式化方法仍然不够完备.典型的如自动机理论中的状态爆炸问题，虽然可以通过层次化的思想对问题进行解决，但在具体的工业应用领域场景下，仍然存在语义转换的复杂性、一致性等问题.因此，如何选择适合的形式化工具(自动机/Petri网/B语言等)对组件内部的时间行为进行建模，继而对系统整体的时间行为进行验证.也是系统中时间行为可组合问题的主要挑战.

3)运行时系统在组件时间可组合性上的支持

组件的可组合性是一个关键的、核心的软件工程理论问题.其中，可组合性问题也涉及到计算机软硬件架构多方面的技术定义与实现.比如改造或重构现有底层架构使其增加时间语义，优化现有实时调度方法(RM/EDF等)，甚至在编程语言中增加时间属性等调整，类似对系统架构进行的优化，均影响到组件执行的时间属性，甚至提升组件时间行为的可组合性.现今，相关工作给出若干方案，但仍然缺少完整的、具有时间语义的软硬件架构的支撑.

应对上述挑战，信息物理系统下组件化软件的可组合性问题研究可以从以下几个方面进行展开：

1)系统中时间行为可组合定义

已有的组件时间可组合的形式化定义均从组件组合行为的本质出发，描述当组件之间的时间行为彼此不干扰时，则组件是时间可组合的.然而对于安全攸关的信息物理系统而言，任务的执行时间和任务执行的顺序关系均影响着系统的正确性.因此，对系统中组件的时间和顺序行为进行建模及分析，能够准确刻画系统的时间行为，保证系统的正确性.比如在MARTE/CCSL建模语言中[43-45]，通过逻辑时钟建模了系统的时序行为，并验证多个层次上的时序行为的可组合性.但从该角度出发，如何从需求模型逐步精化到实现模型，仍然需要大量工作的开展.

2)具有精化与组合语义的形式化验证

在模型驱动开发过程中，首先建立需求规约模型(specification)，并据此需求模型对系统进行逐步精化.在精化过程中，可以对复杂系统进行分解(decomposition)[46].并在后续开发过程中，再将分解后的子系统进行组合，并验证多个子系统组合后的行为是否与最初的规约一致.现有的形式化方法中，自动机、Petri理论均被广泛应用于上述过程的建模，但相应方法也有各自缺陷，如状态爆炸[47]、多次转换导致转换效率下降等问题.同样，类似B语言/Event-B语言等具有事件精化及组合本质的形式化方法可以有效对系统行为进行建模，建模语言本质上的精化特质更适合将上层的需求模型逐步转化为系统实现模型.

3)支持任务时序行为可组合的运行时系统

运行时系统应该能够支持设计时的时序语义.同样，实现具有时间可组合的信息物理系统涉及到计算机整体架构的各个层面(包括如，需求建模层—语言层—操作系统层—体系结构层)，需要保证从设计时到运行时的各个层次中时序行为的一致性.较为典型的工作，如文献[48]重构了操作系统内核，将系统进行了层次化(应用/内核/硬件平台)划分，并提出层次之间应彼此不干扰(Zero-disturbance)，以及操作系统应该具有稳定的时间行为(Steady timing behaviour)两个设计准则，并据此准则实现了具有时间可组合的操作系统原型TiCOS(Time Composability OS).为了缓解现有调度方法导致组件时间行为的异常、以及面对减小输入/输出行为的抖动的需求，项目组在前期面对相关挑战进行了若干尝试，基于LET模型，提出了具有时间可预测的操作系统原型[49]及验证方法[50]，并基于FPGA实现了支持时间语义的硬件操作系统[51]，相关实验数据表明了方案有效降低任务输入/输出时间的抖动，实时性能优于传统的体系结构，也有效提升了系统中组件时间行为的可组合性.

5 结 论

组件的可组合性是组件化软件的核心理论.尤其在针对复杂的信息物理系统的设计过程中，系统非功能属性(时间、执行顺序[52]、功耗等)的可组合性显得尤为重要.本文总结时间行为可组合的若干工作，重点阐述了可组合的形式化定义，以及为了提高组件时间行为可组合性所提出的几种主流编程模型.在后续的工作中，将基于已有的理论基础，继续在可预测、可组合系统的设计及验证等方面进行探索与尝试，如编译器中时间属性的支持，以及提出更有价值的系统可组合框架等.