论文部分内容阅读
智能交通系统((CityIntelligentTrafficSystem)(CITS))是目前比较热门的有实际应用背景的项目，模型检查(ModelChecking)也是近二十多年来软件工程界的一个热门话题。根据CITS涵盖面很广的特点，本文仅仅从交通及信号数据的角度，展开一些涉及计算理论和形式化逻辑基础方面的探讨。以交通信号及流量分析与控制为背景，探讨软件工程特别是形式化的模型检查技术对这些实际问题的解决方案，并进一步探讨软件工程和应用的互动发展以及其内在深刻的逻辑背景。
在深入地分析Bryant的OBDD(OrderedBinaryDecisionDiagram)图表方法，Clarke的模型检查基本原理和Pnueli的Tableau图方法的基础上，我们通过引入了一个动态Kripke语义模型，得到了可以不用OBDD就可以完成模型检查计算的基于矩阵向量数值计算的“直接模型检查DMC”算法，这是一项原创的方法和算法。由于我们的算法不再需要对状态转化关系进行复杂的OBDD计算和存储，也就是说在我们的未来模型检查工具中将不再需要Bryant的OBDD的16种符号公式运算而直接采用数值计算，所以同样的计算模型下采用我们的算法将可以在极短的时间内完成状态的可达性分析，从而为将模型检查技术实现成一个实时运行部件在计算算法上打下了基础。
本文研究了模型检查技术应用于交通信号调度管理的可行性。采用基于随机过程理论的离散型Markov-Chain的方法描述了CITS系统的“绿灯波原则”，“公平通行原则”；采用双向工作流的分析，将电信和广电领域单边带的概念运用到CITS中；同时运用可计算性理论中的有穷损伤优先原理并结合操作系统的一些基本调度原理，提出了基于信号控制的绿灯波和动态快速干道的建立对其它方向阻塞的损伤记点原则。