科学网—ymin的博文 - 第6页

设为首页收藏本站

开启辅助访问切换到宽版

科学网 › 我的中心 › 博文 › ymin的博文

ymin

https://wap.sciencenet.cn/?290937

学术导航| 做学问| 微电子| 计算机| 科研管理| 杂谈| 网络|

模型检验（4）（091231）: 闵应骅 2009-12-31 17:25; 模型检验（4）（091231）闵应骅模型检验的成功之处在于它用自动搜索代替手动证明来解决验证的问题。模型检验包括三部分：1。基于命题时态逻辑的规范语言，2。表示被验证系统的编码状态机的方法，3。验证算法，对状态空间的智能搜索以确定规范是真还是假。如果规范没有被实现，模型检验能够给出反例。 ...; 个人分类: 学术导航|6453 次阅读|没有评论

模型检验（3）（091231）: 闵应骅 2009-12-31 11:36; 模型检验（3）（091231）闵应骅时态逻辑用来描述正确的系统行为，模型检验提供实用的硬件和软件验证方法。模型验证可形式地描述如下：给定一个有限结构M，状态s，和一个时态逻辑公式，问M, s |= f ?即问：在结构M中，于状态s0，f是否为真？或者说，给定M和f,计算这个集合{s : M, s |= f}。他们证明了 ...; 个人分类: 学术导航|4777 次阅读|没有评论

模型检验（2）（091231）: 闵应骅 2009-12-30 17:17; 模型检验（2）（091231）闵应骅程序正确性的形式验证依靠数学逻辑的使用。程序是一个很好定义了的、可能很复杂、直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去，人们倾向于正确性的形式证明。而模型检验回避了这种证明。在上世纪60年代，流行的是佛洛伊德-霍尔式的演绎验证。这种办法 ...; 个人分类: 学术导航|5352 次阅读|没有评论

模型检验（1）（091230）: 闵应骅 2009-12-30 10:23; 模型检验（1）(091230）闵应骅大家承认，计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke，E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术，用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足，则提供 ...; 个人分类: 学术导航|5496 次阅读|没有评论

社会网络（091212）: 闵应骅 2009-12-13 11:51; 社会网络（091212）闵应骅我一直有一个疑问：为什么google搜索这么快？我们平时上网，给定了web地址以后，有时要好久才能上去。而google上去得特别快。设定搜索短语以后，又很快出来大量搜索的结果，而且不是胡说八道。而上IEEE或ACM数字图书馆搜索就要慢得多。康内尔大学计算机系的Jon Kleinberg也 ...; 个人分类: 学术导航|4157 次阅读|1 个评论

三个因素影响浏览器安全（090905）: 闵应骅 2009-9-5 10:54; 三个因素影响浏览器安全闵应骅我并不欣赏笼统地来谈信息安全，例如，信息要有几个性、信息安全的定义是什么等等。我觉得，对于学术研究来说，现在的问题是：我们用什么技术能够提高我们信箱系统的安全水平。至于用字符串匹配去堵网站、堵文件，那是工程任务，也许是政府下 ...; 个人分类: 学术导航|3758 次阅读|没有评论

静下心来，思考安全问题(090810): 闵应骅 2009-8-10 09:28; 静下心来，思考安全问题闵应骅信息安全热得烫手互联网普及以来，人们真正进入了信息社会。信息安全的问题突现出来。国家、企业和个人都受到安全威胁，都想采取有力措施，解决各种信息安全问题。从中央到地方，中央各部委都列出课题，研究信息安全问题。公司开发安全芯片， ...; 个人分类: 学术导航|3586 次阅读|没有评论

请不要将信任计算混同于可信计算: 闵应骅 2009-8-3 14:30; 请不要将信任计算混同于可信计算闵应骅 2009/7/20-22在海拉尔召开的第13届全国容错计算学术会议上，专门举办了一个关于可信和安全计算的未来的讨论会，邀请了美国卡内基梅隆大学Daniel P. Siewiorek教授（美国工程院院士，IEEE Fellow, ACM Fellow, AAAS Fellow）,法国国家科学院系统结 ...; 个人分类: 学术导航|6712 次阅读|没有评论

会议

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

GMT+8, 2024-4-19 20:19

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部