扩展的线性时段不变式的模型检验

Extended linear duration invariants(ELDI) form an important subset of Duration Calculus(DC), as many interval and safety properties of real-time systems can be defined with them. However, due to the undecidablility of decision problems of ELDI both in the discrete time and continuous time,there still exists unsolved theoretical problems of checking ELDI. In addition, there is a big gap between the theory and application. Therefore based on the technique developed in our previous work, we will focus on model checking ELDI in this project. The aim of the project is to be achieved by carrying out the following reseach topics. 1) In the context of the standard discrete time semantics, put forward inverse idea to optimize our algorithm that has been developed to handle the problem of bounded model checking of ELDI. This work consists of a) constructing an inverse property for a subset of ELDI with the "chop" modality and conjunction operator, b) designing a modelling algorithm to automatically acquire the inverse timed automaton A' of the former systems A, and c) proving the checking equivalency of A and A' and extending the inverse idea to deal with other formulae. 2) In the context of the standard continuous time semantics, design the bounded model checking algorithms of ELDI. This work is further divided into designing a) a checking algorithm of the ELDI with only one "chop" modality, and b) a checking algorithm of the ELDI with several "chop" modalities and boolean operators. 3) In the context of the standard discrete time semantics and unbounded observation interval, design the checking algorithms of ELDI. We need to investigate a) a checking algorithm of the ELDI with only one "chop" modality, and b) a checking algorithm of the ELDI with several "chop" modalities and boolean operators. 4) Develop a checking tool that can be integrated with UPPAAL and demonstrate the efficiency of the designed algorithms by some industrial examples.

扩展的线性时段不变式（ELDI）是时段演算中描述系统区间性质的一类重要公式，然而因ELDI的决策问题在离散和连续时间下是不可判定的，对ELDI的模型检验仍然存在许多待解决的理论问题且与实际应用还有一定差距。因此本项目将主要致力于解决ELDI的模型检验，主要研究内容有：1)优化离散时间语义下ELDI的有界模型检验算法，包括a）研究一类带有"切变"和"与"运算符结合的ELDI性质的反转；b) 研究原系统自动机A的反转自动机A'；c)验证结果的等价性和反向思想的扩展。2）连续时间语义下ELDI的有界模型检验算法，包括a)只含有一个"切变"运算的检验；b)含有多个"切变"运算以及和逻辑运算符结合的检验。3）离散时间语义下无界观测区间的ELDI的模型检验算法，包括a)带有单个切变运算符的检验算法；b) 带有多个切变运算符以及与其他逻辑运算符结合的检验算法。4）模型检验的工具实现以及具体工业实例分析。

在标准离散时间语义和连续时间语义下，我们研究扩展的现行时段不变式 (ELDI) 的有界和无界模型检验。 同时, 我们还研究了凸二分图动态匹配、混合系统验证以及实时自动机的不透明度和模型学习等相关问题。发表了8篇较高水平论文，目前培养博士2名和硕士8名。主要研究成果如下：.1. 基于时间自动机的连续时间ELDI的有界模型检验.ELDI的模型检查问题在标准连续时间和离散时间语义方面都是不可判定的，我们证明这个问题在连续时间语义中仍然是可判定的。方法主要是通过转化为量词线性实算术公式（QLRA）并求解来实现。一些示例说明了我们的方法的效率。.2. 基于实时自动机的连续时段演算的验证.我们将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题，从而可以采用量词消去技术进行求解。降低了验证复杂度并且加速了验证过程的实际速度。.3. 凸二分图动态匹配问题的解决.研究两种带权凸二分图中动态权值匹配问题，以及提高凸二分图动态基数匹配问题中查询操作的效率。.1）提出了一个解决二分图动态匹配问题的方法框架。2）解决左侧顶点带权凸二分图动态权值匹配问题 3）解决两侧顶点带权凸二分图动态权值匹配.4. 基于证明的使用微分不变量的混合系统开发方法.从混合系统连续行为的建模方法、连续行为模型的证明义务规则、证明技术、证明工具等四个方面进行了研究，提出了一种基于Event-B框架的混合系统开发方法。.5. 设计基于屏障证书的相连混成系统的安全性验证.我们提出了一个数值方法验证互联混合动力系统的约束状态的安全性。该方法是一种数值方法，状态约束基于双线性平方和规划。可以验证互联混合系统的安全性。.6. 实时自动机的学习 （论文已投）.我们提出了一种在连续时间语义和离散时间语义上的确定性实时自动机（DRTA）的主动学习算法。 对于一个由DRTA A能识别的目标语言，我们将学习DRTA A的问题转化为正交实时自动机A’的学习，并且 L（A'）= L（A）。.7. 实时自动机的不透明性.研究了实时自动机（RTA）的不透明度问题，这是一种用于实时系统的模型。证明RTA的语言不透明问题是可判定的。.8. ELDI模型检验工具和模型学习软件实现