安全关键的信息物理系统中时序行为的组合与精化

陈 博 李 曦,2 周学海,2

1 （中国科学技术大学软件学院 江苏苏州 215123）

2 （中国科学技术大学计算机科学与技术学院 合肥 230051）（chenbo2008@ustc.edu.cn）

信息物理系统（cyber physical systems, CPS）通常是由多个组件（物理组件、计算组件等）组成的复杂信息系统[1].其发展迅速，尤其在近年计算机系统中软硬件架构处理能力不断强化的加持下，使得CPS迭代速度不断加快.比如某款汽车系统中包含由200个供应商中提供的70多个 ECU 单元，且数量不断增加，同时预计内部软件系统代码量也将从2005年的几百行增长至2025年的100亿行，面对如此复杂庞大的系统，如何保证系统的正确性、安全性是类似CPS开发过程所面临的主要问题.现今，基于构件的开发（component-based development, CBD）方法成为该类系统主要的开发方式[2].其具体过程如图1所描述，首先给出顶层规约（specification），再通过精化方法细化规约，最终得到具体实现（implementation）.因此，构建系统关键属性的行为模型，再利用精化与组合方法生成具体模型，最终对关键属性进行验证是CBD方法的核心内容.

Fig.1 Component software development method based on V model图1 基于 V 模型的组件化软件开发方法

为了对安全攸关的CPS进行设计开发，本文基于时序约束描述语言（clock constraint specification language,CCSL）对系统进行实现.具体地，本文主要贡献体现在3个方面：

1）给出时序行为可组合的形式化定义.为了阐述时序行为的组合过程，通过迁移系统（transition system,TS）描述时序约束语义，并在此基础上给出时序行为可组合的形式化定义.

2）给出基于L*学习的系统属性验证方法.通过分治策略对系统属性进行验证，有效解决模型组合后所带来的状态激增的问题.

3）提出针对时序约束行为的逐步求精方法.主要针对3种典型的时序约束规约进行精化实现，给出任务结构的生成规则，能够将顶层的时序规约模型映射为操作系统中任务级的时序行为约束模型.

1 相关工作

目前，在时序规约建模与精化等方面已有若干相关工作的开展[3-4]，本节将对其进行归纳和比较.

1.1 时间行为的组合与验证

时序行为模型是安全攸关的CPS在设计与开发过程中需要构建的主要内容[5].为了对系统的时序行为进行描述，国内外研究小组从系统的不同层次、不同角度对系统行为进行刻画.较为著名的研究如加州大学伯克利分校的Eker等人[6]从系统的异构计算模型（model of computation, MOC）角度刻画组件行为，生成组件的异构行为模型，并在文献[7]中通过状态机方法来检查组件之间异构行为的可组合性.其次，Kopetz[8]从通信行为角度对组件时序关系进行刻画，设计时间触发架构用于保证节点与节点之间传输过程的正确性，并给出时序防火墙（temporal firewall）概念[9]来刻画组件的时序行为并判定其可组合性.其次，宾夕法尼亚大学Insik等人[10]的研究工作专注于建立层次化的系统行为模型，描述CPS具有分层的系统架构，建立分层模型逐层刻画行为和验证行为的可组合性.文献[11]中给出了更为传统的系统模型，并描述系统由若干任务、调度器以及时钟等元素组成，以及通过UPPAAL验证工具对任务的可调度性进行验证.

针对CPS进行设计开发仍然需要形式化工具的支持.在已有的方法中，基于状态语义的自动机模型，如接口自动机[12]、I/O自动机[13]等均被用于描述组件的接口行为，并分别依据典型的乐观与悲观2种组合方式对组件的可组合性进行判定.同时，相关工作增加了时间属性并给出时间自动机[14]、时间I/O自动机[15]等方法用于对系统的时间行为进行刻画.Henginzer[16]提出的混成自动机也是一种典型的基于状态建模思想，是能够对CPS中离散行为和连续行为进行建模与验证的形式化方法.2021年，Lin等人[17]也通过混成自动机建模了复杂系统的行为，并以此判定系统的可控性.又如基于事件语义的Event-B形式化方法，相关工作给出了基于Event-B语言的以事件精化、事件组合[18-19]为核心的系统实现方法.其次，迁移系统也是一种能够对组件行为进行建模的有效方法，基于此语义开发的LTSA（label transition systems analyzer）分析软件是一种有效的建模工具，能够对系统进行建模、分析，同时可以判定模型所具有的属性，并当存在违反属性的反例时，能够对反例数据进行输出.因此从易用性、可行性等角度出发，本文最终选择迁移系统作为时序行为的形式化描述方法.

1.2 CCSL时间约束建模

CCSL语言由Zhang等人[20]提出，其作为UML/MARTE语言中的时间模型被广泛关注.CCSL是一种半形式化的语言，对于CCSL的形式化表达及属性验证仍然是一个具有挑战性的工作.为了验证时序约束关系，相关工作已经基于不同的方法对模型进行验证，如自动机、动态逻辑[20]、SMT可满足理论等方法对CCSL进行语义转换并验证.在国内的研究中，华东师范大学Zhang等人[21]的若干工作对CCSL的发展也起到推动作用.

1.3 时间行为的精化

传统的逐步求精方法[22]主要针对UML中的时序图、状态图进行求精的实现，将时序图、状态图模型映射为底层具体模型.然而在对CPS行为进行求精时，如何将顶层的规约精化为底层的具体实现是CBD方法的核心内容.而针对时间行为的精化等同于对任务的时间属性的分解.文献[23]将数据流分成2种类型并进行调度，给出了保证时间约束的数据流调度算法，以使数据延迟变得确定.文献[24]也设计一种能够保证数据流延迟时间约束的调度实现方法，将系统整体的时间约束转化为子系统的时间约束关系，保证传输过程时间行为的正确性.同样，文献[25]提出一种将上层时序规约映射为下层任务执行模型的求精策略，在求精流程中将时间延迟规约分解为子系统级的时间规约，最后生成相应的任务集.在文献[26]中实现了对组件执行时间进行预分配（time-budget）的方法，主要通过2个过程来具体实现：过程1会把时间延迟进行子系统级别的分配；过程2将基于迭代的策略对子系统中的任务进行组合来创建任务子集.

通过对国内外关于CPS建模与精化的研究发现，现有工作中解决CPS的建模问题普遍从计算行为、层次化调度行为等角度入手建立模型并验证属性.而针对安全关键CPS的实际具体开发而言，仍然需要依据已有的上层建模语言，从时间行为角度建立系统的时序行为需求模型，继而通过组合、精化等方法对系统进行设计与验证.通过调研，现有研究中仍然缺少类似工作.为了解决该问题，本文较为系统化地对基于时序行为的建模与验证进行研究，继而从时间行为角度出发，基于CCSL时序约束语言建立系统的时序行为需求模型，借鉴接口自动机的组合机理，通过乐观方法定义时序行为的可组合性.给出时序行为的精化方法，同时通过L*方法来迭代学习模型的行为，并基于此实现针对时序行为的组合验证，以此形成自上而下、统一的开发框架.

2 时序行为建模及可组合性定义

2.1 CCSL建模

CCSL是用于描述系统中时序规约的半形式化语言，该语言定义了丰富的时间约束语义来对系统规约进行表达.比如优先语义（precedence）：m＞n，定义了时钟m的滴答次数要多于时钟n的滴答次数，或者交替语义（alternative）：m～n，表达了时钟m和时钟n会交替滴答产生的约束关系.

CCSL规约语言的核心要素是逻辑时钟，区别于能够度量物理时间的物理时钟，逻辑时钟可以看作是能够在设计阶段对系统中任务的时序关系进行表达的模型元素.本节首先描述一个逻辑时钟的概念，再扩展出系统中存在多个逻辑时钟的时间结构定义.

定义1.逻辑时钟.采用5个标签〈I,≺, D, τ, u〉结构来进行表达.标签I为一系列事件的发生时刻，≺为发生时刻序列I上的严格优先（strict precedence），D是时钟上的记号，通过函数τ进行定义：τ∶I→D，u是时钟递增幅度.针对逻辑时钟而言，递增幅度u可以是系统滴答tick，也可以是总线的传输周期等.

定义2.时间结构.通过标签〈C, ≼〉进行表达，在时间结构中，C为包括逻辑时钟或度量时钟的时钟集合，≼为这组时钟上的先后约束关系.

可以看出，逻辑时钟是一系列具有严格先后关系的时间点集合.通常用来描述某个事件在时间线上的一系列动作.2个时钟之间最纯粹、最本质的关系是优先（precedence）.从最基本关系出发，可以推出其他时序关系，如同时发生（coincidence）、严格优先（strict precedence）、互相排斥（exclusive）等.

例1.假设存在2个时钟c与d，2个时钟的关系为：时钟c与基准时钟延迟1个时间单位，并在之后以4为周期值进行执行（属于subclock子时钟约束的一种），而时钟d与基准时钟延迟3个时间单位，之后同样以4为周期值进行执行.通过CCSL语言进行描述可以得到的关系为：

cisPeriodicOnclkperiod=4 offset=1,

disPeriodicOnclkperiod=4 offset=3.

在CCSL仿真工具Timesquare中对时序行为进行模拟得出的执行过程如图2所示.执行过程描述的3个逻辑时钟的时序约束关系为：首先逻辑时钟clk滴答，在其后产生的是逻辑时钟c的滴答（offset=1），继而，逻辑时钟c以4为周期值进行滴答.逻辑时钟d以逻辑时钟clk为基准，同样以4为周期值产生滴答，并且其偏移值为3（offset=3）.

Fig.2 Diagram of clocks relationship图2 时钟的关系图

2.2 时序约束行为的组合与可组合性定义

在系统开发过程中需要对时序行为进行建模及分析，本文依据文献[27]所给方法通过迁移系统来刻画CCSL，并采用组合推理方式对属性进行检查.

定义3.时钟迁移系统[27].可以通过一个在事件集A上的五元组A=（S，λ，α，β，Tran） 进行表达，其中：

1）S为一组状态节点，s0是初始节点；

2）λ∶Tran→A定义节点转换过程中对应的事件；

3）α，β∶Tran→S是映射函数，节点转换中的起点和终点的节点；

4）Tran⊆S×2λ×S是描述转移集合是节点之间转换关系的子集，当事件e⊆λ，则当节点s到s’的所有触发事件e都发生，并将产生该转换.

描述时钟m的行为Clockm=（S，λ，α，β，Tran），时钟滴答集合为Am={m,ε}，则：

1）S={s} 逻辑时钟m仅存在一个状态；

2）Tran={t,e}是2个转换过程，分别由时钟m滴答和ε产生；

3）α（t）=α（e）=s，β（t）=β（e）=s，是2个转换过程对应的起点节点和终点节点；

4）λ（t）=m，λ（e）=ε，引起转换的相应事件.

图3（a）是时钟m的滴答转换过程，图3（b）是同步关系（mcoincidencen），以及图3（c）是子时钟关系（nis subclockofm）.

Fig.3 Clock ticking behaviors图3 时钟的滴答行为

同样，通过迁移系统对图2中的时钟行为进行建模，可以得到图4所示结果.执行的迹（trace）为{（c=0,d=0,clk=0），（c=1,d=0,clk=1），（c=0,d=0,clk=2），（c=0,d=0,clk=2），（c=0,d=1,clk=3），（c=0,d=0,clk=0），（c=1,d=0, clk=1）,…}.

Fig.4 Relationship diagram of timing constraint based on state transition图4 基于状态迁移的时序约束关系图

在能够表达一个时钟的执行过程后，需要对系统中存在的多个时钟的约束行为关系进行组合来描述整体，最直观的方法是计算多个时钟的笛卡儿积.

定义4.时钟约束行为的组合.对于n个逻辑时钟A1, A2,…,An，其同步行为是A1×A2×…×An的一个子集合I，则多个时钟的约束行为组合可以描述为在动作子集I⊆A1×A2×… ×An上的时钟迁移系统A=（S, λ,α, β, Tran），其中：

1）S=S1×S2×…×Sn，系统的全部状态；

2）λ（〈t1,t2,…,tn〉）=〈λ（t1）,λ（t2）,…,λ（tn）〉，转移过程的事件行为；

3）α（〈t1,t2,…,tn〉）=〈α（t1）,α（t2）,…,α（tn）〉，转移过程的起始状态节点；

4）β（〈t1,t2,…,tn〉）=〈β（t1）,β（t2）, …,β（tn）〉，一次转移过程的目的状态节点；

5）Tran= {〈t1, t2, …, tn〉∈T1×T2× …Tn|〈λ1（t1）,λ2（t2）,…,λn（tn）〉 ∈I}，是所有的转移行为.

定义5.禁止状态.2个系统M与N的乘积为AP×AQ，其禁止状态节点Forbidden（M, N）⊆SM×SN应具有属性：

其中AM（v）与AN（v）是系统M与系统N在组合后所得到的状态v下所接受的事件集合.shared（M, N）表示M与N之间的共有动作.基于定义5，组件组合后，当处于禁止状态下，M对事件e有转移发生，而N对事件e没有转移发生，或两者情况彼此相反，即，在禁止状态下，不能在同一时刻使得M与N一起产生转移，称为禁止状态节点.

定义6.时序行为可组合.如果M和N有一个外部系统E，可以保证M和N在组合后禁止状态节点不可达，可得M和N是时序行为可组合的.

行为可组合的定义描述了系统在组合后的执行行为并没有改变原系统的执行行为，确保了系统在集成前与集成后行为的一致性.基于这个基本检查形式，可以对系统的行为进行笛卡儿积的计算，并在此基础上进行模型检查.本文给出图5的示例进行更具体的说明.

Fig.5 System behavior model图5 系统行为模型

图5（a）描述3个时钟（observe,write,replace）的时序行为，首先时钟observe滴答，之后是时钟write滴答，该模型与图5（b）模型组合后，形成了图5（c）的模型.其中，图5（a）模型中时钟write滴答后期待响应的是时钟replace，而图5（b）模型在产生时钟write滴答后时钟exec滴答，可能产生ok或nok，而在nok发生后将导致时钟incorrect滴答，而该时钟行为是图5（a）模型不能接受的.因此，组件进行组合后有可能进入非法状态Err，导致系统错误.因此组件是不可组合的.简单而言，在组件组合后的状态集合中，某状态并不是所有组件都希望到达的，则该状态称为禁止状态.

“死鬼，接招！看我无敌旋风脚！”我一边喊一边把脚踢了出去。只见那些可怜的鬼还没有反应过来，就被我打倒在地了。哈哈！鬼被我打趴下了！我得意地大笑起来，准备对付下一个目标了。

本文将组件时序行为的可组合性描述为各个组件的时序行为在合并之后，如果能够满足组件原有的时序行为约束要求，则可以定义为时序行为可组合的.如图6所示，系统给出了外部环境的执行过程，外部环境读入exec后，执行内部动作check，最后输出ok告知系统结果.上述过程没有时钟incorrect滴答.可以看出，能够存在一个子系统使得整体系统在组合后没有进入Err节点，则表明系统整体行为约束是具有可组合性的.

Fig.6 A legal external environment图6 一个合法的外部环境

3 组件的时序行为可组合验证

在计算若干个组件行为的笛卡儿积后可以得到整体模型.为了验证属性需要，对计算后的模型进行检查以验证其是否满足时序行为可组合的要求.

3.1 组合验证框架

为了缓解模型组合后产生的状态爆炸问题[28]，本文通过组合验证的方法对时序行为进行检查.组合验证基于分治的思想对个体模型的属性进行检查来减少对整体状态空间的搜索，以此缓解状态爆炸问题.首先介绍最基本的推理规则.

假设-保证推理（assumption-guarantee reasoning,AGR）[29]：该范式包含元素〈A〉M〈P〉，其中，M是一个组件，P是一个属性（可以用迁移系统表示），A是组件M的外部环境的假设条件.该推理规则描述组件M属于某类系统，该类系统在满足假设条件A的前提下，系统可以保证具有属性P.如果系统是由组件M1和M2构成，则描述推理形式为

该规则描述为：如果需要验证组件M1和M2在组合之后的整体行为能够提供的保证为P，则首先得到组件M1在提供保证P时，外部环境需要满足的假设行为A（上述规则中的步骤1），基于此，在推导出假设行为A后，则再检查组件M2在默认外部行为为true时，是否满足假设条件A（上述规则中的步骤2），通过此方法对M1||M2是否满足属性P进行验证.以此通过检查局部状态空间的方法，实现对整体状态空间的搜索.通过组合验证的方法对得到外部环境应具备的假设条件A，在本文中，我们通过L*方法对模型进行推理学习，得到条件A.

为了获得假设条件A，如图7所示，验证框架采用迭代的方式进行组合验证的推理.在每一次迭代过程中，基于上一轮得到的正确行为以及本轮的推导行为，给出假设条件Ai.首先通过步骤1判断M1在外部系统为Ai时，是否能保证提供行为P，如果结果是false，其含义为假设行为Ai偏弱（Ai尚未对外部系统进行足够的限制，存在错误的行为导致属性P不被满足），因此，需要通过返回的反例对假设条件Ai进行强化（对环境Ai的行为太过“宽容”，需要移除一些行为）.因此，在下一轮迭代过程Ai+1中，所学习得到的外部环境至少将上一轮迭代过程中破坏属性P的反例行为给剔除掉.

Fig.7 Iterative based compositional verification framework图7 基于迭代的组合验证框架

当步骤1的返回值为true，则表明Ai的行为已经足够强化，能够满足属性P.为了完成证明，步骤2需要判定在外部环境行为条件为true的情况下，M2是否能满足属性Ai，如果步骤2返回值为true，则表明组合验证成立，M1和M2的组合可以满足保证具有行为P；如果返回值为false，则应该分析M1||M2是否破坏了属性P，或者Ai过于强化.如果Ai过于强化，则需要在第i+1次迭代时通过反例对其弱化，因此，至少在下一轮迭代的时候，这个反例中的行为将在假设条件Ai中被允许.

在具体工作中，本文基于L*方法来对外部环境应具有的正确行为进行学习，不断尝试去找出能够让模型M满足属性P的所有行为，以此利用得到的所有正确行为序列构建出外部环境Ai.

3.2 基于L＊学习的时序行为可组合验证

L*学习早期被用于对正则表达式进行规则推理[30]以得到符合行为要求的状态机.该推理给出一个虚构身份——最小胜任教师（minimally adequate teacher），在具体过程中，方法通过迭代的方式向教师提出2个问题，分别为成员资格询问（membership query）和候选者资格询问（candidate query）.考虑到有些行为没有时间语义，本文将具体的学习过程划分为无时间语义推理与有时间语义推理2个阶段.2个推理过程在整体流程上是类似的，都需要经过“成员资格询问”和“候选人资格询问”2个查询操作.而2个学习过程不同的是，无时间语义推理过程是一种对行为的不断学习（查询）的过程，而在有时间语义的行为推理中，需要不断将全局时间进行分解，不断找出满足属性P的时间行为的过程.

1）无时间语义的推理过程

在对假设条件A进行推理时，该方法先定义一个判定表（S,E,T），在这个表格中S列和E列表示所判定行为的前字符串序列和后字符串序列，最初，S列和E列都是空事件集{ε}.T列是经过“教师”查询后从字符串S∪S·Σ·E到{true, false}（或{1,0}）的计算值.判断该字符串是否属于正确行为，“·”的计算定义为：对于2个字符串m和n，M·N= {mn|m∈M , n∈N}，计算出字符串m和n序列动作.向“教师”查询获得结果后，将判定表中的T值进行更新.（在算法1伪代码中对应的处理过程是行①～⑬）.

算法1.对时间进行学习的L*算法.

输入：事件集合Σ；

输出：通过学习得到满足时间行为的迁移系统.

①S=E={ε}； / *初始化判定表中的集合 * /

②查询ψm（ε），判断是否属于合法的行为，同时查询ψm（ε·σ），更新判定表中的T值，其中σ∈Σ；

③ while true do

④ whileTF（s·σ·e）≠TF（s'·e） do

⑤S←S∪s·σ； / *将s·σ加入前缀集合S中 * /

⑥ end while

⑦ 通过前面判定表中学习得到的行生成相应的迁移系统M；

⑧ ifψc（M）==1 then

⑨ returnM；

⑩ else

⑪ updateT； / * 教师返回反例并对其进行分析，得到后缀加入到集合E中，再次对判定表中的行为进行查询，更新T值 * /

⑫ end if

⑬ end while

⑭σ←（σ,true）；s←（s,true）；e←（e,true） ； / * 通过对无时间语义的行为进行学习得到判定表（S,E,T），在该判定表中加入时间语义，其中，σ∈Σ, s∈S, e∈E* /

⑰ 不满足条件的情况下，给出反例（a1,g1） （a2,g2）…（an,gn） ；

⑱ for （i= 1;i≤n;i++）

⑲ …

⑳ if （ai,g） 是p或e的子串，其中p∈S∪（S·Σt），e∈Ethen [gi]∩[g]≠∅

㉑ 将p分割为，其中（ai,gi）是pi的子串，（aj,gj）是pj的子串，j∈1,2,…,n;

㉒ 将e分割为，其中（ai,gi）是ei的子串，（aj,gj）是ej的子串，j∈1,2,…,n；

㉔ end if

㉕ end for

㉖ whileTF（s·σ·e）≠TF（s'·e） do

㉗S←S∪s·σ； / * 将s·σ加入到前缀集合S中，（s·σ·ε），更新T，其中ε∈Σt* /

㉘ end while

㉙ 得到封闭的判定表，生成Mt，将其提交至教师进行候选人查询（Mt） ；

㉚ 如果返回false，则同时返回反例，对反例进行分析并得到后缀加入到集合E中，不断迭代学习得到假设条件Ai的模型Mt；

㉛ end while

㉜ returnMt.

上述伪代码给出了对行为进行学习的整体过程，最终得到了具有时间属性的、满足行为规则要求的模型Mt，接下来将结合伪代码讲解算法中的成员查询过程和候选人查询过程.

成员查询.该阶段将判断字符组成的事件序列是否属于正确的系统该接受的行为.计算可得，事件序列为σ=〈a1,a2, …,an〉，σ∈Σ，Σ是事件集合.“教师”验证模型〈Aσ〉M1〈P〉.当其值是true时，则成员查询函数ψm（ε·σ）=1，判定表中T值也为1，表明该事件序列没有在M1中影响行为P，应属于正确的事件行为序列.如果ψm（ε·σ）=0，则返回值为false，同时判定表中T值为0，并给出一个负反例，该反例属于当前Ai中的事件行为序列，却破坏了属性P，因此对反例分析后再将该行为剔除掉，得出前字符串并加入判定表的集合S中.向教师提交事件序列进行查询，并同步更新对应的T值（算法1中行②）.最后，通过公式来查看判定表是否为封闭的（行④）：

∀s∈S, ∀a∈Σ, ∃s'∈S, ∀e∈E:TF（sa·e）=TF（s'e）.

候选人查询.通过成员查询过程判断判定表是否是封闭的（算法1中行④～⑥）.如果是封闭的，则依据判定表生成迁移系统M.其中，迁移系统的状态是前序字符串集S中的元素，s0=ε，动作λ=Σ为事件集合（算法1中行⑦）.通过候选人查询函数ψc（M）进行查询，如果返回值为true，则证明M1||M2能够保证属性P（算法1中行⑧⑨）；否则如果模型检查返回false，则同时返回一个正反例（counter- example），该正反例描述了其所表示的事件序列能够满足属性P，却不在Ai中，表明所得到的条件Ai对事件行为进行了过度的约束，应将正反例行为加入到Ai中，再分析正反例得出后缀并加入到判定集合E中，并向教师提交字符序列进行查询，并更新T（算法1中行⑪）.

本节给出针对前述示例1行为的学习过程，初始阶段判定表为空，逐步添加事件行为的前、后字符串序列来对判定表进行创建， 得到判定表T-1（表1）和判定表T-2（表2）.在计算M的判定表时，需要先确定M的事件集，具体地，前序字符串为S={ε}，后序字符串为E={ε}，事件集为Σ={c,d}，向“教师”提交整合后的字符串并查询，判断该字符串序列是否属于所要学习的模型行为，如果属于，就将判定表中对应的T赋值为1，如表1所示.

Table 1 The Observation Table T-1 of Model M表1 模型M的判定表T-1

Table 2 The Observation Table T-2 of Model M表2 模型M的判定表T-2

再次按照算法1中行④所给出规则来检测判定表是否封闭，发现不存在s'满足公式T（s·c·e）=T（ε·c·ε）.则判定表T-1不封闭，并将c添加至字符串集S中，更新T值，如表2所示.

再次检查判定表的封闭情况，如封闭，则将其转换为迁移系统，并发送给“教师”判断该模型是不是正确的假设条件，“教师”返回false，并提供反例序列σ=cdd.此行为是被Ai认可的事件序列，但不是正确的学习结果.因此需要在判定表中更新、计算后序字符串为d.修改判定表，依此过程进行推导，最终得到满足条件的判定表T-3.

计算得到判定表T-3是封闭的，由表3可得出，所学习到的模型包括4个状态s0，s1，s2，s3，状态s0接收到时钟c滴答后迁移至状态s2，图8展示了所有迁移的路径关系，建模了时钟c与d的约束行为.

Table 3 The Observation Table T-3 of Model M表3 模型M的判定表T-3

Fig.8 Learning results without timing semantics图8 无时间语义的学习结果

2）有时间语义的推理过程

对时间属性进行推理的过程也可以理解为是对无时间语义行为进行精化的过程.首先要做的是将无时间语义事件集Σ转换为描述时间语义的事件集ΣT=Σ×GΣ.基于类似的操作，判定表也会变为有时间语义的判定表（算法1中行⑭）.具体地，对于时间语义行为的推理过程为：

①通过算法1中行①～⑬可以生成一个缺少时间语义的假设条件Ai，再把Ai交给函数ψc（M）进行判定（算法1中行⑮～⑰）.

②当函数ψc（M）的判定结果为false，会一同给出一个错误的行为（反例），如 （a1,g1），（a2,g2），…，（an,gn）（第2个元素g1，g2，…，gn是事件a1，a2，…，an产生的时序约束），需要对这个错误行为进行分析并进一步地分割事件流，检查判定表中前字符串S和后字符串E在时间属性上是否包含（ai,g），并满足[gi]∩[g]≠∅，则时序属性[g]被gi分割成[g]=[gi]∪G.在这样的方式下，前字符串序列S将被分割为，具体地，元素（ai,g0）刻画了，元素（ai,gj）刻画了Sˆj.同样，判定表中后字符串序列E也被分割为，元素（ai,gi） 刻画了， 元素（ai,gj） 刻画了， 其中j∈{1,2,…,m}.在这个阶段，基于对时间属性的分割把无时间语义的事件分解为多个具有时间语义的事件结构，再将事件流提交给函数进行检查，其形式为，其中j∈{1,2,…,m}，再对判定表中的T值进行更新（算法1中行⑱～㉓）.

③依据行⑭～㉓将得到更为具体的判定表，并再检查其封闭性.对于前字符串序列s·a，如果没有发现某个s'∈ Σt，满足s·a≡s′，则定义这个判定表不封闭.这样就要把s·a添加进集合S，再利用函数（s·a·ε）重新对判定表中T赋值（算法1中行㉖㉗）.

④当判定表是封闭的，再把判定表转换为迁移系统Mt，并通过函数（Mt）检查其是否满足属性要求，如果Mt不是正确的学习结果，则将给出反例修订判定表，再次迭代学习，直至得到所学习到的正确的模型Mt（算法1中行㉙）.

如下对2.1节中例1进行时间属性学习的过程描述.首先对第1阶段（无时间语义的行为推理过程）得到的判定表进行时间属性的赋值，如表4所示.

Table 4 The Observation Table T-4 of Model M表4 模型M的判定表T-4

在判定表T-4中，Σt= {（c,true）,（d,true）}，St={（ε,true）,（c,true）,（c,true）,（d,true）,（d,true）,（d,true）}，同时后序字符串序列Et={（ε,true）,（d,true）}.可以把判定表 T-4转换为假设条件，并再把交给函数ψc（M）进行检查，如其值为false，则会提供一个破坏属性的行为：σ={（c=1,clk＞1）（d=1,clk＞1）}；然而当判定表中S={（c,true）（d,true）}，则判断时间属性的有效值：|(clk＞1)(clk＞1)|∩|(true)(true)|≠∅，并把前后字符串序列的时间约束进行分解，事件c和d的时间约束分别分解为（c,clk＜1）和（c,clk＞1），同时（d,clk＜1）和（d,clk≥1），再次利用判定表得出事件序列，并提交给函数（Mt），获得T值，可得表5中的判定表T-5.

Table 5 The Observation Table T-5 of Model M表5 模型M的判定表T-5

不断对模型进行学习，能够形成封闭的判定表T-5，通过判定表T-5可以得到图9中的假设条件Ai（转换为模型M）.

Fig.9 Assumption Ai derived from reasoning图9 推理得到的假设条件Ai

L*算法的正确性.L*算法通过对模型M的行为进行学习推算得到一个拥有最少状态集的系统TS.首先，L*算法在推导阶段的每个迭代过程中得到的模型在状态数量上是增长的，每轮迭代过程所得到的模型中状态数量都比上一轮迭代过程中的状态数量多.究其原因，判定表中所给出的前序字符串S就是所推导出模型的状态集合，所得到的模型应该有数量为|S|的状态节点，而在学习过程中，在得到正确的模型之前，每轮迭代所得到的模型都是错误的，因此，每轮迭代所得到的状态数量都是最少的，直到学习到了正确的行为，这样，在学习到一个行为正确的模型时，这个模型包含最少数量状态的状态集合.而在猜测次数上，假设模型有n个正确的状态，算法将作出n-1次候选人查询.

4 组件的时序行为精化方法

精化实现了对系统规约逐步具体化的操作过程[31].为了建立具体时序行为模型，本文通过CCSL时序约束语言建立上层时序模型，并对3种典型的时序规约实现精化.本文给出精化关系定义7.

定义7.时序约束关系的精化.如果模型K=(SK,s0K,ΣK,→K)与模型L=(SL,sL0,ΣL,→L)存在精化关系，描述成K≼L，表示为具有关系R⊆SK×SL，（sK0,s0L）是初始状态节点，对于所有节点(s,t)∈R，属性成立：如果其中(k′,l′)∈R,k′∈SK；

定义7定义了2个模型（K和L）满足精化条件(K≼L)，模型K和L具有关系(R⊆SK×SL)，其中，在某个状态节点（K,L）下所有事件c1,c2,…,cn发生，在L中产生转移同样动作〈c1,c2,…,cn〉下模型K中产生转换则称模型K和L满足精化条件.

精化过程实现了从较高层级模型到低层级模型的过渡与转换.高层模型表达了系统需求层的时序关系，低层模型可以表达更为具体的系统任务级的时序关系[32].为了构建上层时序规约，本文以3种基本的时序约束需求作为基础来建立规约模型并进行精化.3种约束关系分别为：

1）延迟约束.考虑系统读入某个数据，然后内部任务计算反馈数据，并再把反馈数据进行输出的时间区间.假设某组件在时刻m读取外部控制命令，经过本地控制任务处理得到反馈信息，并在时刻n写入外部缓存，同时限定整体处理时限为t，类似这样的约束关系可以采用CCSL中的n-m＜t进行描述.

2）关联约束.考虑组件中的某个输出动作，追溯到所有与其相关的输入动作，则关联约束刻画所有输入事件的同步关系，可以利用时序约束语言CCSL中最小上界inf（）和最小下界sup（）进行刻画.

3）间隔约束.在某系统中，限定输出事件的产生在某个时间范围内称为间隔约束.如某示例，“汽车制动指令将在20～50 ms之间产生”，类似约束可以在CCSL中使用min＜n-m＜max关系进行刻画.

刻画任务在执行过程中的前后顺序依赖关系是精化过程的基础，为了刻画依赖约束，本文将通过任务图来建立时序行为需求规约与任务模型之间的关系.

4.1 任务图结构

利用任务图G（U，V，N）结构可以刻画任务之间的优先顺序，其包括基本元素：

1）U表示图中节点，V表示图中的边，N={τ1,τ2,…,τn}描述任务；

2）更为重要的是，每个任务具有相应的特征，Ti为任务的执行周期，任务的初始相位Pi应大于0，任务执行的时限Di应大于Pi，同样，任务应具有最差执行时间ei的属性，在各属性中，[Pi, Di]时间段刻画了任务可调度运行的区间Wi（Wi=Di-Pi）.

3个属性Ti，Pi，Di描述了任务τi的时间行为，本文将对其进行逐步求精推算.

对时序行为进行精化的过程如算法2所示，针对时序行为进行精化的方法包含3个步骤：

1）算法初始化过程.罗列需求（如给出系统的几种时序行为需求、建立任务图等）（算法2的行①）、给出任务图、描述时间约束（timing constriant, TC）、定义若干变量（主要为任务周期、任务的截止时间，以及任务的初始相位等）.

2）时间属性细化过程.通过约束关系将任务的时间属性进行细化，得到任务时间属性的解空间，再通过变量消除方法消除相位Pi以及截止时间Di，得到仅有任务周期Ti的约束关系，同时使用利用率进行周期值的计算，得到任务的属性值（算法2的行②③）.

3）推导出任务若干时间属性的过程.得到任务周期值后，通过启发式方法对相位Pi以及截止时间Di（算法2的行⑤～⑩）.

算法2.时序行为的精化方法.

输入：时序约束需求模型；

输出：精化后的时序约束任务模型，周期Ti，任务实现Di，相位Pi.

① 给出系统任务图结构G，描述系统中任务τ1,τ2,…,τn之间的依赖关系；

② 根据任务图以及需求中的时序约束关系，通过任务之间的步调协同约束关系、延迟约束关系、间隔约束关系等，推导出任务参数Ti，Di，Pi的整体解空间S；

③ 消除解空间中的变量Di，Pi，将S映射到只有周期变量的子解空间；

④ 在得到周期值后，通过启发式方法求得相位值与截止时间；

⑤ fork=0 →n-1 do

⑥Pk=0； / * 设置Dk为所有任务中最大的周期值，初始化任务的相位、截止时间 * /

⑦ forj=k+1 →n-1 do

⑧ ifτj≺τkthen

⑨Pj=Dk,Dj≤Pj； / *具有优先关系的任务，其相位值等于（或大于）前序任务的截止时间，进一步得到二者之间的关系 * /

⑩ end if

⑪ end for

⑫ end for

⑬ 目标力争最小化任务的相位值，最大化任务的截止时间，以此最大化任务利用率，得到Pi与Di的解空间，求得最优值；

⑭ returnTi,Pi,Di.

针对时序行为进行逐步求精，本质是将上层的时序规约转换为底层具体实现的过程，为了满足行为的一致性，转换过程应保证3方面的特性要求：

1）正确性.将精化后任务层的时序关系描述为TC，其次假定δ是系统的上层时序约束规约，在此定义下转换出的 TC需要能够满足δ的要求.

2）可行性.通过精化方法可以得到任务的若干时间属性，如周期、相位等，而在此时间属性下，需要保证所有任务调度执行的可行性，同时在所有任务运行的情况下，资源利用率应小于1.

3）可组合性.通过精化过程能够推导出任务模型（周期、相位等），同时该任务模型能够满足系统时序规约的要求，可以得到多个子系统（组件）之间的时序行为是可以进行组合的.

4.2 约束关系的处理

任务之间的传输数据要尽量能够保持数据传输步调的协同性.发送端和接收端的速率过于杂乱不利于数据的处理.如图10中的示例，发送端和接收端具有一定的协同性，任务τ2可以容易地处理接收任务τ1的数据，因为任务τ1的发送周期P1=10 ms，而任务τ2的接收周期P2=30 ms，则任务τ2每隔3个时间间隔对数据进行接收（忽略掉2个），可参见图10示例.

Fig.10 Task behavior with harmonious relationship图10 具有协同关系的任务行为

定义8.任务周期的协同性.考虑2个或多个任务之间具有先后顺序的依赖关系，在这种情景下，如果周期之间存在倍数关系，则称任务之间是具有周期协同性的.假设任务为τ1和τ2，相应的周期值为T1和T2，2个周期值具有关系：T2=KT1（K∈ ℕ+），则2个任务的执行周期是具有协同关系的（T2|T1）.在图11的任务图结构可给出约束关系：

Fig.11 Timing relationship of task chain图11 任务链的时序关系

针对具有共同输入事件的2个或多个任务而言，其输入行为将影响2个或多个任务，假设存在任务τ1和τ2，任务具有共同的输入行为I2，而2个链路的写入外部环境事件分别为O1和O2，为了简便起见，可以把2个数据输入行为进行合并.在图11中，存在2个任务链路都包含输出到外部环境的事件Y2，在这种情况下，可以把相应的同步输入行为{I1,I2,I3}统一合并为任务τs.并结合任务的时间属性给出式（2）的定义：

其中，Jcorrd表示多个任务链路中输入行为的最大抖动时间.

定义9.延迟约束的处理.F（O|I）=tf定义了这样的约束关系：为了保证任务在时间t内把写入外部环境的事件O执行完成，参与这个输出值计算的全部输入数据事件I应该早于t - tf的时间到达.

这个过程涉及到从输入到输出的整条任务链，而整条任务链中的时间行为将具体涵盖每个任务的任务计算处理时间以及数据传输过程所用时间.其中，任务的计算处理时间描述任务具体代码段在特定平台上的运行时间；而任务的数据传输过程所用时间涉及到任务在整条链路的执行过程中由于等待数据输入产生的延迟时间.在本质上，应该让等待任务输入数据的时间尽量减小，而对于前面所给出的任务同步输入行为的处理，恰恰能够解决该问题，使多个输入任务的处理时间达到最优.

系统中任务的处理流程通常呈现链路路径的形式，比如τ1,τ2,…,τn，在该路径中τn是最终写入外部环境的任务，τ1是最初从外部环境读入数据的任务，相应的周期是T1,T2,…,Tn，从任务的协同性考虑，得到关系式Ti+1|Ti（1≤i＜n）.比如考虑图11中有3个任务τ1,τ2,τ3，如果从协同性上考量可以得到T3|T2以及T2|T1.

其次，从整体任务或部分任务的输入输出行为上考量，可以得出的关系式为：

基于任务的时间行为属性，同样可以得到一些基本的时间约束关系，比如基于任务的优先顺序可以得到关系式Di≤Pi+1（1≤i＜n），描述了第i个任务结束后，第i+1个任务可以开始执行.

定义10.间隔约束关系的处理.该时间约束描述了2个连续输出的相同事件在时间属性上的关系，类似例子所描述的“控制指令的输出需要在3～13 ms之内完成”，描述了控制指令最短在3 ms时输出完成，最长在13 ms时输出完成，则可以分别表达为：l（O）=3和u（O）=13.

如图12所示，在任务的执行过程中涉及多个与时间约束相关的时间属性值，其中包括任务执行的初始时间点位置（相位Pi）和描述任务执行结束的时间点位置（时限Di）.

Fig.12 The timing behavior of separation constraint图12 具有间隔约束的时序行为

在此基础上可以结合任务的时间行为属性给出具体的约束关系式，即当第i个输出事件尽量早发生，第i+1个输出事件尽量晚发生时，该情景下产生输出事件的最大的间隔输出时间；当第i个输出事件尽量晚发生时，第i+1个输出事件尽量早发生时，该情景下将产生输出事件最小的间隔输出时间.相应约束关系为：

在描述任务的时间行为约束关系时，除去基本的任务执行周期、相位等时间元素，任务在执行中的计算时间上界e同样是比较关键的建模内容.可以建立任务的执行时间ei、相位Pi以及截止时间Di之间的关联.

同理，将上述关系扩展到多个任务的情景，能够推导出如式（6）的约束表达（其中，E=e1+e2+…+en）.

4.3 约束关系的推导

针对某系统，能够通过式（1）～（5）得出任务的时序约束关系表达式集合，在此基础上对式（1）～（6）进行推导得出具体的变量值.相关流程为：

1）通过式（1）～（6）能够得到系统整体的时序约束关系集合S，剔除其中的相位与截止时间，得到仅涉及任务周期值Ti的时序约束集合；

3）将步骤2）中计算得到的Ti代入最初的时序约束S，在此情况下将生成仅关于相位和截止时间的关系集合，进一步利用线性关系对相位和截止时间属性值进行最终推导.

4.3.1 变量消除方法

在对时间属性值进行推导的过程中需要不断地对变量进行消除.本文利用傅里叶-莫茨金消元法[33]来对变量进行消元，将关系式中的若干元素（周期、相位等）有限次地变换，消去其中的某些元素.当存在若干元素x=（x1,x2,…,xn），且多个元素之间满足的关系为：

为了通过消元来计算每个元素的值，需要进一步推导出元素之间的关系，具体给出的关系式为：

再对x¯进行处理，能够给出如式（10）所示的取值范围空间.

假设某个例子，相位和截止时间之间的关系为P4≥D4+18，P4≤31-D4，通过式子转移将P4进行消除，得到的关系式为：

限定取值范围为正整数，则D4相应的取值范围为{1,2,…,7}.

在计算任务的周期Ti时，依据前面给出的优先顺序约束，以及任务执行周期Ti的协同性等基本限定，同时，任务执行应保证资源利用率的限制，得：

基于此，建立系统的任务结构图能够确定时序规约和底层时序行为之间的推演关系，通过式（1）～（11）能够确定基本的任务模型解空间.进一步对周期值进行限定，能够细化取值范围并最终确定最优的任务执行周期Ti.

4.3.2 相位和截止时间推算方法

通过前面的计算过程能够推导出周期的取值范围，并最终求得最优解.将所得到的周期值代入式（1）～（11）中能够得到关于相位Pi和截止时间Di的关系式.对相位和截止时间的推导可以基于贪心算法完成，其原则为，在任务可调度的前提下，使得运行窗口尽可能大，则要求Di值尽可能大，而使得相位的取值尽可能小.依据此规则来对这2个值进行推导.

5 实验分析

为了对方法进行性能评估，本文开展了2个实验.第1个仿真实验评估了精化方法的性能，第2个实验通过智能小车示例评估模型的组合，验证方法的性能.

5.1 精化方法性能分析

为了对精化方法的性能进行评估，本文对比了多种将需求规约转化为实现模型的精化方法，主要从2个角度分析性能：1）精化的扩展性通过具体分析精化过程所用时间得到；2）生成任务集的效能通过相同约束场景下生成的任务数量进行评估.表6给出了相关的实验设置.

Table 6 Scenario of Experiment表6 实验场景

与当前多数针对CPS的建模与精化的工作类似，为了全面评估精化方法的性能，本文与2种具有代表性的关键方法进行对比：1）UML-RT方法.该方法通过扩展UML语义和通过封装体（capsule）、端口（port）与连接器（connector）等元素建立系统的静态与动态模型，最终转化为任务.2）Shige方法.通过建立时间需求模型，并对时间行为进行分解与合成等操作，生成系统任务.

精化过程的性能评估涉及到支持模型数量多少的问题，可将其定义为模型精化方法的可扩展性.在进行评估时通过整体精化过程中相同模型转化为底层具体实现模型时所调用的代码行数来进行评判.代码行数体现不同方法对于解空间集合进行搜索求解时的性能及效率，是扩展性的体现.相关统计数据可见图13，在对相同模型进行精化的前提下，本文方法和UML-RT方法相比较，平均可降低0.11次迭代次数；与Shige方法相比，平均可降低3.16次迭代次数（迭代次数取自然对数）.

Fig.13 Computation on of iterations of different refinement algorithms图13 不同精化算法的迭代次数对比

另一个重要的性能分析指标是精化方法的有效性，本文依据精化方法所生成任务模型的任务数量来对其进行评估.在相同的需求场景下，生成任务数量越少，任务切换及调度代价越小则精化方法表现越好.在操作过程中，分别给出不同的场景需求，将利用率划分为0.75 /0.85/ 0.95（低/中/高），同时对系统的时序需求规约进行随机生成（端到端延迟、任务执行时间等）.

图14给出不同精化方法在限定组件数量的前提下，随机生成系统的时序需求规约，并通过不同精化方法得到任务模型中任务数量的对比.由于对资源利用率的限定，不同精化方法生成的任务数量也存在差异，统计数据可见，本文所给方法在满足利用率要求的前提下，所构建任务数量相对较少.同时在系统组件个数分别为12和16的场景下，组件为16时精化后任务集的利用率相对更低.本文方法可以在保证时序约束的前提下，系统资源利用率可提升约15.22%.

Fig.14 Comparison of the number of tasks generated by refinement图14 精化生成的任务数量对比

5.2 组合验证方法的实验及性能评估

本文通过实现智能主从小车系统来对组合验证方法进行性能评估.该系统由手柄端、主车端以及从车端组成，其执行过程为：首先，手柄端发送操作命令至主车端，主车端收到命令后，对数据进行解析并执行具体操作.主车端也将自身信息发送至从车端，使得从车端执行跟车等动作.对时间行为约束关系进行分析，最为关键的时间属性是端到端的时间约束关系.如表7所示的具体规约主要定义3种时间约束行为：1）主车端内部任务流延迟.从接收到手柄端控制命令开始到发送至控制单元的控制流时间延迟.2）主从车端传输延迟.主车端需要将自身的速度、姿态等信息数据发送给从车端，并将操作指令输出到从车端执行单元的时间延迟.3）从车端内部任务流延迟时间.由从车端采集自身的速度、姿态等信息，经过计算后发送到从车端执行控制单元所用的时间.

Table 7 Requirement Description of End-to-End Delay表7 端到端延迟的需求描述ms

从时序约束行为的角度出发，通过构件化的方法对系统进行设计和开发.首先建立任务之间的优先顺序结构图，同时给出具体的需求规约模型（部分如图15所示）用于后续组件时间行为的可组合验证.

Fig.15 Behavior requirement model of delay constraint relationship in automotive system图15 智能车系统中延迟约束关系的行为需求模型

在图16中，任务τ1建模手柄的操作命令发送到主车，主车读取数据的行为；任务τ2建模了主车采集自身速度、位置等数据的行为；任务τ4建模了主车自身的内部任务，对速度、方向等数据进行计算，并发送到控制单元的行为；任务τ5建模了读取姿态、速度等信息，并发送给从智能车的行为；任务τ3建模了从智能小车获取传感器姿态、位置等信息的过程；任务τ6建模了对控制命令计算后，发送到组件O2的过程.

Fig.16 Task structure diagram of automotive system图16 智能小车系统的任务结构图

得到系统的任务结构图后，依据式（5）（6）可以得到表8中的任务-时间属性关系式.

Table 8 Timing Behavior Relationship deduced from Task Link表8 任务链路推导的时间行为关系

将变量（周期、相位、截止时间等）和常量（任务的执行时间）代入任务-时间属性的关系式，依据傅里叶-莫茨金消元法，由式（8）～（10）消除特定变量元素并推导出时间属性的最优值，如表9所示.

Table 9 Determination of Task Time Properties表9 任务时间属性的确定

如表9所示，对任务进行精化后可以得到具体的任务结构（包括任务执行周期、截止时间等）.得到任务的基本时间属性后可以利用传统的调度方法（单调速率RM、最早截止时间优先EDF等）进行调度实现.图17给出了采用RM单调速率调度方法的调度过程.

为了评估组合验证方法的性能，本文针对智能主从小车系统给出2个版本的实现，在第1个版本（CAR-1）中实现了手柄数据收发、从车读取主车信息并跟随等功能，在第2个版本（CAR-2）中实现了主从小车距离检测、从车的姿态回传等功能.基于对需求的分析，给出规约模型并逐步精化，得出具体模型.本文分别对3种验证方法进行性能评估及对比，具体是：1）组合验证方法.通过本文所给的方法对时序模型逐步求精并验证.2）分组验证方法.基于本文所给组合验证方法，利用启发式方法进行组件分组的验证.3）时间I/O自动机的验证方法.得到系统的任务模型后，通过时间I/O自动机建立模型并基于UPPAAL工具[35]对模型进行验证，具体的统计数据见表10和表11.

Table 10 Experimental Statistical Results of CAR-1表10 CAR-1的实验统计结果

Table 11 Experimental Statistical Results of CAR-2表11 CAR-2的实验统计结果

CAR-1中存在3个时序约束规约，结合前面推导出的任务结构给出了32个逻辑时钟定义，包括初始执行相位、截止时间等，本文借鉴华文献[36]给出的任务结构来建立具体模型.同时利用本文所给的组合验证方法与图15所示的系统需求模型（specification model）所精化后的模型进行可组合验证.需要验证由表10所生成的任务模型是否满足系统时间属性的要求，如图18所示.相关的验证结果统计如表10所示，在CAR-1场景下采用的组合验证方法用时12.27 s，采用的分组验证方法用时9.98 s.通过自动机模型进行验证（UPPAAL工具）用时较长，约为38 s.

Fig.18 Verification rules for automotive system图18 智能小车系统的验证规则

如表11中的统计数据，本文所给方法在模型检查所用时间以及消耗内存方面，尤其在分组验证的模式下，验证用时降低约63.24%，内存的使用约减少44.01%.同时，模型过于复杂导致内存消耗较大，使得表11中的规格5和规格8在组合验证方法中没有完成.而在这2种规格分组验证的方式下，验证过程用时约为38 s，内存消耗峰值约为73 MB.

为了对方法进行综合考量，本文也利用基于状态语义的建模方法对智能车系统进行行为建模，并采用UPPAAL验证工具对模型进行检查.其中，针对CAR-1系统的所有属性，检查都能够完成并得到相关结果.而在CAR-2系统的行为验证中，由于系统的复杂性导致在验证过程中出现状态数量急剧增长的情况，几个属性验证没有得到结果.相关验证时间和内存使用的数据统计如表10和表11所示.

6 结 论

对安全关键的信息物理系统进行建模、分析和验证是该类系统开发过程的关键步骤.本文给出了一种基于时序行为的系统建模及验证方法，首先通过CCSL时序约束语言构建上层的时序行为需求模型，并对时序行为进行精化，最终通过组合验证的方法对系统的实现模型进行验证.本文通过仿真实验与小车示例对方法进行了评估，相关统计数据表明本文所给方法在一定程度上提高了精化和验证过程的性能.

在未来的工作中，将基于CCSL语言进一步开展系统时序行为分析及验证等相关工作，包括将任务模型转化为具体底层代码、扩展建模工具来对CCSL进行支持等相关研究与探索.

作者贡献声明：陈博提出实现方案、分析实验数据，以及撰写论文；李曦提出了研究思路，并审阅文章内容；周学海提出论文写作思路并修改论文.