注册
登录
| 关键词： 系统 档案 验证 图式 程式 形式 研究人员 语言 臭虫 电脑 |
三名来自麻省理工学院（MIT）电子工程系（EECS）的研究人员利用形式验证（formal verification）的程序建立了一个即使电脑突然当掉也不会造成资料遗失的档案系统，相关研究成果并准备在今年10月举行的作业系统学术会议ACM Symposium on Operating Systems Principles（SOSP）上发表。 MIT电子工程系副教授Nickolai Zeldovich表示，很多人都担心档案系统的稳定性，不论是在正常运作的状况下，或是在电脑当机、电源故障、硬体故障，或是软体出现臭虫的时候，而且使用者还会发现，就算是经过严谨测试的档案系统，其当机复原功能亦存在着许多臭虫，因为这并不是件容易的事。 所谓的形式验证是以数学方法描述电脑程式运作时可以接受的「绑定」（bounds），且证明它绝不会超出这些绑定。这是个复杂的程序，因此多半只应用在描绘程式功能的高阶图式（schema）上，将这些图式转换成程式码可能会带来相关验证未能解决的各种复杂问题。 MIT研究人员则是直接验证档案系统的程式码，而非高阶图式，他们透过名为Coq的验证助理工具，以其形式语言描述电脑系统的各个组件与它们之间的关联。由于此一形式验证环境包含了程式语言，在此环境中以同样的语言撰写档案系统，就能让验证程序检查真正的程式码而非图式。 研究人员先以Coq的形式语言定义此一档案系统的各种元件，然后还得描述这些元件在遭遇当机情况时的行为与彼此间的关联，之后才进行系统验证，并写出相对应的档案系统。 此一新的档案系统将能保证使用者不会因为系统当掉而遗失资料，即使受限于今日的标准而使得该档案系统运作缓慢，但研究人员宣称他们所使用的技术将可适用于更精密的设计，形式验证最终将让打造可靠及有效率的档案系统变得更容易。 |
|
声明：文章版权归原作者所有 部分文章转自互联网 如有侵权请联系
[邮箱地址] 删除
|
