科技通报
科技通報
과기통보
BULLETIN OF SCIENCE AND TECHNOLOGY
2015年
1期
94-99
,共6页
时空自动机%CPS%微分动态逻辑%时空一致性%验证%KeYmaera
時空自動機%CPS%微分動態邏輯%時空一緻性%驗證%KeYmaera
시공자동궤%CPS%미분동태라집%시공일치성%험증%KeYmaera
spatial hybrid automata%CPS%differential dynamic logic%spatial-temporal consistence%verification%KeYmaera
为了描述信息物理融合系统（cyber-physical systems，CPS）的时空一致性，一种实时规范语言STeC已经提出[1]，CPS的设计和实现能否满足时空一致性显得十分重要。文中对混成自动机进行了扩展，提出了具有位置驱动特点的时空自动机。文中提出了基于时空自动机的CPS建模与验证框架。在框架中，首先使用STeC语言对CPS进行了描述并使用时空自动机对CPS进行建模。文中采用的形式化验证方法为微分动态逻辑（differential dynamic logic，DL），其操作模型为HP（hybrid program）。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的CPS属性进行规约，最后使用定理证明器KeYmaera对属性进行自动化验证。
為瞭描述信息物理融閤繫統（cyber-physical systems，CPS）的時空一緻性，一種實時規範語言STeC已經提齣[1]，CPS的設計和實現能否滿足時空一緻性顯得十分重要。文中對混成自動機進行瞭擴展，提齣瞭具有位置驅動特點的時空自動機。文中提齣瞭基于時空自動機的CPS建模與驗證框架。在框架中，首先使用STeC語言對CPS進行瞭描述併使用時空自動機對CPS進行建模。文中採用的形式化驗證方法為微分動態邏輯（differential dynamic logic，DL），其操作模型為HP（hybrid program）。利用DL可以將所建模型轉換為對應的HP。結閤得到的HP對驗證的CPS屬性進行規約，最後使用定理證明器KeYmaera對屬性進行自動化驗證。
위료묘술신식물리융합계통（cyber-physical systems，CPS）적시공일치성，일충실시규범어언STeC이경제출[1]，CPS적설계화실현능부만족시공일치성현득십분중요。문중대혼성자동궤진행료확전，제출료구유위치구동특점적시공자동궤。문중제출료기우시공자동궤적CPS건모여험증광가。재광가중，수선사용STeC어언대CPS진행료묘술병사용시공자동궤대CPS진행건모。문중채용적형식화험증방법위미분동태라집（differential dynamic logic，DL），기조작모형위HP（hybrid program）。이용DL가이장소건모형전환위대응적HP。결합득도적HP대험증적CPS속성진행규약，최후사용정리증명기KeYmaera대속성진행자동화험증。
In order to describe the requirement of spatial and temporal consistence of cyber-physical systems (CPS), a specification language called STeC was proposed by Chen [1]. It is of vital importance to ensure that the design and implementation of CPS meet the requirement of spatial and temporal consistence. The Spatial Hybrid Automata (SHA), characteristic of the location-triggered, is proposed based on the extended hybrid automata. This paper presents a framework of CPS modeling and verification based on SHA, where CPS are described by STeC and modeled by SHA. The adopted formal method is the differential dynamic logic (DL), whose the operational model is Hybrid Program (HP). The SHA model is transformed to its corresponding HP through DL. Then CPS properties are specified based on the result from HP. Finally, the CPS properties are automatically verified through the theorem-prover named KeYmaera.
