【摘 要】
：
形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如
【机 构】
：
常熟理工学院计算机科学与工程学院,南京大学软件新技术国家重点实验室
【基金项目】
：
国家自然科学基金(61402057);江苏省科技计划自然科学研究项目(BK20140418);中国博士后科学基金(2015M571737);江苏省高校“青蓝工程”优秀青年骨干教师培养对象项目(2017)
论文部分内容阅读
形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.
其他文献
自Wlerner提出配位学说以来,配位化学在与其他相关学科联系、融合和交叉过程中迅速地发展起来,配位法也越来越广泛地应用于农业、工业、医药、国防和航天等各个领域中。本文
本文以单板层积空心柱为研究对象，系统的研究了单板层积空心柱的制作方法和轴压承载性能，并通过ANSYS软件对其进行模拟分析。根据GB/T20241—2006《单板层积材》，本文选取含水率
金黄色葡萄球菌(Staphylococcus aureus,简称金葡菌)及肠毒素B(SEB)对海产品的严重污染一直困扰着海产品加工企业。本研究建立S.aureus及SEB免疫磁快速检测法,并评价两种制剂
本文主要是针对H公司的桌板线生产产能如何提高进行研究，文中首先详细介绍了桌板流水线由开料锯,冷压,数控机床,直线封边,手工修边,组装,包装这七个工作中心组成.并且分别介绍
为了研究双光子聚合加工光路系统对聚合效果的影响,使用ZEMAX软件对光路系统的3个主要部分,即扩束镜、扫描振镜和聚焦透镜分别进行了设计,然后将3个部分结合到一起,从整体上
目的分析重症监护病房(ICU)患者呼吸机相关性肺炎的发生原因及对策。方法选取100例医院ICU中使用呼吸机的患者作为观察对象,观察患者有无呼吸机相关性肺炎的出现,并通过采集
背景转化生长因子-β1(transforming growth factor -β1,TGF-β1)在心肌纤维化发生、发展过程中具有重要的作用。大量研究证实,TGF-β1/Smads信号传导通路是TGF-β1发挥生物
目的:探讨糜酶转基因小鼠心肌TGF-β/Smads信号转导通路相关基因mRNA表达的变化及三七花总皂苷的治疗影响。方法:24只7月龄糜酶转基因小鼠随机分为三七花总皂苷治疗组、糜酶
介绍了专用汽车的造型和轻量化设计的重要性,并结合造型设计的原则和轻量化材料的应用情况提出了现阶段提高我国专用汽车设计水平的思路和建议。
未来,汽车朝着电动化、智能化、网联化发展,自动驾驶是汽车产业与物联网、人工智能、计算机等新一代信息技术深度融合的产物,也是各国争抢的战略制高点。环境感知系统是实现