构建度量区间时序逻辑的时间自动机
文献类型：学位论文
| 作者 | 王勤思 |
| 学位类别 | 硕士 |
| 答辩日期 | 2010-06-03 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 北京 |
| 导师 | 李广元 |
| 关键词 | 模型检测 实时时序逻辑 度量区时序逻辑 基于迁移的扩展时间Büchi自动机 Tableau方法。 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 实时系统的安全性至关重要，使用模型检测工具对其进行形式化分析是提高 其安全性的重要手段。我们已有的实时系统模型检测工具CTAV 目前可以验证 LTL 描述的性质。本文工作的最终目的是让CTAV 能够验证实时时序逻辑，即， 使得CTAV 同样可以直接验证由实时时序逻辑描述的连续时间域上的实时性质。 度量区间时序逻辑MITL 是常用的一种关于实时系统的性质规范语言。已有 不少文献讨论过MITL 到时间Büchi 自动机的转换，但由于过程较复杂，大多数 仅限于理论研究，并没有与时间Büchi 自动机的空性判定过程结合成为一个可用 的关于MITL 的模型检测工具。 为了开发可用的关于MITL 性质的模型检测工具，本文采用与CTAV 中待验 证系统模型一致的pointwise 语义模型，选取了MITL 的一个可以较高效的进行模型检测的子类——MITL≤/<。在表达能力方面，这个子集能够描述实时系统模 型检测实际过程中常见的实时性质。 本文给出了将MITL≤/<公式转化为等价的基于迁移的扩展时间Büchi 自动机 的算法过程，并讨论了转化中逻辑公式重写规则的正确性和完备性问题。基于迁 移的扩展时间Büchi 自动机是时间Büchi 自动机的一种变体。二者最主要的区别在于它们采用了不同类型的Büchi 接受条件。文中给出的构造算法是将原先应用于非实时领域的Tableau 方法扩展调整，并应用于实时连续领域。Tableau 方法的关键之一是公式重写规则。而为了保证结果自动机仅存在有限多个状态，在重写规则中定义不动子公式是至关重要的。本文给出的在pointwise 语义模型下的公式重写规则，借用了此前在continuous 语义模型下已有的将时钟变量作为时序算子的约束直接引入公式中来保证重写规则中存在不动子公式的思想，并对其进行了修改，使原先性质自动机的时钟递减变为时钟递增，与系统自动机中的时钟行走方式一致。这省去了下一步将性质自动机和系统自动机相乘判空时，因为时钟行走方式不一致而引起的麻烦。另外，本文将MITL≤/<中的某些公式扩展为包含时钟约束的新的公式。这样，在定义重写公式时，不仅保证重写规则中存在不动子公式，也保证结果自动的前进性。 本文还根据构造算法实现了转化工具MITLCon。与Marc Geilen 和Dennis Dames 实现的逻辑转化工具相比，MITLCon 显著地减少了结果自动机节点和迁 移的数量，从而降低了结果自动机的大小，有利于进一步的模型检测过程。 |
| 英文摘要 | The security of real-time systems is of vital importance, and can be improved through the formal analysis adopting model checkers. Our existing tool – CTAV – can model check real-time systems against Linear Temporal Logic (LTL). In real-time domain, LTL can only present properties based on discrete time domain. Our ultimate goal is to enable CTAV to check real-time systems against real-time temporal logics which can describe properties based on continuous time domain. Metric Interval Temporal Logic (MITL), as a kind of real-time temporal logics, is widely adopted to depict real-time properties. There were some researches discussing how to translate MITL formulae into Timed Büchi Automata. However, due to the complex procedure, most of these work stayed on the theoretical level. Until now, there has not been a tool which can construct Timed Büchi Automata for MITL formulae and offer a functional interface to model checkers using emptiness decision methods to verify real-time systems. During the developing process of such a tool, the pointwise modeling semantics is adopted. We pick up a subclass of MITL – MITL≤/<. Compared with the whole class of MITL, its complexity of model checking is much lower. And, in terms of expressiveness, this subclass can describe common real-time requirements which would be encountered during the practical procedures of model checking real-time systems. Moreover, in this paper, an algorithm translating MITL≤/< formulae into equivalent Timed Transition-based Generalized Büchi Automata, and the correctness of this algorithm are also discussed. Timed Transition-based Generalized Büchi Automata is a variant of Timed Büchi Automata. The main difference between these two formalisms is that they adopt distinct kinds of Büchi acceptance condition. The construction algorithm extends the tableau construction method, which is widely used in discrete time domain, into the method that can also apply to construction in continuous time domain. The key of the tableau method is how to define the rewriting rules for logic formulae. In order to promise that the result automaton of a formula only has finite locations, it is essential to find the fixed sub-formula correctly. The rewriting rules given in this paper borrows a previous idea, under continuous modeling semantics, that clock variables are introduced into logic formulae as the constraints added to temporal operators directly and modifies this idea. The modification let the progression manner of clocks in property automata be consistent with that in system automata, which can avert the troubles aroused by disaccord progression manners of clocks during the next step of model checking. Additionally, a novel idea of how to extend the logic formulae to guarantee the progression of automata is promoted. Finally, a translator MITLCon is implemented according to the algorithm mentioned in this paper. Compared with Marc Geilen and Dennis Dames’, the number of both locations and transitions of the result automaton are significantly reduced. This will benefits the whole process of model checking a lot. |
| 学科主题 | 自动机理论 ; 计算机可靠性理论 ; 算法理论 ; 数据安全与计算机安全 |
| 语种 | 中文 |
| 公开日期 | 2010-06-08 |
| 源URL | [http://124.16.136.157/handle/311060/2342]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 王勤思. 构建度量区间时序逻辑的时间自动机[D]. 北京. 中国科学院研究生院. 2010. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。