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

摘要

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