![点击分享此内容可以赚币 分享](/master/images/share_but.png)
安全关键的信息物理系统中时序行为的组合与精化.pdf
《安全关键的信息物理系统中时序行为的组合与精化.pdf》由会员分享,可在线阅读,更多相关《安全关键的信息物理系统中时序行为的组合与精化.pdf(17页珍藏版)》请在咨信网上搜索。
1、安全关键的信息物理系统中时序行为的组合与精化陈博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,Jian
2、gsu 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,andrealizeautomaticcontrolandmanagementoftheexte
3、rnalenvironment.Model driven development method is the main way to develop real-time and heterogeneous CPS,and thecomposabilityofthemodelisthekeypoint.Inthispaper,thetimingbehaviorspecificationmodelofthesystemisestablishedbytheclockconstraintspecificationlanguage(CCSL),andonthisbasis,thetimingbehavi
4、orsemanticsofCCSLisdescribedbythetransitionsystems,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 constr
5、aint behavior at thespecificationlevelistransformedintothetimingconstraintbehavioratthetasklevel.Atthesametime,themodelbehaviorislearnedbasedontheL*methodtorealizecompositionalverificationtoalleviatethestateexplosionproblem,andthecomposabilityoftherefinedmodelisverified.Finally,therefinementandverif
6、icationmethodsareevaluatedbysimulationexperimentsandthemaster-slaveintelligentvehicleexample.Therelevantdatashowsthat,therefinedmethodandcompositionalverificationmethodshavesomeperformanceadvantagesinprocessingtimeandmemoryconsumption.Key words cyber physical system(CPS);clock constraint specificati
7、on language(CCSL);composiability ofcomponent;L*algorithm;refinementoftimingbehavior摘要信息物理系统(cyberphysicalsystems,CPS)通常被应用于安全关键的场景中,需要进行实时监控,并计算反馈信息,实现对外部环境的自动控制与管理.基于模型驱动的开发方法是针对实时的、异构的CPS 进行开发的,而模型的可组合性是其中的核心关键点.针对时序行为的可组合问题,首先通过时序约束语言(clockconstraintspecificationlanguage,CCSL)建立系统的时序行为需求模型,在此基础上通
8、过迁移系统描述 CCSL 的时序行为语义,并给出其组合操作方法及可组合性的形式化定义.进一步地,对时序行为进行精化操作,给出从时序行为需求模型到任务执行模型的转换方法.同时,基于 L*方法对模型行为进行学习,实现组合验证以缓解状态爆炸问题,并验证精化后模型的可组合性.最后通过仿真实验及主从收稿日期:2022-01-09;修回日期:2022-10-12基金项目:国家自然科学基金项目(61772482)ThisworkwassupportedbytheNationalNaturalScienceFoundationofChina(61772482).计 算 机 研 究 与 发 展DOI:10.75
9、44/issn1000-1239.202220041JournalofComputerResearchandDevelopment60(8):18951911,2023智能小车实例对精化与验证方法进行评估.相关数据显示,精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.关键词信息物理系统;时序约束语言;组件的可组合性;L*算法;时序行为精化中图法分类号TP311.5信息物理系统(cyberphysicalsystems,CPS)通常是由多个组件(物理组件、计算组件等)组成的复杂信息系统1.其发展迅速,尤其在近年计算机系统中软硬件架构处理能力不断强化的加持下,使得 CPS迭代速度不断加
10、快.比如某款汽车系统中包含由 200个供应商中提供的 70 多个ECU单元,且数量不断增加,同时预计内部软件系统代码量也将从 2005 年的几百行增长至 2025 年的 100 亿行,面对如此复杂庞大的系统,如何保证系统的正确性、安全性是类似 CPS开发过程所面临的主要问题.现今,基于构件的开发(component-baseddevelopment,CBD)方法成为该类系统主要的开发方式2.其具体过程如图 1 所描述,首先给出顶层规约(specification),再通过精化方法细化规约,最终得到具体实现(implementation).因此,构建系统关键属性的行为模型,再利用精化与组合方法生
11、成具体模型,最终对关键属性进行验证是 CBD 方法的核心内容.为了对安全攸关的CPS 进行设计开发,本文基于时序约束描述语言(clockconstraintspecificationlanguage,CCSL)对系统进行实现.具体地,本文主要贡献体现在 3 个方面:1)给出时序行为可组合的形式化定义.为了阐述时序行为的组合过程,通过迁移系统(transitionsystem,TS)描述时序约束语义,并在此基础上给出时序行为可组合的形式化定义.2)给出基于 L*学习的系统属性验证方法.通过分治策略对系统属性进行验证,有效解决模型组合后所带来的状态激增的问题.3)提出针对时序约束行为的逐步求精方法
12、.主要针对 3 种典型的时序约束规约进行精化实现,给出任务结构的生成规则,能够将顶层的时序规约模型映射为操作系统中任务级的时序行为约束模型.1相关工作目前,在时序规约建模与精化等方面已有若干相关工作的开展3-4,本节将对其进行归纳和比较.1.1时间行为的组合与验证时序行为模型是安全攸关的 CPS 在设计与开发过程中需要构建的主要内容5.为了对系统的时序行为进行描述,国内外研究小组从系统的不同层次、不同角度对系统行为进行刻画.较为著名的研究如加州大学伯克利分校的 Eker 等人6从系统的异构计算模型(modelofcomputation,MOC)角度刻画组件行为,m1?m2?m3?m2!m1?m
13、1?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 规约语言的核心要素是逻辑时钟,区别于能够度量物理
14、时间的物理时钟,逻辑时钟可以看作是能够在设计阶段对系统中任务的时序关系进行表达的模型元素.本节首先描述一个逻辑时钟的概念,再扩展出系统中存在多个逻辑时钟的时间结构定义.定义 1.逻辑时钟.采用 5 个标签I,D,u结构来进行表达.标签 I 为一系列事件的发生时刻,为发生时刻序列 I 上的严格优先(strictprecedence),D是时钟上的记号,通过函数 进行定义:ID,u 是时钟递增幅度.针对逻辑时钟而言,递增幅度 u 可以是系统滴答 tick,也可以是总线的传输周期等.定义 2.时间结构.通过标签C,进行表达,在时间结构中,C 为包括逻辑时钟或度量时钟的时钟集合,为这组时钟上的先后约束
15、关系.可以看出,逻辑时钟是一系列具有严格先后关系的时间点集合.通常用来描述某个事件在时间线上的一系列动作.2 个时钟之间最纯粹、最本质的关系是优先(precedence).从最基本关系出发,可以推出其他时序关系,如同时发生(coincidence)、严格优先(strictprecedence)、互相排斥(exclusive)等.例 1.假设存在 2 个时钟 c 与 d,2 个时钟的关系为:时钟 c 与基准时钟延迟 1 个时间单位,并在之后以 4 为周期值进行执行(属于 subclock 子时钟约束的一种),而时钟 d 与基准时钟延迟 3 个时间单位,之后同样以 4 为周期值进行执行.通过 CC
16、SL 语言进行描述可以得到的关系为:cisPeriodicOnclkperiod=4offset=1,disPeriodicOnclkperiod=4offset=3.在 CCSL 仿真工具 Timesquare 中对时序行为进行模拟得出的执行过程如图 2 所示.执行过程描述的 3 个逻辑时钟的时序约束关系为:首先逻辑时钟clk 滴答,在其后产生的是逻辑时钟 c 的滴答(offset=1),继而,逻辑时钟 c 以 4 为周期值进行滴答.逻辑时钟d 以逻辑时钟 clk 为基准,同样以 4 为周期值产生滴答,并且其偏移值为 3(offset=3).01020Periodicitynewfile:m
17、ain:clkPeriodicitynewfile:main:cPeriodicitynewfile:main:d时间Fig.2Diagramofclocksrelationship图2时钟的关系图 2.2时序约束行为的组合与可组合性定义在系统开发过程中需要对时序行为进行建模及分析,本文依据文献 27 所给方法通过迁移系统来刻画 CCSL,并采用组合推理方式对属性进行检查.A定义 3.时钟迁移系统27.可以通过一个在事件集A 上的五元组=(S,Tran)进行表达,其中:1)S 为一组状态节点,s0是初始节点;2)TranA 定义节点转换过程中对应的事件;3),TranS 是映射函数,节点转换中
18、的起点和终点的节点;4)TranS2S是描述转移集合是节点之间转换关系的子集,当事件 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)是子时
19、钟关系(nissubclockofm).m m,n,m m,n(a)时钟m行为(b)时钟m=n行为(c)时钟nm Fig.3Clocktickingbehaviors图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),.clk=3c=1,d=0/clk=1c=0,d=1/clk=0Fig.4Relations
20、hipdiagramoftimingconstraintbasedonstatetransition图4基于状态迁移的时序约束关系图在能够表达一个时钟的执行过程后,需要对系统中存在的多个时钟的约束行为关系进行组合来描1898计算机研究与发展2023,60(8)述整体,最直观的方法是计算多个时钟的笛卡儿积.定义 4.时钟约束行为的组合.对于 n 个逻辑时钟 A1,A2,An,其同步行为是 A1A2An的一个子集合 I,则多个时钟的约束行为组合可以描述为在动作子集 IA1A2 An上的时钟迁移系统 A=(S,Tran),其中:1)S=S1S2Sn,系统的全部状态;2)(t1,t2,tn)=(t1)
21、,(t2),(tn),转移过程的事件行为;3)(t1,t2,tn)=(t1),(t2),(tn),转移过程的起始状态节点;4)(t1,t2,tn)=(t1),(t2),(tn),一次转移过程的目的状态节点;5)Tran=t1,t2,tnT1T2 Tn|1(t1),2(t2),n(tn)I,是所有的转移行为.定义 5.禁止状态.2 个系统 M 与 N 的乘积为 APAQ,其禁止状态节点 Forbidden(M,N)SMSN应具有属性:Forbidden(M,N)=(v,u)SMSN|a shared(M,N),a AM(v)a AN(u)a AN(v)a AM(u).其中 AM(v)与 AN(v
22、)是系统 M 与系统 N 在组合后所得到的状态 v 下所接受的事件集合.shared(M,N)表示M 与 N 之间的共有动作.基于定义 5,组件组合后,当处于禁止状态下,M 对事件 e 有转移发生,而 N 对事件 e 没有转移发生,或两者情况彼此相反,即,在禁止状态下,不能在同一时刻使得 M 与 N 一起产生转移,称为禁止状态节点.定义 6.时序行为可组合.如果 M 和 N 有一个外部系统 E,可以保证 M 和 N 在组合后禁止状态节点不可达,可得 M 和 N 是时序行为可组合的.行为可组合的定义描述了系统在组合后的执行行为并没有改变原系统的执行行为,确保了系统在集成前与集成后行为的一致性.基
23、于这个基本检查形式,可以对系统的行为进行笛卡儿积的计算,并在此基础上进行模型检查.本文给出图 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)模型不能
24、接受的.因此,组件进行组合后有可能进入非法状态 Err,导致系统错误.因此组件是不可组合的.简单而言,在组件组合后的状态集合中,某状态并不是所有组件都希望到达的,则该状态称为禁止状态.s0s2s4s5s3wirtenokfailokreplace123observe,write,okexec observewritereplace incorrectwritenok okincorrectreplaceexec(a)数据采集端(b)控制端3,s33,s43,s22,s11,s12,s5Errobservewriteexecoknokreplaceincorrect(c)数据采集端和控制端的组合
25、行为 Fig.5Systembehaviormodel图5系统行为模型本文将组件时序行为的可组合性描述为各个组件的时序行为在合并之后,如果能够满足组件原有的时序行为约束要求,则可以定义为时序行为可组合的.如图 6 所示,系统给出了外部环境的执行过程,外部环境读入 exec 后,执行内部动作 check,最后输出 ok 告知系统结果.上述过程没有时钟 incorrect 滴答.可以看出,能够存在一个子系统使得整体系统在组合后没有进入 Err 节点,则表明系统整体行为约束是具有可组合性的.101112execcheckokFig.6Alegalexternalenvironment图6一个合法的外
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 安全 关键 信息 物理 系统 时序 行为 组合
![提示](https://www.zixin.com.cn/images/bang_tan.gif)
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。