基于广义符号轨迹赋值理论的模型检测

广义符号轨迹赋值（GSTE）是一种针对超大规模集成化电路设计的符号轨迹赋值的推广。符号轨迹赋值在Intel、IBM和Motorola等公司得到成功的应用。广义符号轨迹赋值可以验证无限时间区间上的omega性质，在Intel得到成功应用。但它发展时间不长，还不成熟。本项目针对五个方面：GSTE中断言图之间的蕴涵关系，细化与反例的产生，GSTE与传统模型检验的关系，软硬件协同验证，系统并发性质的验证，进行研究。目标是丰富GSTE理论，实现基于这些理论的高效、准确的形式化验证工具。基于语言的蕴涵关系可以转换为传统模型检验有限状态机之间的蕴涵关系。基于模型的蕴涵关系可以通过求断言图的极大模型来判断。如何在GSTE中引入SAT和按断言图作同步模拟是细化与产生反例的重要手段。比较GSTE检验方法与传统模型检验方法的差别，融合它们的优点，设计高效的形式化验证算法。同时建立软硬件统一的形式化描述方法。

摘要：广义符号轨迹赋值（GSTE）是一种针对超大规模集成化电路设计的符号轨迹赋值的推广。广义符号轨迹赋值在Intel、IBM和Motorola等公司得到成功的应用。我们研究了如下几个方面：GSTE中断言图之间的蕴涵关系；细化与反例的产生；GSTE与传统模型检验的关系；嵌入式系统的仿真；SAT问题完备算法的优化；SAT求解器和BDD的应用等等。我们比较了GSTE检验方法与传统模型检验方法的差别，融合了它们的优点，设计出了高效的形式化验证算法；我们丰富了GSTE理论，实现了基于这些理论的高效、准确的形式化验证工具；同时，通过应用形式化的方法，我们验证了一些混杂系统的特性，优化了生化系统中同步布尔网络求吸引子的算法等等。