【作者】 朱维军；

【导师】 周利华；

【作者基本信息】 西安电子科技大学 ， 计算机应用技术， 2011， 博士

【摘要】 行为、事件具有实时关系的软件或硬件系统构成了实时(计算)系统。在交通控制,航空航天等一系列对安全性要求极高的应用领域,实时系统的形式化验证成为保证系统正确性的重要手段。实时模型检测就是其中的一类自动验证方法,原理是实时逻辑公式描述系统所需满足的性质,时间自动机建立系统模型,验证算法自动判定模型是否满足性质。实时逻辑有很多种,用于形式化描述与验证也各有其优势,时间区间时序逻辑就是其中的一种线性实时逻辑,并已被应用于对一些实时系统的形式化描述与分析中。虽然该逻辑有其独特的比较优势,然而到目前为止,时间区间时序逻辑还不能用于实时系统的模型检测,因为缺少验证方法,也没有支撑方法的形式化理论来加深人们对该逻辑的理解和认识。针对于此,本文研究命题部分的时间区间时序逻辑模型检测问题,以该问题为主线,从理论、方法、应用三个层面构建其体系。为了搞清楚该逻辑可以描述哪些性质、是否可应用于模型检测以及模型检测的效率,本文分别从逻辑的表达能力、判定性及复杂性三个方面进行研究,从而形成该逻辑模型检测的形式化理论。证明了离散时间域上的该逻辑与离散时间正则表达式、离散时间自动机等价,结果表明一切离散时间正则语言均可由离散时间区间时序逻辑加以形式化的描述。证明了稠时间逻辑其满足性不可判定,但存在其子集可判定,证明了离散时间逻辑满足性可判定,结果表明离散时间语义下该逻辑可模型检测。证明了问题固有复杂度为非初等,这表明人们所能开发出的最优工具在最坏情况下模型检测需时非初等,且分析表明最坏情况很难实际出现。为了得到该逻辑模型检测的具体可操作方法,我们提出了一种新的计算模型---时间正则图。首先把逻辑公式转化为时间正则图,使得公式模型与图中路径一一对应。其次在图中添加接受条件即为性质时间自动机。最后性质自动机与模型自动机求交判空即为模型检测结果。这样就得到了基于时间正则图的离散时间区间时序逻辑模型检测算法。复杂度分析表明,新算法复杂度达到问题固有复杂度下限。针对样本公式的仿真结果表明,新方法在生成图状态空间方面优于对同类逻辑验证的现有方法。同时新方法也可推广到包括离散时段演算等同类逻辑模型检测中,我们给出了这样的推广算法。为了避免普通模型检测方法从逻辑公式到自动机的复杂转换,我们发现了一种使用时间区间时序逻辑公式建立系统模型的方法,使用另一个该逻辑公式描述性质,这样统一模型检测问题就被归约为本文研究已解决的该逻辑公式满足性判定问题。与普通模型检测方法相比,新方法有利于实时计算系统开发中从规范到实现的逐步细化与求精。为了提高误用入侵检测对实时攻击与并发攻击的描述能力与检测能力,我们提出了一种基于时间区间时序逻辑模型检测的入侵检测方法。首先使用该逻辑的公式描述不同攻击模式的签名,其次使用时间自动机建立日志库模型,最后模型检测算法自动验证自动机是否满足公式,即日志记录是否与攻击模式相符。仿真结果表明,与现有的基于模型检测的入侵检测方法相比,新方法可更有效地检测多种形式的telnet攻击和口令攻击。更多还原

【Abstract】 Real-time systems are constituted of software or hardware systems that have real-time constraints. In the safety-critical systems, such as transport control systems, spaceflight and nuclear react control systems, model checking is a vital formal technique for guarantee correctness of real-time systems. The principles of this method are: describe the properties of a system with some real-time logic formulas, construct system models with timed automata, model checking algorithm decides automatically whether the models satisfy the properties. Several real-time logics including timed interval temporal logic (TITL) have been presented for formal verification. As a linear real-time logic, TITL has been used widely due to its advantages. But until now, TITL model checking problem has not been solved due to its absence of verification technique and formal theory. To this end, this paper investigates propositional TITL model checking problem as well as constructs its architecture on theory, method and application.In order to make clear what kind of properties can be described by TITL, whether TITL can be used to model checking or not, and the efficiency of TITL model checking, we study expressive power, decidability and complexity of the logic. We prove the equivalence relation between discrete TITL formulas, discrete timed regular expressions and discrete timed automata. So, all of discrete timed regular language can be described and verified by TITL formulas. We prove its satisfiability is not decidable in the dense time domain, but there exists some subsets of full version of the logic that can be decidable. And we prove full version of the logic can be decided in the discrete time domain. So, TITL model checking problem is decidable. We also prove TITL satisfiability checking is a non-elementary problem. As shown in the analysis, not operation and chop operation are embedded interleaved in the worst case, but the probability is very low. So, non-elementary complexity affects scarcely applications of TITL model checking.For automatic verification, we present a novel computational model named with timed normal form graph (TNFG). The fist step is to translate a TITL formula into a TNFG in order that there exists a one-to-one mapping between models of the formula and paths of the TNFG. The second step is to append accepting conditions to the TNFG in order to obtain the timed automaton modeling the TITL formula. The final step is to compute conduct automaton of two timed automata and decide whether the conduct automaton accept empty language or not. So, we obtain an algorithm for discrete TITL model checking based on TNFG. As shown in the complexity, our new algorithm reaches the lowest bound of inhabit problem complexity. As shown in the simulation results for some sample formulas, compared with the existing approaches, the new algorithm can produce lower state-space. And what’s more, we give an algorithm for translating formulas in a subset of discrete duration calculus (DC) into discrete TITL formulas. So, model checking this subset of discrete DC can be solved with TNFG.In order to avoid complicated transformation from logic formulas to automata, we find an approach for unified TITL model checking. The first step is to construct a system model by a TITL formula. The second step is to describe a property with another TITL formula. So, unified TITL model checking problem is deduced to satisfiability checking problem that has been solved in this paper. Compared with common model checking techniques, the unified technique is benefit for refinement of real-time systems.In order to raise the describing power of real-time attacks and concurrent attacks, we present an approach for intrusion detection based on TITL model checking. The first step is to describe attack patterns with TITL formulas. The second step is to construct an audit log by automata. The final step is to verify automatically whether automata satisfy formulas, i.e. the log match the attack patterns, by TITL model checking algorithm. As shown in the simulation results, compared with the existing approaches for intrusion detection based on model checking, our new approach can detect efficiently various telnet attacks and password attacks.更多还原