文档介绍：华东师范大学
博士学位论文
程序验证与系统分析中的若干符号计算问题
姓名:徐鸣
申请学位级别:博士
专业:系统理论
指导教师:李志斌
20100301
摘要形式化方法是开发高可信软件和安全攸关系统的有效途径,是高可信计算的研究重点之一。高可信计算追求软件和系统提供可信赖的计算服务能力,而这种可信赖性是建立在严格数学证明上的。形式化方法主要研究软硬件系统的规格描述、开发过程、以及检测验证,特别是程序正确性证明和系统安全性分析。研究的问题有活性、安全性、公平性、终止性、不变式、同步、异步、互斥、可达性、持续性、在处理这些程序和系统中的分析与验证问题时,传统的逻辑方法会因为状态空间爆炸而无法检测出全部错误,不能彻底地保证安全性;单纯数值计算又会产生浮点误差,影响整体的可靠性。因而,近年来研究者正在尝试使用以绝对准确性为目标的符号计算方法来处理它们,即将这些性质的检验问题转换成代数系统的求解问题。特别是随着计算机性能和计算机数学的不断发展,,提出了用连分数技巧逼近超越数酽和区间算术思想进行准确计算,改进了现有指数多项式实根隔离算法;同时对于幂指数多项式,推广了伪导数序列的构造方法,证明了广义ɡ矶云淙匀成立,并给出一个正根隔离近似算法。τ貌糠郑褐饕3⑹粤私鲜隼砺鄢晒τ迷诔绦蜓橹ず拖低撤治隽煊颉R方面,利用估计多指数多项式实根界算法,完善了甌旯赜谙性循环终止性的结论。在其终止性可判定理论的基础上,对于给定非终止循环构造出其非终止输入作为反例,使该结果更加完整。另一方面,将广义多项式实根隔离算法用于判定线性系统的可达性问题,除去了线性系统矩阵的可对角化限制,丰富了输入函数的类型,扩展了甃热嗽砑糠郑褐饕T诩扑慊低矼下编制了程序包,能够准确求解任意由指数多项式等式和不等式所组成系统,实现了判定有理特征值线性系统可达性的数学机械化,能集成在一般混成系统的验证工具中。稳定性等。供了强有力的支撑。本文的主要贡献由以下几部分组成:的结果。
关键词:符号计算,实根隔离,程序验证,终止性,混成系统,可达性数学主题分类:,
甌篢.,,瓵:八’甀,瓵疭酽甀瑆,—瓼琩—瑂甌,瑃,瑂,,瑀,.,甋瑆瑃,—猰瓸,琾,.,瑃猟.—
.甒,,.痳瑆琣琀,,,,
%次徐呜博士学位论文答辩委员会成员名单泄牒潭诽躥私姓名职称单位备注主席蒮翻诌钾
第一章绪论一弟一早珀研究背景了匕一程序验证和系统分析都是形式化方法中的核心研究方向。程序验证主要研究程序代码的正确性,已在开发与设计密码芯片、特殊⒏叨酥靼宓攘煊虻玫焦泛应用;而系统分析主要研究物理控制系统的安全性、可靠性、稳定性等问题,无论是在理论研究还是在工程应用都有极其重要价值。两者虽研究的对象和侧重点不同,但研究的方法、技术手段却大致相同。特别是近年来随着信息锢砣诤舷的迅速发展,更使得两者相互影响、相互渗透、相互发展。因此,用统一的观点研究它们将是本文研究工作的首要出发点。在理论计算机科学和软件工程领域,形式化方法是一种基于数学上推理证明的特定技术,用于软硬件系统的规格描述、开发设计、测试验证等各个环节,以严格的归纳与演绎手段,换取系统提供可靠的和鲁棒的计算服务能力。特别适用于军事、航空、航天、医疗、交通等关键应用领域中许多可靠性要求严格的高可信软件和安全攸关系统,如核反应堆控制系统、城市交通导航系统、国家电网调控系统等。任何一个细小的错误都可能引发不可预测的灾难性后果。年突鸺状畏⑸涞氖О芫褪且桓龅湫偷睦印緇】。其原因是突鸺募扑机导航软件是直接复制了能在型火箭上运行正常的软件,但突鸺某叨群驮载量都大幅增加了,导致最终的崩溃。如何保证这些程序的绝对正确、系统的绝对可靠是计算机科学家和控制论专家们所共同面临的重大挑战形式化方法是开发高可信软件和安全攸关系统的有效途径,已经在工业实践中获得巨大成功。现有的形式化方法有基于逻辑的、有基于自动机的,也有基于代数的。但无论使用何种形式化方法,研究的问题都是相同的,它们包括活性、安全性、公平性、终止性、不变式、同步、异步、互斥、可达性、持续性、稳定性等。已实现的形式化分析与验证技术主要有如下四种:静态程序分析⒊绦蚶嘈突⒒诙ɡ碇っ鞯难菀U馑闹中问窖橹ぜ际醯暮诵亩际统和模型检测
具闭僦中,用于对由线性动力系统、自动机、规则和命题逻辑规则所构成的混成系统进行建模描述【硼;并应用在空中交通的控制系统中。围绕程序正确性证明和系统的安全性分析展开的。因此,程序验证和系统分析是形式化方法的核心研究方向。长期来,国际上大量的研究团队对程序验证和系统分析进