电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2012年
6期
1126-1132
,共7页
朱敏%李必信%陈乔乔%吉顺慧%李加凯
硃敏%李必信%陳喬喬%吉順慧%李加凱
주민%리필신%진교교%길순혜%리가개
信息物理融合系统%微分动态逻辑%HybridUML%模型转换%验证
信息物理融閤繫統%微分動態邏輯%HybridUML%模型轉換%驗證
신식물리융합계통%미분동태라집%HybridUML%모형전환%험증
随着信息物理融合系统(Cyber-Physical Systems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Logic),其操作模型为hybrid program.将HyhridUML模型转换为hybrid program时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybrid program对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.
隨著信息物理融閤繫統(Cyber-Physical Systems,CPS)應用的越來越普及,CPS的設計和實現能否滿足實際需求顯得至關重要.本文提齣瞭一種CPS建模與屬性驗證框架.在框架中,首先使用HybridUML對CPS進行建模,然後將該通用模型轉換為形式化模型,進而進行形式化驗證.本文採用的形式化驗證方法為dL(Differential Dynamic Logic),其操作模型為hybrid program.將HyhridUML模型轉換為hybrid program時,基于語義一緻性的原則定義轉換規則.轉換完成後,結閤得到的hybrid program對驗證的CPS屬性進行規約,最後使用定理證明器KeYmaera對屬性進行自動化驗證.
수착신식물리융합계통(Cyber-Physical Systems,CPS)응용적월래월보급,CPS적설계화실현능부만족실제수구현득지관중요.본문제출료일충CPS건모여속성험증광가.재광가중,수선사용HybridUML대CPS진행건모,연후장해통용모형전환위형식화모형,진이진행형식화험증.본문채용적형식화험증방법위dL(Differential Dynamic Logic),기조작모형위hybrid program.장HyhridUML모형전환위hybrid program시,기우어의일치성적원칙정의전환규칙.전환완성후,결합득도적hybrid program대험증적CPS속성진행규약,최후사용정리증명기KeYmaera대속성진행자동화험증.
