期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

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

Formalizing Description of Object File System Based on Linear Temporal Logic
下载PDF
导出
摘要 基于线性时序逻辑,给出了对象文件系统特性的形式化描述.对象文件系统时序逻辑(OFSTL)是线性时序逻辑在描述对象文件系统应用中的一个推广.用OFSTL描述对象文件系统的性质,用模型化的状态迁移系统表示对象文件系统的访问行为.试图解决目前对象文件系统研究存在的问题: ①关注提升对象文件系统性能和功能,但是以增加对象文件系统复杂性为代价; ②很少针对对象文件系统精确描述,缺乏形式化的辅助,妨碍从细节上考查对象文件系统的正确性.
作者 曾令仿 冯丹 王芳 施展
机构地区 华中科技大学计算机科学与技术学院
出处 《计算机研究与发展》 EI CSCD 北大核心 2007年第z1期154-160,共7页 Journal of Computer Research and Development
基金 国家自然科学基金项目(60303032,60603048) 国家发改委CNGI基金项目(CNGI-04-5-1D) 国家"九七三"重点基础研究发展规划基金项目(2004CB318201)
关键词 对象文件系统 线性时序逻辑 智能存储 性质验证
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献17

  • 1[1]M Mesnier,G R Ganger,E Riedel.Object-based storage.Communications Magazine,IEEE,2003,41(8):84-90
  • 2[2]M Satyanarayanan.A survey of distributed file systems.Annual Review of Computer Science.Annual Reviews,Inc,1989
  • 3[3]T Yokogawa,T Tsuchiya,T Kikuno.Automatic verification of fault tolerance using model checking.In:Proc of Pacific Rim Int'l Symp on Dependable Computing.2001.95-102
  • 4[4]Matthias Sivathanu,Lakshmi Bairavasundaram,Andrea C Arpaci-Dusseau,et al.Database-aware semantically-smart storage.The 4th USENIX Symp on File and Storage Technologies (FAST'05),San Francisco,California,2005
  • 5[5]Z Manna,A Pnueli.The Temporal Logic of Reactive and Concurrent Systems:Specification.Berlin:Springer-Verlag,1992
  • 6[6]E M Clarke,E A Emerson,A P Sistla.Automatic verification of finite state concurrent systems using temporal logic specifications.In:Proc of the 10th Annual ACM Symp on Principles of Programming Languages.New York:ACM Press,1983.117-126
  • 7[7]C Stirling,D Walker.Local model checking in the modal Mucalculus.In:Proc of the 3rd Int'l Joint Conf on Theory and Practice of Software Development.Berlin:Springer-Verlag.1989.369-383
  • 8[8]L Lamport.The temporal logic of actions.ACM Trans on Programming Languages and Systems,1994,16(3):872-923
  • 9李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证[J].软件学报,2002,13(1):33-41. 被引量：16
  • 10[10]P C Attie,N A Lynch.Dynamic input/output automata,a formal model for dynamic systems.The Int'l Conf on Concurrency Theory,Aalborg,Denmark 2001,2001

二级参考文献14

  • 1Alur, R., Henzinger, T.A. Real-Time system=discrete system+clock variables. Software Tools for Technology Transfer, 1997, 1(1/2): 86～109.
  • 2de Bakker, J.W., Huizing, K., de Rover, W.-P, et al, eds. Proceedings of the REX Workshop 'Real-Time: Theory in Practice'. Lecture Notes in Computer Science 600, New York: Springer-Verlag, 1991.
  • 3Henzinger, T.A., Manna, Z., Pnueli, A. Temporal proof methodologies for timed transition systems. Information and Computation 1994,112(2):273～337.
  • 4Manna, Z., Pnueli, A. Clocked transition systems. In: Pnueli, A., Lin, H., eds. Logic and Software Engineering. Singapore: World Scientific, 1996. 3～42.
  • 5Alur, R., Courcoubetis, C., Dill, D.L. Model-Checking in dense real-time. Information and Computation, 1993,104(1):2～34.
  • 6Alur, R., Feder, T. Henzinger, T.A. The benefits of relaxing punctuality. Journal of the ACM, 1996,43(1):116～146.
  • 7Alur, R., Henzinger, T.A. A really temporal logic. Journal of the ACM, 1994,41(1):181-204.
  • 8Ostroff, J.S. Temporal logic for real-time systems. Taunton, England: Research Studies Press Ltd., 1989.
  • 9Alur, R., Dill, D.L. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183-235.
  • 10Manna, Z., Pnueli, A. The temporal logic of reactive and concurrent systems: Specification. New York: Springer-Verlag, 1992.

共引文献15

计算机研究与发展
2007年 第z1期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部