一种实时系统时间约束验证方法研究

潘诚　王珊珊　王梓　司佳

摘要：目前，能够对汽车电子领域中复杂嵌入式系统安全关键软件功能模和时间约束分析的方法尚在研究中，而这些系统作为实时控制系统，应该确保其具有准确的、可分析的时间行为。时钟约束规范语言CCSL是实时系统的标准描述语言中描述时钟约束的规范语言。采用CCSL规范表达式描述实时系统时间约束；设计了CCSL基本元素到时间自动机基本元素的转换规则；使用时间自用机验证工具UPPAAL对转换得到的自动机模型进行验证分析，验证实时系统是否满足相应的时间约束。

关键字：实时系统；CCSL；时间自动机；时间约束；模型检测

中图分类号：TP311文献标识码：A

Abstract：Nowadays，functional modeling and time constraint analysis are separated for safetycritical software in complex embedded system，in the areas of automotive electronics.These systems as realtime systems should be ensured that they are accurate and can be analyzed by time constraint.Clock Constraint Specification Language （CCSL） is the standard language for describing clock constraints in a standard description language of a realtime system.Time constraint of realtime system described by CCSL regular expression；The transformation rules of CCSL basic elements to time automata basic elements are designed.Using UPPAAL，we validate that the realtime system satisfies the corresponding time constraints by verifying and analyzing the converted automata model.

Key words：realtime system；CCSL；time automata；time constraint；model checking

1引言

嵌入式实时系统中存在大量、复杂的组件交互行为，其中广泛应用于航空航天、汽车电子、核电等对实时响应，时间约束具有较高要求的安全性工业控制中[1]。随着软件体系结构越来越复杂，软硬件的交互行为越来越广泛，这些行为如果不严格满足特定的时间约束，则有可能带来不可估量的生命财产损失。如何设计有着高质量、高可靠性的实时系统，并且可以进行时间约束的验证工作，这是学术界和工业界亟待解决的一大热点问题[2]。

目前为止，UML/MARTE[3]（ Unified Modeling Language /Modeling and Analysis of Real Time and Embedded systems）已成为工业界认可的针对实时系统的标准建模语言且已广泛使用。CCSL[4]是MARTE规范中的一个附件，专门用来描述实时系统中各组件之间的时钟规范，它在MARTE时钟基础上建立了时钟间的因果关系和时间约束。本文提出一种基于时间自动机的时间约束验证方法：首先，实时系统中的时间约束被描述为CCSL表达式；然后给出CCSL表达式到时间自动机之间的转换方法；最后根据得到的时间自动机网络，在UPPAAL[5]工具中进行验证，分析時间约束是否被满足。

本文后续章节安排如下：第2节，简要介绍时钟约束规范语言CCSL、时间自动机TA，给出基于时间自动机的实时系统时间约束验证框架；第3节给出CCSL表达式到时间自动机的转换规则；第4节，通过一个实例说明本文提出方法的可行性和有效性；第5节，结束语。

2相关理论

21CCSL

UML/MARTE引入了一个丰富的时间模型来支持离散和连续时间，物理和逻辑时间。在MARTE中，时钟（Clock）是时间模型中的重要元素[6]。在使用MARTE时间模型时，某些独立的时钟又一般定义为单独的模型，CCSL是描述这些时钟模型的规范语言。

定义2.1CCSL时钟：一个时钟可以描述为一个五元组C = < T，<，D，λ，u >，其中T是瞬时的集合，<是Γ上关系的集合，D是标签的集合，λ：T→D是标签函数，u是一个符号化的单元。

时钟可以分为逻辑时钟（离散时钟），物理时钟（连续时钟），CCSL描述的时钟为逻辑时钟[7]，u被称为一跳（tick），表示对应瞬时的发生。有序集合< T，< >是时钟上的时序化结构，<是T上的非自反，可传递的二元关系。由于逻辑时钟也是离散时钟，那么瞬时集合T中的瞬时可以采用自然数来表示排序关系：如果

CCSL的时钟模型是MARTE对时间概念的进一步抽象，在MARTE的规范说明书中，时间建模是其重要部分之一，其中包括元模型的建立，与其他模型之间的关联等，CCSL语法包括时钟约束CC（clock constraint）、时钟关系CR（clock relation）、时钟表达式CE（clock expression）、时钟规范CS（clock specification）和关系操作Rop（relation operators）。其中时钟关系与时钟表达式是本文关注的重点，使用巴克斯（Backus-Naur）范式对其进行描述[8]，如图1所示。endprint

22时间自动机

在对实时系统的软件安全性分析中，由于计算过程通常需要在满足特定的时间约束条件下才能进行，为了解决这一问题，Alur R于1994年提出时间自动机（Timed Automata，TA），其本质是一种扩展了时间变量的有限状态机，通过时钟（主要包括用来描述绝对时间的物理时钟和描述相对时间的逻辑时钟）和时钟通道等概念来描述系统时间约束性，有效实现了对实时系统行为的形式化描述及计算[9]。

在时间自动机中，系统的行为由时间变量约束，系统所处的状态由位置节点表示，位置节点之间的有向边表示系统状态的迁移。在系统运行的开始阶段，系统内置时钟初始化为0，随着时间的推移，系统的运行时间不断增长，当内置时钟变量的值满足有向边上的迁移条件（如有同步信号则还需同步信号到来）时便发生状态的迁移。这种基于时间约束迁移条件的自动机保证了系统在时间轴上不会一直停留在一个状态。

定义2.2时钟约束：时钟约束集合由时钟变量集合C，约束关系集合

Φ组成，其中Φ（C）={φ|φ是一个时钟约束}

表示时钟约束集合[8]。时钟约束φ具有如下定义：φ=x≤c|x≥c|xc|-φ|φ1^φ2，其中x∈C表示时钟变量，x∈R+表示非负实数常量，φ1和φ2表示两个不同的时钟约束。

定义2.3时间自动机语法[10]：一个时间自动机可以由一个六元组表示，六元组的定义为：A=，其中：

P是时间自动机A中有穷状态的集合，此集合非空；

P0是初始状态的集合，且P0P；

Q是时间自动机A中有穷时钟变量的集合；

S是时间自动机A中有穷事件的集合；

M是映射关系的集合，M可以表示为状态之间的笛卡尔积，对于m∈M，记m=， 其中p表示起始状态，p0表示目标状态，且p、p0∈P；s是遷移动作，φ表示时钟约束，x是时钟变量；m表示在迁移动作s的触发下，约束条件φ得到满足，时间自动机A从起始状态迁移到目标状态，同时时钟变量x被更新；

T是状态集合P到时钟集合的映射，记为P→Φ（0）。

定义2.4时间自动机语义[10]：对于时间自动机A=，它的语义可以通过转换系统PA来描述。PA的状态表示为一个二元组（p，f），其中p∈P，f是T（p）的时钟解释，满足T（p）；若p∈P0且f（q）=0，那么状态（p，f）是初始状态。PA中主要有两类转换：

1）延迟迁移，即因时间的流逝导致状态发生改变而引发的迁移：（p，f）q（p，f+q），其中q∈R+，f∈T（p）且f+q∈T（p）。

2）离散迁移，即因位置的变换而引发的迁移：（p，f）q（p′，f′），当且仅当sa，φ，qp′时，f∈T（p），f′=[q→0]f，f′∈T（p′）。

23验证框架

本文基于时间自动机的实时系统时间约束验证框架如图2。

该方法首先系统行为和时间约束结合起来用CCSL规范表示；然后根据给出的CCSL到时间自动机的转换规则，将CCSL表达式转换为时间自动机；最后导入到UPPAAL中验证。

3CCSL到时间自动机的转换

31CCSL的状态迁移语义

CCSL是描述UML/MARTE时间模型的时钟规约语言，能够采用时钟模型对系统行为和时间需求进行规约，但是其规范说明书中并未明确给出与状态迁移相关的语义[11]。在给出CCSL和时间自动机之间的映射关系之前，为CCSL引入基于状态迁移系统的语义是必要的。

定义3.1时钟状态迁移系统（cLTS）：时钟状态迁移系统是一个四元组，A=，其中：

1）S是状态的集合；

2）s0∈S是初始状态；

3）C是有限时钟集合；

4）TS×2c×S是转换关系的集合，其中（s，Y，s′）∈T表示当系统从状态s迁移到状态时s′，在中YC所有的时钟都会跳动一次。

CCSL规约可以采用cLTS表示。其中状态表示当前系统经过时钟跳动之后所处在的位置，状态之间的有向边表示相应的时钟跳动一次。下面给出几种简单的CCSL时钟关系的状态迁移图：

同步关系：时钟a，b是两个逻辑时钟，对于任意调度σ∈N→2c满足条件（σ=a=b）（n∈N，a∈σ（n）b∈σ（n）），则a与b满足同步关系a=b。状态迁移图如图3所示。

包含关系：时钟a，b是两个逻辑时钟，对于任意调度σ∈N→2c满足条件（σ=a=b）（n∈n，a∈σ（n）b∈σ（n）），则a与b满足包含关系ab。状态迁移图如图4所示。

互斥关系：时钟a，b是两个逻辑时钟，对于任意调度σ∈N→2c满足条件（σ=a=b）（n∈N，aσ（n）Vbσ（n）），则a与b满足互斥关系a # b。状态迁移图如图5所示。

32CCSL元素到时间自动机元素的映射

CCSL支持Integer、Boolean、String以及Real等数据类型，而在UPPAAL中仅支持整型Integer、布尔型Boolean以及字符型String三种基本数据类型（数组等其他类型都是从这三种演化而来的）。根据CCSL和UPPAAL时间自动机对于数据类型的定义，给出它们之间的映射关系，如表1所示。其中，Real类型在映射到整数型时直接向下取整。

CCSL规约将系统行为抽象为时钟表达式，其中时钟刻画了系统在其运行时某一类事件发生的序列，时钟关系描述了系统在其运行时多类事件之间的优先关系，时钟表达式则描述了系统在其运行时事件之间更为复杂的约束关系。根据CCSL和时间自动机中各元素的定义建立它们之间的语义映射规则，其中CCSL规约代表了整个系统行为在语义上与UPPAAL时间自动机网络一致；时钟是瞬时的集合，定义了某一个事件循环往复地发生在语义上与循环结构的自动机状态之间的循环迁移发送广播通道（Broadcast channels）的语义相一致。如上节所述，CCSL并没有明确系统具体所处的状态语义，时钟的瞬时跳动只能表达状态的迁移，即UPPAAL位置之间的有向边，而UPPAAL中的位置只能隐式地表达为时钟瞬时跳动前后的某些状态。CCSL和UPPAAL自动机元素的语义映射详见表2。

CCSL具有多種时钟关系和时钟表达式，其中优先关系，周期表达式，延迟表达式与本文时间约束密切相关，下面给出它们的详细映射规则：其中S状态表示成功状态，F状态表示失效状态。

1）优先关系：优先关系指定了两个时钟的逻辑关系，如果时钟A优先于时钟B，那么时钟A的瞬时也优先于时钟B对应的瞬时。图6表示优先关系映射的时间自动机模板。

2）周期表达式：周期表达式一般用于离散时钟的生成，即时钟从连续物理时间中取周期运算，获得具有某一周期的离散逻辑时钟。图7表示周期表达式的时间自动机模板。

3）延迟表达式：延迟表达式指定了一个参考时钟，目标时钟是由参考时钟经过延迟后生成的，即对于参考时钟的所有瞬时，目标时钟的所有对应瞬时都要延迟一定的时间区间T[low，upper]。图8表示延迟表达式的时间自动机模板。

4实例分析

下面给出一个电子刹车系统的案例分析。刹车系统由刹车踏板传感器，主控制器，刹车执行器组成，它们的UML结构图如图9所示。所需满足的CCSL表达式如表3所示。

5结束语

针对时间约束的验证工作还未得到统一，且时间约束难以进行形式化的分析。本文给出一种将CCSL规范的一部分转换为时间自动机来验证时间约束满足性的方法。通过CCSL基本元素与时间自动机基本元素之间语义的一致性，将CCSL元素映射为时间自动机元素，进而根据映射规则，给出时钟关系的时间自动机模板。最后给出一个实例分析验证方法的可行性和有效性。

在接下来的研究中，我们将进一步对完整的CCSL规范进行转换，并尝试给出语义一致性的证明，并给出一个简单可用的自动化转换工具来完善研究工作。

参考文献

[1]CHEN Huowang，WANG Ji，DONG Wei.High confidence software engineering technologies[J].Acta Electronica Sinica，2003，31（12A）：1933-1938.

[2]黄志球，徐丙凤，阚双龙，等.嵌入式机载软件安全性分析标准、方法及工具研究综述[J].软件学报，2014.25（2）：200-218.

[3]MARTE UML.UML profile for MARTE：modeling and analysis of realtime embedded systems[J].2015.

[4]ANDR C.Syntax and semantics of the clock constraint specification language （CCSL）[D].INRIA，2009.

[5]LARSEN K G，PETTERSSON P，YI W.UPPAAL in a nutshell[J].International Journal on Software Tools for Technology Transfer （STTT），1997，1（1）：134-152.

[6]GASCON R，MALLET F，DEANTONI J.Logical time and temporal logics：comparing UML MARTE/CCSL and PSL[C]//2011 Eighteenth International Symposium on Temporal Representation and Reasoning.IEEE，2011：141-148.

[7]MALLET F.Clock constraint specification language：specifying clock constraints with UML/MARTE[J].Innovations in Systems and Software Engineering，2008，4（3）：309-314.

[8]ANDR C.Syntax and Semantics of the Clock Constraint Specification Language （CCSL）[J].HALINRIA，2009.

[9]ALUR R DILL D L，A theory of timed automata[J].Theoretical Computer Science，1994.126（2）：183-235.

[10]ALUR R.Timed automata[C]//International Conference on Computer Aided Verification.Springer Berlin Heidelberg，1999：8-22.

[11]MALLET F，SIMONE R DCorrectness issues on MARTE/CCSL constraints[J].Science of Computer Programming，2015.106：78-92.endprint