开放反应系统的模型检测与合成

计算机的普及应用使得程序复杂性与软件可靠性的矛盾日益突出。为了缓解这种矛盾，程序的性质及其验证方法以及系统的合成方法的研究得到广泛的重视。一类程序性质验证的方法为模型检测。传统的模型检测方法主要集中在状态和状态转换关系方面的性质研究，对事件和动作之间关系的深入研究较少。本项目的研究为面向开放反应系统的模型检测与合成方法，旨在深入研究基于事件和动作之间关系的、面向开放反应系统的模型检测原理，并在这基础上，研究开放反应系统的合成。主要内容包括开放反应系统的抽象模型及其模型检测和合成原理，算法及相关分析验证工具的设计。针对开放反应系统的性质和特点，如事件与动作的关系、动作的选择与系统运行过程的关系，建立适合于开放反应系统的抽象模型，选择合适的逻辑以描述其性质，研究其模型检测及合成原理，并研究模型检测和逻辑推理方法的结合以降低模型检测的复杂性，对开放系统的设计和验证有重要意义。