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

安全关键的信息物理系统中时序行为的组合与精化陈博1李曦1,2周学海1,21（中国科学技术大学软件学院江苏苏州215123）2（中国科学技术大学计算机科学与技术学院合肥230051）（）Composition and Refinement of Timing Behavior in Safety-Critical CyberPhysical SystemsChenBo1,LiXi1,2,andZhouXuehai1,21（School of Software Engineering,University of Science and Technology of China,Suzhou,Jiangsu 215123）2（School of Computer Science and Technology,University of Science and Technology of China,Hefei 230051）AbstractCyber physical systems(CPS)are usually used in safety critical scenarios,which require real-timemonitoring,computethefeedbackdata,andrealizeautomaticcontrolandmanagementoftheexternalenvironment.Model driven development method is the main way to develop real-time and heterogeneous CPS,and thecomposabilityofthemodelisthekeypoint.Inthispaper,thetimingbehaviorspecificationmodelofthesystemisestablishedbytheclockconstraintspecificationlanguage(CCSL),andonthisbasis,thetimingbehaviorsemanticsofCCSLisdescribedbythetransitionsystems,anditscompositionoperationmethodandtheformaldefinitionofcomposability is given.Further,the timing behavior is refined,and the transformation method from the timingbehavior model of specification to the task execution model is given,The timing constraint behavior at thespecificationlevelistransformedintothetimingconstraintbehavioratthetasklevel.Atthesametime,themodelbehaviorislearnedbasedontheL*methodtorealizecompositionalverificationtoalleviatethestateexplosionproblem,andthecomposabilityoftherefinedmodelisverified.Finally,therefinementandverificationmethodsareevaluatedbysimulationexperimentsandthemaster-slaveintelligentvehicleexample.Therelevantdatashowsthat,therefinedmethodandcompositionalverificationmethodshavesomeperformanceadvantagesinprocessingtimeandmemoryconsumption.Key words cyber physical system(CPS)；clock constraint specification language(CCSL)；composiability ofcomponent；L*algorithm；refinementoftimingbehavior摘要信息物理系统（cyberphysicalsystems,CPS）通常被应用于安全关键的场景中，需要进行实时监控，并计算反馈信息，实现对外部环境的自动控制与管理.基于模型驱动的开发方法是针对实时的、异构的CPS 进行开发的，而模型的可组合性是其中的核心关键点.针对时序行为的可组合问题，首先通过时序约束语言（clockconstraintspecificationlanguage,CCSL）建立系统的时序行为需求模型，在此基础上通过迁移系统描述 CCSL 的时序行为语义，并给出其组合操作方法及可组合性的形式化定义.进一步地，对时序行为进行精化操作，给出从时序行为需求模型到任务执行模型的转换方法.同时，基于 L*方法对模型行为进行学习，实现组合验证以缓解状态爆炸问题，并验证精化后模型的可组合性.最后通过仿真实验及主从收稿日期：2022-01-09；修回日期：2022-10-12基金项目：国家自然科学基金项目（61772482）ThisworkwassupportedbytheNationalNaturalScienceFoundationofChina(61772482).计 算 机 研 究 与 发 展DOI：10.7544/issn1000-1239.202220041JournalofComputerResearchandDevelopment60（8）：18951911，2023智能小车实例对精化与验证方法进行评估.相关数据显示，精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.关键词信息物理系统；时序约束语言；组件的可组合性；L*算法；时序行为精化中图法分类号TP311.5信息物理系统（cyberphysicalsystems,CPS）通常是由多个组件（物理组件、计算组件等）组成的复杂信息系统1.其发展迅速，尤其在近年计算机系统中软硬件架构处理能力不断强化的加持下，使得 CPS迭代速度不断加快.比如某款汽车系统中包含由 200个供应商中提供的 70 多个ECU单元，且数量不断增加，同时预计内部软件系统代码量也将从 2005 年的几百行增长至 2025 年的 100 亿行，面对如此复杂庞大的系统，如何保证系统的正确性、安全性是类似 CPS开发过程所面临的主要问题.现今，基于构件的开发（component-baseddevelopment,CBD）方法成为该类系统主要的开发方式2.其具体过程如图 1 所描述，首先给出顶层规约（specification），再通过精化方法细化规约，最终得到具体实现（implementation）.因此，构建系统关键属性的行为模型，再利用精化与组合方法生成具体模型，最终对关键属性进行验证是 CBD 方法的核心内容.为了对安全攸关的CPS 进行设计开发，本文基于时序约束描述语言（clockconstraintspecificationlanguage,CCSL）对系统进行实现.具体地，本文主要贡献体现在 3 个方面：1）给出时序行为可组合的形式化定义.为了阐述时序行为的组合过程，通过迁移系统（transitionsystem,TS）描述时序约束语义，并在此基础上给出时序行为可组合的形式化定义.2）给出基于 L*学习的系统属性验证方法.通过分治策略对系统属性进行验证，有效解决模型组合后所带来的状态激增的问题.3）提出针对时序约束行为的逐步求精方法.主要针对 3 种典型的时序约束规约进行精化实现，给出任务结构的生成规则，能够将顶层的时序规约模型映射为操作系统中任务级的时序行为约束模型.1相关工作目前，在时序规约建模与精化等方面已有若干相关工作的开展3-4，本节将对其进行归纳和比较.1.1时间行为的组合与验证时序行为模型是安全攸关的 CPS 在设计与开发过程中需要构建的主要内容5.为了对系统的时序行为进行描述，国内外研究小组从系统的不同层次、不同角度对系统行为进行刻画.较为著名的研究如加州大学伯克利分校的 Eker 等人6从系统的异构计算模型（modelofcomputation,MOC）角度刻画组件行为，m1?m2?m3?m2!m1?m1?m1?m5?m4?m4!m2?m1?m3?m2!m5!m3!t2t3消费者未开始状态2start/generated_data()需求模型组件模型组件精化功能/非功能验证代码生成验证和确认时钟约束描述语言(CCSL)自动机模型时序行为精化时序行为验证void generated _data()for(int i=0;in，定义了时钟 m 的滴答次数要多于时钟 n 的滴答次数，或者交替语义（alternative）：mn，表达了时钟 m 和时陈博等：安全关键的信息物理系统中时序行为的组合与精化1897钟 n 会交替滴答产生的约束关系.CCSL 规约语言的核心要素是逻辑时钟，区别于能够度量物理时间的物理时钟，逻辑时钟可以看作是能够在设计阶段对系统中任务的时序关系进行表达的模型元素.本节首先描述一个逻辑时钟的概念，再扩展出系统中存在多个逻辑时钟的时间结构定义.定义 1.逻辑时钟.采用 5 个标签I,D,u结构来进行表达.标签 I 为一系列事件的发生时刻，为发生时刻序列 I 上的严格优先（strictprecedence），D是时钟上的记号，通过函数 进行定义：ID，u 是时钟递增幅度.针对逻辑时钟而言，递增幅度 u 可以是系统滴答 tick，也可以是总线的传输周期等.定义 2.时间结构.通过标签C,进行表达，在时间结构中，C 为包括逻辑时钟或度量时钟的时钟集合，为这组时钟上的先后约束关系.可以看出，逻辑时钟是一系列具有严格先后关系的时间点集合.通常用来描述某个事件在时间线上的一系列动作.2 个时钟之间最纯粹、最本质的关系是优先（precedence）.从最基本关系出发，可以推出其他时序关系，如同时发生（coincidence）、严格优先（strictprecedence）、互相排斥（exclusive）等.例 1.假设存在 2 个时钟 c 与 d，2 个时钟的关系为：时钟 c 与基准时钟延迟 1 个时间单位，并在之后以 4 为周期值进行执行（属于 subclock 子时钟约束的一种），而时钟 d 与基准时钟延迟 3 个时间单位，之后同样以 4 为周期值进行执行.通过 CCSL 语言进行描述可以得到的关系为：cisPeriodicOnclkperiod=4offset=1,disPeriodicOnclkperiod=4offset=3.在 CCSL 仿真工具 Timesquare 中对时序行为进行模拟得出的执行过程如图 2 所示.执行过程描述的 3 个逻辑时钟的时序约束关系为：首先逻辑时钟clk 滴答，在其后产生的是逻辑时钟 c 的滴答（offset=1），继而，逻辑时钟 c 以 4 为周期值进行滴答.逻辑时钟d 以逻辑时钟 clk 为基准，同样以 4 为周期值产生滴答，并且其偏移值为 3（offset=3）.01020Periodicitynewfile:main:clkPeriodicitynewfile:main:cPeriodicitynewfile:main:d时间Fig.2Diagramofclocksrelationship图2时钟的关系图 2.2时序约束行为的组合与可组合性定义在系统开发过程中需要对时序行为进行建模及分析，本文依据文献 27 所给方法通过迁移系统来刻画 CCSL，并采用组合推理方式对属性进行检查.A定义 3.时钟迁移系统