计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2007年
z1期
154-160
,共7页
曾令仿%冯丹%王芳%施展
曾令倣%馮丹%王芳%施展
증령방%풍단%왕방%시전
对象文件系统%线性时序逻辑%智能存储%性质验证
對象文件繫統%線性時序邏輯%智能存儲%性質驗證
대상문건계통%선성시서라집%지능존저%성질험증
基于线性时序逻辑,给出了对象文件系统特性的形式化描述.对象文件系统时序逻辑(OFSTL)是线性时序逻辑在描述对象文件系统应用中的一个推广.用OFSTL描述对象文件系统的性质,用模型化的状态迁移系统表示对象文件系统的访问行为.试图解决目前对象文件系统研究存在的问题: ①关注提升对象文件系统性能和功能,但是以增加对象文件系统复杂性为代价; ②很少针对对象文件系统精确描述,缺乏形式化的辅助,妨碍从细节上考查对象文件系统的正确性.
基于線性時序邏輯,給齣瞭對象文件繫統特性的形式化描述.對象文件繫統時序邏輯(OFSTL)是線性時序邏輯在描述對象文件繫統應用中的一箇推廣.用OFSTL描述對象文件繫統的性質,用模型化的狀態遷移繫統錶示對象文件繫統的訪問行為.試圖解決目前對象文件繫統研究存在的問題: ①關註提升對象文件繫統性能和功能,但是以增加對象文件繫統複雜性為代價; ②很少針對對象文件繫統精確描述,缺乏形式化的輔助,妨礙從細節上攷查對象文件繫統的正確性.
기우선성시서라집,급출료대상문건계통특성적형식화묘술.대상문건계통시서라집(OFSTL)시선성시서라집재묘술대상문건계통응용중적일개추엄.용OFSTL묘술대상문건계통적성질,용모형화적상태천이계통표시대상문건계통적방문행위.시도해결목전대상문건계통연구존재적문제: ①관주제승대상문건계통성능화공능,단시이증가대상문건계통복잡성위대개; ②흔소침대대상문건계통정학묘술,결핍형식화적보조,방애종세절상고사대상문건계통적정학성.
