验证带有线程动态创建和退出的多线程程序.pdfVIP

摘要 法；2)提出了对程序内存划分的显式的推理机制，该机制可用于验证底层程序的 内存划分；3)使用计算机辅助定理证明工具Coq实现了框架的形式化定义及可靠 性证明。 本文的工作是在原有工作基础上对证明操作系统做出的进一步尝试。操作系统 包含虚拟存储，地址映射，硬件驱动等诸多机制，尽管本文的扩展框架模型与真 实的操作系统内核还存在着差距，但是本文工作为验证操作系统内核提供了一种 途径。同时，本文也为汇编语言及程序的形式验证，特别是为携带证明的代码的 技术的应用积累了重要的理论和实践经验。 关键词：软件安全，线程的动态创建和退出，程序验证，多线程，汇编代码 Ⅱ Abstract Abstract Withthe of hardware，thesoftware’Sscale rapid computer computer development the the and are of softwareis a safety complexitygrowingday·—by-·day．Now becoming hotissueinboth and ofcurrentsoftware industrycomputerscience．Safety computer most onsoftwareand safe thesafe depends testingusingprogramminglanguage．But safe as et based language，suchC撑，Javaa1．，are propertiessupportedby programming ontheruntime．Andthesoftwareliesonthetester’S itseems testing ability,moreover tocoverallsituationstest verificationisasolutioncase impossible by cases．Program in for software science．Itusesformular presentedbuidinghi曲reliable compmer to software’Sand seemstobeaneffective techniqueverifying safetyreliability,and way while verificationviaformalmethodsinthe ofsoftware performingprogram stages development． is usedinsoftware Nowd