【摘 要】
：
文件系统作为操作系统中数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法时微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架
【机 构】
：
常熟理工学院计算机科学与工程学院,江苏苏州215500;南京大学软件新技术国家重点实验室,南京210046;南京大学计算机科学与技术系,南京210046;伦敦大学国王学院,英国伦敦WC2R2LS南京大
论文部分内容阅读
文件系统作为操作系统中数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法时微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语义和系统状态转换,分析和归纳文件系统的功能正确性断言.以实现的微内核安全操作系统(Verified Trusted Oper ating System,VTOS)为例,阐述在Isabelle/HOL定理证明器环境中构建状态自动机模型的方法,并对VTOS文件系统的形式化设计和功能正确性断言进行一致性验证,结果显示,VTOS文件系统的设计和实现符合预期的正确性规格说明.
其他文献
条件风险值模型是风险管理中的一种重要工具.文章研究了一种具有上下层决策的多损失条件风险值模型,引入了基于权值的多个损失函数下的α-VaR损失值(最小风险值)和α-CVaR损
在当前的国际分工体系下,我国依靠大量劳动力支撑起制造业的比较优势,其持续发挥的前提是劳动要素从质和量上自始至终都能得到必要的补充,而这一前提正是马克思工资理论中劳
2001年春季在临安(30.30°N,119.75°E)进行的臭氧垂直探测发现,从3月25到31日有一次明显的臭氧异常增加过程,其中尤以29日和30日对流层上层的臭氧异常增加最具代表性.结合分
读,对"至道在微,变化无穷,孰知其原?窘乎哉,消者瞿瞿,孰知其要?闵闵之当,孰者为良"一段,颇为不解.以"瞿瞿"、"闵闵"二语,横亘其间,令不得通矣.吾查稽群言,考辨良久,一旦豁然,
矿物岩石的表面微形貌和孔隙结构是影响其地球化学行为的关键因素,从纳米尺度上表征这一特征对地球化学动力学研究和材料研发有着重要的意义。重点介绍了基于吸附等温线的分
文章旨在通过沉积相的研究,弄清孔雀河斜坡储盖组合,解决长期以来勘探成功率极低,在油气源充足的情况条件下找不到大油气田的问题。利用单井沉积相分析、典型井岩心分析、野
探讨了次氯酸盐氧化法制备的高纯度高铁酸钾对微污染水中双酚A(BPA)的降解效果以其影响因素。结果表明,采用次氯酸盐氧化法自制的高铁酸钾的质量分数可以稳定在90%以上;在pH
白垩纪事件是全球非常明显和重要的一次地质突发事件,包括洋壳的超巨量形成,地磁正超时达41Ma之久(124~83 Ma),海水温度大幅度升高,黑色页岩沉积和石油形成的大量增长,海平面的快速上升,大气CO2水平的急剧升高,以及伴生的生物灭绝事件等。中—新生代的大火成岩省与冈瓦纳超大陆的裂解伴生,是超级地幔热柱产生的结果,而与欧亚超大陆的形成伴生分散火成岩省,是超级冷地幔下降流的结果,两者的联合构成全地
通过对南海北部ODP184航次1148站井深477 m之下深海相渐新世浮游有孔虫Globoquadrina baromoenensis压扁壳、次生方解石和充填壳的氧同位素对比,定量分析了钙质成岩作用对壳
现代软件的功能需求越来越多样,软件编制规模越来越大,但隐藏其中的代码错误也随之增长.与此同时,种类丰富的外设、高级程序语言特性、现代处理器特性等因素的出现,却使得软