当前时区为 UTC + 8 小时



发表新帖 回复这个主题  [ 2 篇帖子 ] 
作者 内容
1 楼 
 文章标题 : Verve:一个类型安全的操作系统
帖子发表于 : 2010-12-11 9:56 
头像

注册: 2010-10-18 14:39
帖子: 677
送出感谢: 0 次
接收感谢: 1
Verve:一个类型安全的操作系统
发表于:2010-12-10 23:22 UTC

“Singularity(一个用用于调查目的的代码写成的操作系统)项目提供了几个非常有用的调查结果,为操作系统的设计开辟了新的探索之路。最近,微软研究院发布了一个描述一个操作系统调查项目的文件,它寻求出了一个新的、用可检验与类型安全的管理代码建造OS栈的途径。此项目以新奇的方式使用了类型化汇编语言;后者即为你从字面意思理解到的——带型(以注释形式实现,使用Boogie认证技术和定理谁器Z3(Boogie生成出认证条件,之后它们会被Z3静态证明。Boogie同时也是一个用于编译其他语言的程序认证器的语言)静态认证)汇编语言。Singularity中,C# Bartok编译器也被使用了,不过这次它生成的是TAL(事物处理应用语言)。整个OS栈经证实是类型安全的(其Nucleus本质上是Verve HAL),并且所有对象都可被垃圾回收。这并没有使用进程隔离的SIP(SIP是一个计算机网络中应用层的信令控制协议)模型(像Singularity)。这种情况下,整个操作系统再次被确保是类型安全的,并使用世界级定理认明器被静态认证。Channel9有一个与其中一位开发者有关他该项目的视频采谈。Verve源码可用。

英文原文:http://www.osnews.com/story/24115/Ver ... ype_Safe_Operating_System
转载请注明:Linux人社区 英文资讯翻译专版 编译
http://www.linux-ren.org/modules/newbb/viewtopic.php?topic_id=58134&post_id=320003#forumpost320003


_________________
Linux人社区开源新闻资讯翻译专版小编。翻译来自互联网上最新的英文开源资讯,提供给大家最迅即、最忠实于原文的开源业界动态、软件更新、有用技能等等。不至之处欢迎指正!xyxzfj@gmail.com


页首
 用户资料  
 
2 楼 
 文章标题 : Re: Verve:一个类型安全的操作系统
帖子发表于 : 2010-12-11 10:54 

注册: 2009-04-17 13:15
帖子: 2
送出感谢: 0 次
接收感谢: 0 次
:em04 :em04 顶起来


页首
 用户资料  
 
显示帖子 :  排序  
发表新帖 回复这个主题  [ 2 篇帖子 ] 

当前时区为 UTC + 8 小时


在线用户

正在浏览此版面的用户:没有注册用户 和 2 位游客


不能 在这个版面发表主题
不能 在这个版面回复主题
不能 在这个版面编辑帖子
不能 在这个版面删除帖子
不能 在这个版面提交附件

前往 :  
本站点为公益性站点,用于推广开源自由软件,由 DiaHosting VPSBudgetVM VPS 提供服务。
我们认为:软件应可免费取得,软件工具在各种语言环境下皆可使用,且不会有任何功能上的差异;
人们应有定制和修改软件的自由,且方式不受限制,只要他们自认为合适。

Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group
简体中文语系由 王笑宇 翻译