基于具有时间性质的自动机模型检测的程序分析方法研究

保证对实时性有要求的程序语言能够高效、正确和可靠地运行，有着重要的理论和应用价值，已成为形式化方法研究领域中的热点之一。本课题拟采用基于具有时间性质的自动机模型检测的方法，对这类程序语言进行程序分析研究，以期达到其高效、正确和可靠地运行目标，须解决两类主要问题：i.程序语言的实时性所带来的并发性问题；ii.对时间建模的有效手段和理论基础。目前国内外众多的并发模型检测理论的研究结果为解决并发性问题提供了理论基础，通过借鉴这些研究成果，找出解决适合实时性并发的方法；对于时间建模问题，要建立针对实时性程序语言模块化的特点的新模型，解决在时序语言上新计算的可判定性问题和计算复杂性问题，并根据时序语言信息量的度量方法，建立在时序语言上的新的模型检测方法，结合解决第一类问题的结果，给出新模型检测方法的高效实现。作为验证研究成果的案例，实现AADL语言的自动化程序分析工具。

实时程序的本质就是并发程序。因此即使单线程实时程序分析，其性质与多线程的程序分析相同。对于实时程序分析，研究做出了如下贡献：在理论上，提出了良结构下推自动机，为通用多线程程序进行建模，其两个可判定子集可以覆盖下推及其扩展系统以及向量加法及其扩展系统，其覆盖稠密时间下推自动机的现象说明了实时程序与并发程序的相同；提出了嵌套时间自动机，证明了存在私有时钟的时间敏感上下文系统可达性可判定的结论，并同时证明了一些实时程序在不同时钟约束下可达性的判定性结论。在实践上，提出了控制器自动机，用来进行模块化实时模型检测，细粒度地研究了模块之间的并发与互斥，并且实现了工具。