面向CPS时间属性的软件可信建模与验证方法研究

摘要

软件形式化方法已经在工业领域得到广泛应用，形式化方法已成为提高软件可信性的重要手段。但是在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公式的有界模型检测算法，在命题公式的编码过程中，保留了公式中的时间属性。在逻辑公式路径的选择上，提出了基于优化的路径量词选择方法，具有减少路径数目的优点，并在理论上证明了该编码方法的可行性。

目录

第一个书签之前