基于时钟约束和信号约束的信息物理融合系统的建模、分析与验证

发布时间：2017-12-09 09:37

  本文关键词：基于时钟约束和信号约束的信息物理融合系统的建模、分析与验证

  更多相关文章： 信息物理融合系统 时钟约束 信号约束 模型检查 形式化验证 调度分析

【摘要】：信息物理融合系统(Cyber-Physical Systems, CPS)是一种通过融合计算、通信和控制与物理过程实现计算机世界与物理世界深度协作的复杂系统。相较于一般传统系统,信息物理融合系统具有以下突出特性：信息世界与物理世界的高度耦合、异构性、并发性、时间攸关性,以及要求较高的可预测性和安全性。这些特性带来了以下挑战：需要整合异构的计算通信模型,需要异构的时间模型以及时间模型与行为语义的融合,需要以分析、验证等手段保证系统具有较高的可预测性和安全性。本文提供针对这三大挑战,为信息物理融合系统提供建模、验证和调度性分析的支持,主要工作包括：·提出了针对信息物理融合系统特性的声明式建模语言-信号约束语言Signal Con-straint Modeling Language (SCML),以及使用SCML的建模方法。SCML的时间模型是异构的,包括逻辑时间和超稠密时间,支持逻辑时间、连续物理时间和离散物理时间的整合。在异构时间模型基础上,SCML提供多样的信号支持异构的行为的描述,包括连续动态行为、离散动态行为、实时行为和(非实时)逻辑行为。SCML还提供丰富的信号约束用于描述信号之间的关系,包括不同类型信号之间的交互和转换,并支持多种计算通信规则。SCML具有操作语义,在计算通信模型理论的基础上实现异构计算通信模型的整合以及异构时间与行为的融合。本文提出将SCML作为伴随约束语言与SysML并PUML-MARTE协作建模的方法,建模所得的SCML规约将为模型提供显式的形式化的行为语义,从而支持后续的形式化分析和验证。·提出了对建模所得的SCML规约进行调度分析的方法。为提高系统的可预测性和安全性,定义了要检查的属性,包括可采纳调度的条件、定性的调度分类和调度时间不敏感性、定量的调度衡量标准(例如调度成功率、错失率和平均响应时间)等,并识别出了这些属性在SCML规约的语境下的表现形式以及检查所需的信息。为表达以上内容,扩展了时钟约束语言Clock Constraint Specification Language(CCSL),引入了对时钟终结和物理时间的支持,得到了扩展的时钟约束语言eCCSL,并为eCCSL提供了基于状态的操作语义。给出了从SCML规约中提取检查属性所需信息的方法,并将其构成了eCCSL规约。根据eCCSL的语义,提供了使用模型检查器SPIN, NuSMV和UPPAAL检查eCCSL规约的以上属性的方法。为识别eCCSL规约的可采纳调度,定义了基于迁移的广义Buchi自动机及其语境下的可采纳调度的识别条件,给出了识别可采纳调度的算法。该算法还可以约简规约的状态空间,约简后的自动机的所有运行都能产生可采纳调度。分析了规约规定的时钟时刻的依赖关系,提供了算法探查导致规约调度失败的选择,当有其他选择时规避引发调度失败的选择。·提出了对建模所得的SCML规约进行形式化验证的方法。定义了针对系统可预测性和安全性进行验证要检查的属性,包括安全性和活性等通用属性、系统业务逻辑相关属性等,并识别出了这些属性在SCML规约的语境下的表现形式以及检查所需的信息。采用与调度分析时类似的方法,从SCML规约中提取所需信息、并将其构成eCCSL规约。将构建的eCCSL规约转换为了Promela模型和UPPAAL时间自动机,定义了用时序逻辑LTL和TCTL表达待检查属性,提供了观察者模版收集所需信息,利用模型检查器SPIN和UPPAAL实施了验证。为证明验证方法的正确性,定义了带检测点的标号迁移系统、基于动作和检测点的线性时态逻辑和基于检测点的互模拟关系,以此为基础给出了正确性的证明。本文将提出的方法应用于轨道交通领域,以智能交通控制系统在道口问题上的应用为案例,表明了提出的方法和过程的可行性与有效性。
【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP202
，

本文编号：1269944