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