论文部分内容阅读
为了达到经过形式化验证分区操作系统内核隔离性质的目标,采取形式化方法描述系统的顶层规范设计中描述隔离性质需求,通过将航空电子应用软件标准接口ARINC653与GWV定理相结合,实现了对分区操作系统需要满足的隔离性质的抽象描述,并通过使用类Z/Z＋＋作为形式化描述语言。
分区操作系统内核中隔离性质的研究
【摘 要】
：
为了达到经过形式化验证分区操作系统内核隔离性质的目标,采取形式化方法描述系统的顶层规范设计中描述隔离性质需求,通过将航空电子应用软件标准接口ARINC653与GWV定理相结
【机 构】
：
太原理工大学计算机学院,清华大学计算机科学与技术系
【出 处】
：
太原理工大学学报
【发表日期】
：
2014年4期
【基金项目】
：
国家自然科学基金资助项目（61170051,61272086,90818019）,“核高基”国家科技重大专项（2012ZX01039-004）,山西省自然科学基金（2012011011-2）
其他文献
研究了褐煤进行低温热解时,热解温度对褐煤热解气相产物产量的影响规律;分析了不同热解温度下煤气的基本组成。结果表明,热解温度对煤气的产量、组成产生一定的影响。在300℃
遥感影像图质量的评价研究近些年主要集中在色彩质量评价及影像质量评价上,并有部分评价软件推出。笔者在研究的基础上,设计了遥感影像质量评价体系,提出了影像质量评价二级指标及相应权比,介绍了几何质量、色彩质量评价原理,最后设计并实现了遥感影像质量评价系统,并选择6种遥感影像图进行了色彩质量评价试验,以机助形式实现了半自动化的影像生产质量定量评价。结果表明:系统具有操作简单,定量客观等特点,可应用于遥感影
本研究利用中国科学院巴音布鲁克草原生态研究站1984-1990年、2004-2008年2个时间序列植物营养生长期的气候指标及净第一性生产力（NPP）实测值,结合北京模型、综合植被模型和林
利用ISSR分子标记，对河南主栽的9个枣品种进行了遗传关系分析．结果表明，10个引物共扩增出96个条带，多态性务带82个．9个枣品种45个样本的Nei’S基因遗传多样度（H。）为0．2720，Shannon信
盐生植物碱蓬是北方盐渍化草地一种潜在的饲料资源,其矿物元素富集的特征增加了家畜采食后的矿物质缺乏和不平衡的风险。本试验重点研究了羔羊日粮中添加0%,25%,50%碱蓬干草
对河南省正阳县典型土壤进行了分析与检索，确定其在中国土壤系统分类中的位置．结果表明，供试土壤在中国土壤系统分类中分别归属为淋溶土、变性土和雏形土3个土纲；湿润淋溶土、湿
对甲醇耐受性脂肪酶产生菌Galactomyses geotrichum SXL-107产酶条件进行了优化．通过单因素试验确定碳源、氮源和诱导剂，响应面法确定发酵培养条件，250mL摇瓶培养和10L发酵罐发
以叶片愈伤组织为材料,先分别在质量浓度为40,80,120,160,200 mg.L-1的MMS和质量分数分别为0.1%,0.2%,0.4%,0.6%的NaCl的MS增殖培养基中培养,确定愈伤组织的MMS半致死浓度和N