系统的同时镇定问题和安全性验证是系统科学与控制理论中的基本问题,有着非常重要的理论意义和应用价值。同时镇定问题考虑如何设计单个的控制器,使其可以同时镇定给定的多个对象,即要求系统的闭环传递函数是稳定的。目前学术界仅对线性系统有一些初步的理论结果,特别地,即使对于三个线性对象的同时镇定问题,也存在大量有待探讨的理论问题。而系统的安全性验证问题则是从实际应用出发,探讨如何验证系统是否满足实际需求的某些约束条件性质,避免系统发生某些不期望的演化过程；这些问题往往转化为若干代数不等式的命题是否成立的验证问题,而求解或者证明这些不等式构成的半代数系统,通常依赖于一些特殊的人工技巧结合计算机进行机器自动证明。本文研究了线性系统同时镇定和非线性系统安全性检验的若干相关问题,主要研究内容和工作如下：1.研究了线性系统同时镇定中著名的“比利时巧克力问题”的系统参数的理论上界确定问题。系统地讨论了比利时巧克力问题连续系统情形与对应离散系统情形下参数的关系,这个离散情形下的参数与复分析理论中著名的“Goldberg常数”有着深刻的联系,基于符号计算的方法和椭圆模函数的概念,本文对复平面挖去两点剩下区域的同伦双曲测地线进行了有效的估计,并将该结果应用于比利时巧克力问题的上界估计中,我们得到的参数估计值改进了Hempel和Smith计算的数值结果。2.对于比利时巧克力问题的数值下界,讨论了控制器设计中多项式方程根的分布与系统参数的关系,指出Boston在2012年宣布找到的“巧克力问题的新界限(0.976462)”文中提到的("a new world record")是不可信的,经过验证,他找到的控制器并不能保证系统闭环多项式是稳定的。另外本文作者给出了一种参数扰动和Hurwitz稳定验证结合的方法,对Boston提出的临界多项式进行辅助参数扰动,提出了一种镇定控制设计算法。实验例子表明,在某些低阶情形下我们的算法得到的数值下界显著地改进了对应阶次的最好结果。3.研究了非线性系统的安全性验证问题。基于符号计算工具、结合微分动力系统定性理论、采用构造分段判别函数的思想以及微分方程解的幂级数截断估计技巧,将问题转化为一组代数不等式的验证问题,并以Van der Pol系统为例进行了安全性验证,可按预先设定的精度,精确地捕捉“安全”与“不安全”之间的临界点。可以认为由上述方法所得到的条件是Sharp的。4.考虑了非线性微分方程的安全系统验证的区域变换问题。通过构造从初始区域出发到非安全区域外部的共形映射,将这个映射转换成二维平面上的实变量代换；对已有的非线性系统进行坐标变换,将原来系统的安全性验证问题转化为新坐标下的安全性验证问题。讨论了经过变换后的系统与原系统的保持不变的一些性质。5.利用符号计算的方法,对于著名的Mordell不等式,使用归一化的方法将含有约束条件的问题转化为无约束的不等式验证问题；当n=3时的情况使用柱形代数分解的方法验证不等式是成立的,采用差分代换的方法验证了n=4不等式也是成立的。