【作者】 徐鸣；

【导师】 李志斌；

【作者基本信息】 华东师范大学 ， 系统理论， 2010， 博士

【摘要】 形式化方法是开发高可信软件和安全攸关系统的有效途径,是高可信计算的研究重点之一。高可信计算追求软件和系统提供可信赖的计算服务能力,而这种可信赖性是建立在严格数学证明上的。形式化方法主要研究软硬件系统的规格描述、开发过程、以及检测验证,特别是程序正确性证明和系统安全性分析。研究的问题有活性、安全性、公平性、终止性、不变式、同步、异步、互斥、可达性、持续性、稳定性等。在处理这些程序和系统中的分析与验证问题时,传统的逻辑方法会因为状态空间爆炸而无法检测出全部错误,不能彻底地保证安全性；单纯数值计算又会产生浮点误差,影响整体的可靠性。因而,近年来研究者正在尝试使用以绝对准确性为目标的符号计算方法来处理它们,即将这些性质的检验问题转换成代数系统的求解问题。特别是随着计算机性能和计算机数学的不断发展,为开展该方向的研究提供了强有力的支撑。本文的主要贡献由以下几部分组成：1.理论部分：主要研究了若干种广义多项式的实根隔离问题。在M. Achatz等人2008年的工作基础上,提出了用连分数技巧逼近超越数ex和区间算术思想进行准确计算,改进了现有指数多项式实根隔离算法；同时对于幂指数多项式,推广了伪导数序列的构造方法,证明了广义Budan-Fourier定理对其仍然成立,并给出一个正根隔离近似算法。2.应用部分：主要尝试了将上述理论成果应用在程序验证和系统分析领域。方面,利用估计多指数多项式实根界算法,完善了A.Tiwari在2004年关于线性循环终止性的结论。在其终止性可判定理论的基础上,对于给定非终止循环构造出其非终止输入作为反例,使该结果更加完整。另一方面,将广义多项式实根隔离算法用于判定线性系统的可达性问题,除去了线性系统矩阵的可对角化限制,丰富了输入函数的类型,扩展了G.Lafferrierre等人在2001年的结果。3.软件部分：主要在计算机代数系统MAPLE下编制了程序包REACH,能够准确求解任意由指数多项式等式和不等式所组成系统,实现了判定有理特征值线性系统可达性的数学机械化,能集成在一般混成系统的验证工具中。更多还原

【Abstract】 Formal method is an effective approach to develop trustworthy softwares and safety-critical systems. It is also one of the most important topics in trustworthy computing. Trustworthy computing pursues the reliable computing services, whom need to be proved by rigorously mathematical reasoning. Formal method stares at the specification, develop-ment, checking and verification of software and hardware systems, specially for proving the correctness of programs and analyzing the safety of systems. Their core tasks include liveness, safety, fairness, termination, invariant, synchronization, asynchronization, ex-clusion, reachability, duration, stability and so on.For the problems in program verification and system analysis, the traditional logic method can not determine the whole safety since it would suffer from the state space ex-plosion and fail to find out all bugs. And purely numerical computation would involve floating-point errors, thus affects the reliability in large. So recent research resorts to symbolic computation, which places excessive emphasis on the absolute exactness, that is, reducing the problem of checking safety properties to that of solving algebraic systems. More importantly, this method is quite feasible and promising owing to the increasing-powerful computer performance and the growing-mature computer mathematics.The main contributions of this thesis are as follows:1. Theory:The real root isolation problems in several generalized polynomials are well studied. Based on M. Achatz’s work (2008), we present a tip of continued fraction for approaching to the transcendent number ex and compute the exact value with interval arithmetic, thus improve the existing algorithm for isolating the real roots of exponential polynomials. In the meanwhile, we also develop the construc-tion of pseudo-derivative sequences for power-exponential polynomials, prove the generalized Budan-Fourier theorem for them, and give an algorithm for isolating their positive roots approximately.2. Application:We dedicate the above theoretic results to the fields of program ver-ification and system analysis. On one hand, we present an algorithm for estimat-ing the real root bounds of multi-exponential polynomials, to supplement the re-sult about the termination of linear loops in A. Tiwari’s work (2004). Under his termination-deciding method, a nonterminating input can be further constructed as an counterexample for the given nonterminating loop, which makes the result more complete. On the other hand, we successfully decide the reachability of linear sys-tems by the algorithms of isolating those generalized polynomials’real roots. We remove the restriction that the matrices of linear systems must be diagonalizable and enlarge the scope of input functions, thus enrich G. Lafferrierre’s work (2001).3. Software:Based on the computer algebra system MAPLE, we provide a program package REACH, which can exactly solve the arbitrary system consisting of expo-nential polynomial equations and inequalities. It implements mathematics mecha-nization of deciding the reachability of rational eigenvalue linear systems, and can be integrated into verification tools for general hybrid systems.更多还原