作者：苏琪; 王婷; 陈铁明; 陈蓉蓉时间自动机形式化方法安全验证建模
摘要：信息物理融合系统（cyber-physical system,CPS）作为一个新的研究方向,在其研究与发展过程中遇到了众多的问题,一些关于CPS安全的问题逐渐呈现.对CPS的设计安全进行探索性研究,主要针对CPS系统各部分之间如何安全地交互进行建模,并讨论安全数据的攻击及其防御措施的有效性.以网络化水位控制系统为例,以时间自动机为形式化建模语言对系统进行建模、验证和分析.建模过程中,采用分层的安全体系结构,分别将系统的各个组成部分的工作抽象为时间自动机模型.这些模型组成一个系统,刻画出完整的CPS工作过程.最后,利用模型检测工具PAT验证系统恢复机制的有效性.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
