近年来，形式化方法——即在计算机系统和软件的规范、设计和构造中使用基于数学模型和离散数学的技术的工具的方法，被广泛应用于高等级安全操作系统的开发过程中。TCSEC的B2级和CC的EAL5级中规定了高安全等级操作系统必须使用形式化技术进行分析验证。　　 从形式化的角度确认一个操作系统是安全的，是指证明它满足某一给定的以安全模型形式描述的安全策略。只有有效保证从设计者到用户都相信模型本身正确无矛盾(验证Verification)，而实现代码准确地体现了模型(确认Validation)时，该操作系统才可以说是安全的。　　 本文首先介绍了几种有代表性的安全操作系统模型，以及结合了几种模型优点的可信进程模型。并且和其他组员共同进行形式化工具的调研，选定了Isabelle作为我们接下来形式化分析的环境。　　 接下来依据上述验证确认两部分的思想，首先结合安全操作系统状态机模型的特点，提出了一套直观的使用形式化工具Isabelle对其进行描述的方法。并且通过实际验证一种典型的状态机模型——可信进程模型，总结出了有效的使用Isabelle形式化设计、分析、验证模型的策略，即实现了对模型本身的验证；接着根据前人提出的一套使用Isabelle的基于DNF(析取范式)来提取测试用例的方法，进行了基于DBLP模型的安全操作系统的测试用例自动生成，并从安全为导向的视角，分析了这种方法在安全操作系统开发过程中的应用特性，即对测试一个安全操作系统是否正确实现了模型功能的确认工作做出了探索。