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

项目名称： 扩展的线性时段不变式的模型检验

项目编号： No.61472279

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 张苗苗

作者单位： 同济大学

项目金额： 78万元

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

中文关键词： 模型检验；时段演算；线性时段不变式；实时系统；时态逻辑

英文摘要： 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.

英文关键词： model checking;duration calculus;linear duration invariants;real time system;temporal logic