基于线性时序逻辑的对象文件系统形式化描述  

Formalizing Description of Object File System Based on Linear Temporal Logic

作　　者：曾令仿[1] 冯丹[1] 王芳[1] 施展[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉,430074 华中科技大学计算机科学与技术学院,武汉,430074 华中科技大学计算机科学与技术学院,武汉,430074 华中科技大学计算机科学与技术学院,武汉,430074

出　　处：《计算机研究与发展》2007年第z1期154-160,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60303032,60603048);国家发改委CNGI基金项目(CNGI-04-5-1D);国家"九七三"重点基础研究发展规划基金项目(2004CB318201)

摘　　要：基于线性时序逻辑,给出了对象文件系统特性的形式化描述.对象文件系统时序逻辑(OFSTL)是线性时序逻辑在描述对象文件系统应用中的一个推广.用OFSTL描述对象文件系统的性质,用模型化的状态迁移系统表示对象文件系统的访问行为.试图解决目前对象文件系统研究存在的问题: ①关注提升对象文件系统性能和功能,但是以增加对象文件系统复杂性为代价; ②很少针对对象文件系统精确描述,缺乏形式化的辅助,妨碍从细节上考查对象文件系统的正确性.

关 键 词：对象文件系统 线性时序逻辑 智能存储 性质验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]