【摘 要】
：
操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验
【基金项目】
：
国家自然科学基金资助项目（61321491）, 江苏省工业和信息产业转型升级专项项目（2015SJXKJ5038）, 国网电力科学研究院科技项目（5246DR150002）
论文部分内容阅读
操作系统作为信息时代的基石,其安全性不言而喻。常规的软件测试方法不足以保障操作系统的安全性,需使用更为严格的基于数理逻辑的形式化验证方法。本文提出一种软件形式化验证的新思路：通过在Isabelle中构造模拟运行环境,使汇编代码运行其中,并记录系统状态的变化,最终根据程序运行前后系统状态的变化情况判断程序的正确性和安全性。重点介绍了顺序、分支和循环等3种程序结构的证明方法,并通过一个程序实例证明,得到在任意前提条件下程序执行前后系统状态的变化情况。
其他文献
针对非计算机专业人员在开发Access数据库应用系统时遇到的登录身份验证问题，介绍采用多种类型宏完成多用户多角色登录验证的设计思路和实现方法。其中首次将Access 2010中新
针对一类非线性、大时延、变参数的复杂温度对象，设计滑模变结构控制。对传统极点配置公式进行改进，并用于滑模面函数的设计；对系统输出曲线初始阶段的特征做提取，并表达为二元线
社会网络中包含大量的社会信息，如何从这些社会信息中发掘对用户有用的信息已成为学者和专家的研究热点。本文提出一种基于社会正则化的推荐算法：把改进的矩阵分解技术应用到社