科学网

 找回密码
  注册
搜索
热搜: 科学 论文
搜索
模型检验(3)(091231)
闵应骅 2009-12-31 11:36
模型检验(3)(091231) 闵应骅 时态逻辑用来描述正确的系统行为,模型检验提供实用的硬件和软件验证方法。模型验证可形式地描述如下:给定一个有限结构M,状态s,和一个时态逻辑公式,问M, s |= f ?即问:在结构M中,于状态s0,f是否为真?或者说,给定M和f,计算这个集合{s : M, s |= f}。他们证明了 ...
个人分类: 学术导航|4050 次阅读|没有评论
模型检验(2)(091231)
闵应骅 2009-12-30 17:17
模型检验(2)(091231) 闵应骅 程序正确性的形式验证依靠数学逻辑的使用。程序是一个很好定义了的、可能很复杂、直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去,人们倾向于正确性的形式证明。而模型检验回避了这种证明。在上世纪60年代,流行的是佛洛伊德-霍尔式的演绎验证。这种办法 ...
个人分类: 学术导航|4222 次阅读|没有评论
模型检验(1)(091230)
闵应骅 2009-12-30 10:23
模型检验(1)(091230) 闵应骅 大家承认,计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke,E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术,用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足,则提供 ...
个人分类: 学术导航|4608 次阅读|没有评论
社会网络(091212)
闵应骅 2009-12-13 11:51
社会网络(091212) 闵应骅 我一直有一个疑问:为什么google搜索这么快?我们平时上网,给定了web地址以后,有时要好久才能上去。而google上去得特别快。设定搜索短语以后,又很快出来大量搜索的结果,而且不是胡说八道。而上IEEE或ACM数字图书馆搜索就要慢得多。康内尔大学计算机系的Jon Kleinberg也 ...
个人分类: 学术导航|3379 次阅读|1 个评论
三个因素影响浏览器安全(090905)
闵应骅 2009-9-5 10:54
三个因素影响浏览器安全 闵应骅 我并不欣赏笼统地来谈信息安全,例如,信息要有几个性、信息安全的定义是什么等等。我觉得,对于学术研究来说,现在的问题是:我们用什么技术能够提高我们信箱系统的安全水平。至于用字符串匹配去堵网站、堵文件,那是工程任务,也许是政府下 ...
个人分类: 学术导航|3040 次阅读|没有评论
静下心来,思考安全问题(090810)
闵应骅 2009-8-10 09:28
静下心来,思考安全问题 闵应骅 信息安全 热得烫手 互联网普及以来,人们真正进入了信息社会。信息安全的问题突现出来。国家、企业和个人都受到安全威 胁,都想采取有力措施,解决各种信息安全问题。从中央到地方,中央各部委都列出课题,研究信息安全 问题。公司开发安全芯片, ...
个人分类: 学术导航|2852 次阅读|没有评论
请不要将信任计算混同于可信计算
闵应骅 2009-8-3 14:30
请不要将信任计算混同于可信计算 闵应骅 2009/7/20-22在海拉尔召开的第13届全国容错计算学术会议上,专门举办了一个关于可信和安全计算的未来的讨论会,邀请了美国卡内基梅隆大学Daniel P. Siewiorek教授(美国工程院院士,IEEE Fellow, ACM Fellow, AAAS Fellow),法国国家科学院系统结 ...
个人分类: 学术导航|5074 次阅读|没有评论

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2021-4-19 08:27

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部