微软又在搞一个新的软件模型验证软件
2004-07-09 10:57
281 查看
微软研究院又推出一个新的模型验证软件,zing。粗略看了下关于zing的介绍,好像卖点在能处理更大型的模型,有一套通用的框架。也就是说工程方面有亮点。但没看出理论上有什么特别的地方。
先简单地科普一下什么是软件模型检验。简单的说,就是用程序来自动检测一个软件,或者一个软件模型(比如一套UML模型),是否正确。自动的检测的好处是详尽,不象测试,总是有所遗漏(不要忘了E.W.Dijkstra大牛名言哈:测试只能证明错误的存在,但不能证明错误的不错在);自动,不需要人的干预;而且严格,少有模糊和二义。听上去好像不太现实?呵呵,早就有现成的检验软件了,比如smv, nuMSV,和SPIN。微软甚至用SLAM自动分析Windows驱动程序,并发现了好些隐蔽很深的错误。模型检验软件的研究和开发和普通的软件开发也颇不一样。模型检验的研究模式是自底向上的:先由严格的定义,然后定理,最后根据定理推出严格的算法。反观系统研究,往往是启发式居多。至于哪个更有效,就见仁见智乐。
其实硬件公司早就在应有模型检查了。毕竟靠测试很难确保关键系统万无一失。象Motorola, IBM, Intel, NASA, Lockheed等都花了不少钱在各种模型检查软件上。
好像现在软件越来越关注模型检验了。毕竟从理论上来说,如果能够在建模阶段(需求分析,功能规划)就发现错误的话,比在测试阶段发现错误要经济得多。或者如果能够自动检查代码,发现错误,并生成产生错误的例子,岂不快哉(多少程序员的梦想啊!:-)。包括Tony Hoare这样的巨牛?(quick sort的发明人,Algo60的作者,Hoare Logic的作者)也在微软研究能自动查错的编译器的说。1996年,以色列牛人A.Pnueli获得图灵奖,就是因为在模型检测的基础理论,时序逻辑,方面做出了开创性贡献。唐稚松院士也是这方面的高手,据说和A.Pnueli的私交也不错。
最后说说模型检验的理论基础。主要就是时序逻辑了。想想看,可以用严格的逻辑来推导和时间有关的东西,还是很酷的。其次就是布尔代数,格点代数,和自动机理论了(不是编译理论用的有限自动机哈,而是无限自动机)。//sigh, 悔当初不好好学数学啊。
先简单地科普一下什么是软件模型检验。简单的说,就是用程序来自动检测一个软件,或者一个软件模型(比如一套UML模型),是否正确。自动的检测的好处是详尽,不象测试,总是有所遗漏(不要忘了E.W.Dijkstra大牛名言哈:测试只能证明错误的存在,但不能证明错误的不错在);自动,不需要人的干预;而且严格,少有模糊和二义。听上去好像不太现实?呵呵,早就有现成的检验软件了,比如smv, nuMSV,和SPIN。微软甚至用SLAM自动分析Windows驱动程序,并发现了好些隐蔽很深的错误。模型检验软件的研究和开发和普通的软件开发也颇不一样。模型检验的研究模式是自底向上的:先由严格的定义,然后定理,最后根据定理推出严格的算法。反观系统研究,往往是启发式居多。至于哪个更有效,就见仁见智乐。
其实硬件公司早就在应有模型检查了。毕竟靠测试很难确保关键系统万无一失。象Motorola, IBM, Intel, NASA, Lockheed等都花了不少钱在各种模型检查软件上。
好像现在软件越来越关注模型检验了。毕竟从理论上来说,如果能够在建模阶段(需求分析,功能规划)就发现错误的话,比在测试阶段发现错误要经济得多。或者如果能够自动检查代码,发现错误,并生成产生错误的例子,岂不快哉(多少程序员的梦想啊!:-)。包括Tony Hoare这样的巨牛?(quick sort的发明人,Algo60的作者,Hoare Logic的作者)也在微软研究能自动查错的编译器的说。1996年,以色列牛人A.Pnueli获得图灵奖,就是因为在模型检测的基础理论,时序逻辑,方面做出了开创性贡献。唐稚松院士也是这方面的高手,据说和A.Pnueli的私交也不错。
最后说说模型检验的理论基础。主要就是时序逻辑了。想想看,可以用严格的逻辑来推导和时间有关的东西,还是很酷的。其次就是布尔代数,格点代数,和自动机理论了(不是编译理论用的有限自动机哈,而是无限自动机)。//sigh, 悔当初不好好学数学啊。
相关文章推荐
- 最近用RecurDyn做了一个简单的车辆四轮模型,验证软件能不能做整车仿真
- 我们期待自己成为一个优秀的软件模型设计者,但是,要怎样做,又从哪里开始呢?
- [导入](转贴)我们期待自己成为一个优秀的软件模型设计者,但是,要怎样做,又从哪里开始呢?
- 突然萌生一个念头:抵制微软的一切,IE,Office,XP,.Net FrameWork,SQL Server都是垃圾软件。
- 微软软件开发过程与团队模型
- 成为一个优秀的软件模型设计者
- (转贴)我们期待自己成为一个优秀的软件模型设计者,但是,要怎样做,又从哪里开始呢?
- 我们期待自己成为一个优秀的软件模型设计者,但是,要怎样做,又从哪里开始呢?
- 通过微软版权验证的一个尝试
- 微软竟然发布了一个察看世界杯足球积分榜的软件!
- .Net微软软件开发过程与团队模型
- 一个模型验证工具--pi4soa
- 一个菜鸟浅谈对 软件、程序、软件模型的认识 ——!
- 发现一个微软的免费同步软件 SyncToy
- Mouse without Borders是微软的一个软件实验项目,这款软件可让鼠标自由在局域网中的多台电脑间移动,键盘输入实现无缝切换,还可以直接用鼠标相互拖拽文件。 如果经常需要同时使用两台以
- 一个微软免费的防病毒软件Microsoft Security Essentials
- 『程序员』 [.Net]微软软件开发过程与团队模型
- 测试杯子(微软的一个软件测试面试题目)
- 如何成为一个优秀的软件模型设计者
- 软件开发企业的一个研发、转发与销售之间的微笑模型