智能系统是当前研究热点,在一些安全攸关的智能系统中,时间和空间信息需具有一致性,即在规定的时间到达规定的位置。为确保智能系统的时空一致性,需对系统的时间和空间信息进行规约。时钟通常有物理时钟和逻辑时钟两种类型,将两者融合在一起形成的混成时钟(Hybrid Clock)能够同时对物理时钟和逻辑时钟进行规约,其物理时钟包含了智能系统的空间与时间信息,规约了时空一致性。本论文构建混成时钟逻辑(Hybrid Clock Logic,HCL)系统对智能系统的时空性质进行规约,通过HCL模型检测验证系统的性质,保证系统的安全性与可靠性。具体研究内容如下:1.建立了混成时钟逻辑系统的语法结构。为了满足系统性质描述的需要,本文在已有混成时钟运算和关系的基础上提出了一些新的运算和关系,定义了HCL的语法,给出了具体的高铁实例对混成时钟运算和关系进行解释,并研究了混成时钟关系的相关性质。2.构建了混成时钟逻辑模型检测方法。首先,通过定义时空一致性规范语言STeC设计与HCL公式之间的可满足关系,给出了 HCL公式的语义;然后,基于STeC设计转换成的混成时钟进行模型检测,设计了 HCL模型检测算法;最后,通过高速铁路和航空航天领域的案例研究表明了 HCL的有效性和模型检测算法的正确性。3.设计开发了基于混成时钟逻辑系统的STeC模型检测工具。该工具可实现将STeC设计转换成混成时钟,并可对以HCL公式描述的系统性质进行验证,以高速铁路和航空航天案例表明了工具的可用性。