改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.

限界模型检测方法及其应用

形式化验证主要是通过精确的分析来证明或证伪硬件或软件系统中一些明确的声明或者性质。形式化验证方法在广义上可以分成两大类：模型检测和定理证明。模型检测由对模型的所有状态和迁移做详尽访问的自动检测机制组成。这种机制是通过对适当的抽象模型进行直接或间接的状态枚举技术来实现的，从而证明模型中存在或者不存在所谓的“瑕疵”状态。定理证明则是运用数学推理和逻辑推论来证明系统的正确性。本文所讨论的就是模型检测方法中的限界模型检测方法及其相关的改进和应用。近些年来，基于可满足性求解（SAT）的限界模型检测方法作为基于BDD的模型检测方法的一种有效的补充，已经有了一定的发展。A. Biere等人最先提出了对于线性时序逻辑公式（LTL）的限界模型检测方法，进而，W.Penczek又提出了对于全局计算树逻辑（ACTL）的限界模型检测方法。由于模型检测方法具有很高的复杂性，因此，其效率问题始终倍受关注。论文第一个方面的重要贡献就体现在提高限界模型检测效率方面的相关研究上。我们对Penczek提出的限界模型检测方法进行了两方面的改进，以提高其求解效率。第一方面的改进是通过改进所需路径条数计算函数，将时序操作符EX和其它时序操作符区分开来，以减少编码时所需的迁移关系和变量数目；第二方面的改进则是采用统一路径编码的方式来简化公式的编码。通过这两方面的改进，公式在最坏情况下的编码复杂度得到了有效的降低。同时，我们还在工具BMV中实现了改进后的方法。随着实时系统的应用日益广泛，在对全局计算树逻辑的限界模型检测方法做了改进，提高了其求解效率以后，我们又将目光转移到了对实时系统的限界模型检测上。如何将限界模型检测方法高效的运用到对实时系统的检测当中成为了本文第二个方面的重要贡献。基于SAT的限界模型检测方法在对实时系统的模型和描述性质的公式进行编码时，需要对时间变量和时钟约束进行布尔编码，由于时间的连续性和不确定性，使得在对它进行布尔编码时，往往会相当的复杂，不仅耗费大量的时间，而且还不利于SAT的求解，即使是使用改进后的限界模型检测方法，整个验证过程的效率还是很低。所以，在对实时系统进行限界模型检测方面，我们转而考虑采用基于可满足性模块理论（SMT）的方法来对实时系统的模型和描述性质的公式进行编码。由于SMT可以直接处理基于整数或者实数的线性算术表达式，因此，我们可以直接用整型或者实型变量来表示时间变量，用线性算术表达式来表示时钟约束。与基于SAT的限界模型检测方法相比，基于SMT的限界模型检测方法在处理实时系统方面，不仅简化了编码过程，而且大大提高了求解效率。在此基础上，我们运用基于SAT的对全局计算树逻辑的限界模型检测方法中的改进思想，对基于SMT的实时系统的限界模型检测方法也做了相应的改进，使其求解效率较之改进前有了较大的提升。最后，我们就基于SAT的限界模型检测方法和基于SMT的限界模型检测方法以及它们的改进方法进行了一系列的实验对比。从实验结果可以看出，改进后的方法比改进前的方法在时间效率和空间效率上都有明显的提升，同时就实时系统来说，采用了SMT和限界模型检测相结合的方法以后，效率也比没有采用这两者的方法要高很多。

基于Yices对时间自动机的有界模型检测

随着工业化程度的提高，对模型的检测方法受到越来越大的重视。通常的检测方法有推理验证和模型检测。而相对于推理验证，模型检测由于其高度自动化的检测过程，在工业界有着更广泛的应用。 模型检测自从概念雏形开始之时，就受到状态爆炸问题的困扰。为了解决这个问题，不同的技术被提了出来。McMillan提出利用OBDD的符号模型检测方法在一定程度上解决了这个问题。另外，本文所主要讲述的有界模型检测，经大量的实践证明，对符号模型检测也是一个很好的补充。 由于问题的特殊性，科学家提出来不同的模型来描述不同情况的系统。由于时间自动机能够很好地描述异步系统，而且这种系统广泛地存在于现实生活中，对时间自动机这种特殊模型的验证方法的研究变得很有必要。另外，由于时间自动机带有实数域的时钟变量，这导致了时间自动机有一个无限域的状态迁移图。为了利用模型检测的方法对其进行验证，需要对时间变量进行预处理。一般的方法是把时钟所对应的时钟区或时钟域根据等价性，化为有限的域，相应地，把时间自动机转化为有限的状态迁移图。 为了避免在对时间自动机有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理，本文给出一个利用SMT工具进行的对时间自动机进行有界模型检测的方法。该方法的主要优点是无需将时间自动机中的时钟进行预处理，也不需要将模型中的变量进行布尔编码，只需将时间自动机转变为SMT工具可解的逻辑公式，利用SMT的高效求解来进行模型检测。实验结果表明，对于某些可达性性质的验证，这种方法的效率有一定的优势。

组合对象的搜索算法研究

现实世界中的大量问题涉及如何安排有限个离散的基本对象，使之满足特定约束，这类问题可通称为组合问题。本论文主要研究复杂的组合对象的存在性问题。我们特别关注较难求解的组合问题，从算法复杂度上来说，至少是NP难的。由于这些组合对象相应的约束一般都不太容易满足，因此局部搜索等非完备算法方法常常失效。我们致力于研究高效的完备搜索算法，能够在庞大的搜索空间中精准地找到解，当解不存在时，也能够给出确定性的回答。 作者在博士期间的工作可分为两部分：组合数学问题的自动求解和线性约束上的可满足性模理论的体积求解。 我们系统化地研究了组合数学问题的计算机求解，这部分研究包括三大类问题：幂等拟群的大集问题、正交拉丁方和正交数组。这些问题的共同特点是，要寻找的不是一个复杂的组合对象，而是一系列复杂的组合对象，这些对象相互之间还要满足一定的约束。这样一来，搜索空间比寻找单独的一个组合对象要庞大很多倍，问题的难度也大大增加了。对于每一类问题，我们都通过深入研究其结构特征，提出了有效的问题表示方法和搜索方法，发展了一系列新颖的消除同构技术来降低搜索空间，在搜索中我们应用了自动推理最新的技术和工具，如高效的一阶逻辑模型产生器和命题逻辑求解器等，取得了较好的效果。具体来说，我们的工作包括以下三点： (1) n阶幂等拟群的大集问题需要寻找n-2个不相交的幂等拟群，这比寻找单个的满足特定性质的拟群要困难的多。我们设计了约束分割的策略，解决了幂等拟群大集上的一系列开放性问题，特别是得出了LSPQ(11)不存在的结论。我们的方法不但可以回答特定的大集是否存在，还能够确定相互不相交的拟群的最大个数。这些数学结果对朱烈教授等数学家很有意义，并被收入``HandBook of Satisfiability"一书中。 (2) 正交拉丁方的存在性是组合数学中著名的问题。我们利用一阶逻辑有限模型产生器对该问题进行了尝试，提出了一种新的建模方法，称为横截建模，其效果比直接建模方法提高了若干个数量级。同时，我们也提出了一种新的打破对称策略。 (3) 正交数组是一种重要的组合数学结构，可用于软件组件的集成测试。我们设计了一个搜索正交数组的完备性算法，并提出了一些新颖的打破对称技术。与当前的其它工作不同，我们的算法是普适性的，对输入OA参数无任何限制，并且当搜索完成后总能得到确定性的答案。实验表明，我们的工具BOAS在搜索强度为3及其以上的正交数组时非常高效，而用传统的数学方法构造这些数组则很困难，局部搜索算法也对这些数组常常失效。而且，BOAS能够轻易地解决一批对于其它完备算法来说非常难的实例。 我们研究的第二个方面是线性理论上的SMT实例的体积计算问题。关于各类逻辑和约束语言的可满足性问题有大量的研究工作，比如SAT和可满足性模理论（SMT），另一方面，判定问题的计数版本在自动推理中也非常重要。我们研究了SMT的计数版本，即对给定的SMT实例（更精确地说，线性算术约束的布尔组合）如何计算解的个数，或者是说如何计算解空间的体积。这一问题同时扩展了命题逻辑的模型计数问题和凸多面体的体积计算问题。SMT实例的体积计算在许多领域都有潜在的应用价值，比如程序分析与验证和近似推理，但目前还没有相关的研究工作。我们首次研究了这一问题，提出了一个高效的体积计算方法——逐簇法，我们的算法集成了SMT求解中的最新技术。我们的原型工具在随机实例上产生了较好的效果，并可应用在实际的程序实例中，以寻找热门路径。

A Structured Prediction Approach for Statistical Machine Translation

We propose a new formally syntax-based method for statistical machine translation. Transductions between parsing trees are transformed into a problem of sequence tagging, which is then tackled by a search- based structured prediction method. This allows us to automatically acquire transla- tion knowledge from a parallel corpus without the need of complex linguistic parsing. This method can achieve compa- rable results with phrase-based method (like Pharaoh), however, only about ten percent number of translation table is used. Experiments show that the structured pre- diction approach for SMT is promising for its strong ability at combining words.

基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法。该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测。实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势。

连续提取和液体磷核磁共振表征太湖梅梁湾沉积物中磷的剖面分布

应用连续提取法（SMT）和液体磷核磁共振（31P NMR）技术研究了太湖北部梅梁湾沉积物中磷形态和组成的剖面变化。结果表明，铁／铝磷是沉积物中磷的主要形态，约占总磷含量的44．0-54．6％。总磷、无机磷、有机磷和铁／铝磷含量均随沉积深度增加呈降低趋势，至18cm以下略有增加，而钙磷却在柱样下部随沉积深度增加呈累积趋势。31PNMR显示，沉积物磷主要由正磷酸盐（72．0--99．2％）和磷酸单酯（0．8--25．9％）构成，磷酸二酯、膦酸盐和焦磷酸盐的相对含量非常低，分别为1．0％、0．4-1．0％和0．1％。正磷酸盐含量在沉积物表层9cm内减少了65％，9cm以下波动变化，但总体呈降低趋势。这些特征表明沉积物中磷对梅梁湾上覆水体具有强烈的释放潜力，是太湖富营养化发生的重要因素.