微内核架构文件系统的形式化设计与验证方法研究

文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper-ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.     

λ演算中的第二不动点定理*

作者研究λ演算中的第二不动点的性质．首先讨论关于第二不动点的3个命题之间的关系且证明了它们．然后为第二不动点组合子给以一个充分条件且作出一系列的第二不动点组合子．作者还提出和证明了多元第二不动点定理．     

冻结／解冻机制——软件开发环境中的一种新机制

通常在软件开发环境中动态快速原型开发和高效产品生成之间存在着一条显著的鸿沟,即先在动态环境下进行快速原型开发，原型开发成功后，再重新编码以生成高效产品.显然，这造成了软件开发时间和费用的浪费.本文提出了一种新的机制——冻结／解冻机制，旨在消除这条鸿沟，使得从快速原型能够平滑过渡到高效产品.     

微内核架构内存管理的形式化设计和验证方法研究

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS（Verified Secure Operating System）内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.     

λ演算中的第二不动点定理

作者研究λ演算中第二不动点的性质，首先关于第二不动点的３个例题之间的关系且证明了这们，然后为第二不动点组合子给以一个充分条件且作一系列的第二不动点组子，作者还提出和证明了多元第二不点宣。     

ITT系统的一些性质

作者给出关于不交并类型的新的消去规则，并且证明新规则与原先的消去规则等价。在本文中，Ｎｋ被定义成类型Ｎ的子集，以及Ｎｋ的所有规则被导出，这里ｋ≥１。文中对Ｎ的分离性也作了详细的讨论。     

R-演算中若干问题的研究

李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念"必要前提",第1种方法来自R-演算,第2种方法基于极大协调子集与极小非协调子集的,最后一种方法是对于R-必要前提的归纳定义.通过比较这3种方法,指出各自的优缺点,并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时,还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.