基于时空自动机的CPS建模与验证

为了描述信息物理融合系统(cyber-physical systems,CPS)的时空一致性,一种实时规范语言STe C已经提出[1],CPS的设计和实现能否满足时空一致性显得十分重要。文中对混成自动机进行了扩展,提出了具有位置驱动特点的时空自动机。文中提出了基于时空自动机的CPS建模与验证框架。在框架中,首先使用STe C语言对CPS进行了描述并使用时空自动机对CPS进行建模。文中采用的形式化验证方法为微分动态逻辑(differential dynamic logic,DL),其操作模型为HP(hybrid program)。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的CPS属性进行规约,最后使用定理证明器Ke Ymaera对属性进行自动化验证。

基于时空I/O混成自动机的物联网服务验证

物联网服务的建模和验证是物联网研究中的重要问题。文中对混成自动机进行了扩展,提出了具有位置驱动特点的时空I/O混成自动机。文中提出了基于时空I/O混成自动机的物联网服务建模与验证框架。在框架中,首先对物联网服务进行了描述,并使用时空I/O混成自动机对物联网服务进行建模。这些时空I/O混成自动机形成一个网络,刻画完整的物联网服务的通信并行过程。文中采用的形式化验证方法为微分动态逻辑(Differential Dynamic Logic,DL),其操作模型为HP(Hybrid Program)。利用DL可以将所建模型转换为对应的HP。结合得到的HP对验证的物联网服务性质进行规约,最后使用定理证明器KeYmaera验证物联网服务的正确性。

一种离散连续混成的时空事件驱动的CPS体系架构

为描述信息物理融合系统(cyber-physical system,CPS)中离散信息系统和连续物理系统交互融合的混成特性,基于混成自动机理论,结合多智能体系统(multi-agent system,MAS)和时空事件驱动方法,提出一种CPS体系架构.该架构用改进的混成自动机理论刻画了离散空间和连续状态混成的CPS体系架构的主体,同时定义了基于时空事件的CPS事件,设计了基于MAS的CPS端,并运用定义不同功能的CPS端和CPS事件驱动机制解析了CPS体系架构内部信息物理交互反馈过程.最后以车速调控系统为例,采用提出的CPS体系架构分析了协同驾驶过程中单一车辆内部速度调控的信息物理融合过程,并对其进行了形式化描述,实例的形式化过程表明提出的体系架构的有效性.构建的CPS体系架构为刻画CPS的本质特征提供了新的方法.