软件形式化方法已经在工业领域得到广泛应用,形式化方法已成为提高软件可信性的重要手段。但是在CPS中,软件的体系结构会随着需求和环境而动态变化,不仅需要满足功能性要求,还要求时间等非功能属性具有可信性。如何精确地描述与验证CPS软件系统,目前国内外还没有一种统一的、成熟的建模和验证方法。CPS可信属性研究的难点在于如何精确地描述软件系统、如何从软件需求场景中抽取系统规范、如何高效地对系统进行模型检测。从而在系统设计的早期阶段尽早发现软件潜在的错误,及时纠正软件需求和系统设计中的不一致性和不完备性等问题,提高CPS软件的可信性。本文立足于CPS软件可信属性的建模与验证问题,旨在建立基于模型驱动的CPS软件时间可信属性的建模与验证集成框架,提出适合于CPS环境的软件时间可信属性的建模和验证方法。利用Object-Z语言的形式化优点描述模型的静态语义,利用PTA在时间约束和转移概率方面的优点描述模型的动态语义,建立软件的时间可信模型。采用基于场景的语言进行需求分析,进而抽取需求规范。针对CPS软件的时间可信属性,设计模型检测算法。本文从软件模型、需求规范、模型检测三方面进行了深入地探索研究,研究工作的主要创新性成果如下:(1)为了精确地描述CPS软件的功能属性和实时性等非功能属性,本文研究了软件的图形化模型和形式化建模方法。建立软件系统的图形化模型,有利于客户与软件开发人员形成共识,同时也能够有效地减低软件开发的复杂度,但是图形化模型不便于软件的形式化验证。因此,一方面充分利用MARTE在建立时间模型等非功能属性方面的图形化优势,另一方面研究融合静态结构和动态行为的形式化集成模型。在MDA框架下,设计了MARTE静态结构到Object-Z类、MARTE动态行为到PTA表达式之间的映射规则,提出了集成的的形式化建模方法PTA-OZ,该方法能够对MARTE建立的软件模型,进行静态结构验证和动态行为验证,从而能够利用形式化方法验证图形化建模语言建立的模型。在理论上,采用不变式和三元元模型相结合的方法,对模型转换的语义一致性进行了验证。并在Papyrus环境中,基于XMI实现了该转换框架。实验分析表明,该方法能够将图形化模型转化为形式化模型,并能够对转换后的CPS软件的功能属性和实时性等非功能属性进行有效地检验。(2)为了准确地描述软件需求,自动抽取属性公式。本文引入时钟和时间约束的形式化定义,定义了LSC图的时间属性模型,提出了TLSC到时序逻辑公式的转换规则,并给出了优化公式的方法。从基于场景的LSC语言出发,来描述CPS的软件需求。由于时间对于CPS软件的系统行为具有不容忽视的影响,需要关注于时间敏感的LSC图属性问题。通过引入时钟和时间约束的形式化定义,提出了TLSC图,研究了基于场景语言在描述软件需求时的时间属性问题。采用形式化的方式定义了TLSC图的语法和语义,以利于转换为时序逻辑公式。通过设计的基本规则和组合规则,实现了TLSC图到时序逻辑公式的转换;为了简化公式规模,利用传递性重新定义时间次序关系,进一步研究了公式优化的方法,使得公式规模有效地降低。最后,设计并完成了TLSC图到时序逻辑公式转换系统,从而实现了从需求场景中自动抽取逻辑公式。该方法适合于描述实时软件系统的属性和行为,能够从TLSC建立的软件需求规范中,自动抽取逻辑公式,并进行优化,初步解决了模型检验中逻辑公式的自动抽取问题。(3)为了准确地计算有界模型检测的完备性阈值,首次将半张量积理论引入到有界模型检测中,提出了基于半张量积的完备性阈值求解方法。采用离散时间进化系统来研究Kripke模型的状态进化拓扑结构,首先,通过Kripke模型解析算法,建立布尔函数的代数形式,并将其转换为逻辑形式。其次,通过固定点求解算法和k-loop求解算法,计算布尔网络中的吸引子。最后,根据吸引子计算固定点的位置、环路的长度以及环路的状态集等参数。采用经典数学理论中的矩阵分析方法来求解Kripke模型的前向半径,作为Kripke模型的完备性阈值。相比于以往的阈值计算方法,本文方法充分运用半张量积理论,利用代数运算代替逻辑运算,计算方法简单。(4)为了提高有界模型检测的效率,提出面向CPS时间可信属性的有界模型检测算法。充分考虑基于SAT方法编码中时间属性的缺失问题,对于CPS实时系统的时序逻辑公式,提出了基于SMT的RTECTL公式的有界模型检测算法,在命题公式的编码过程中,保留了公式中的时间属性。在逻辑公式路径的选择上,提出了基于优化的路径量词选择方法,具有减少路径数目的优点,并在理论上证明了该编码方法的可行性。