将代码静态分析提高一个层次,Coverity提出布尔可满足性概念

2007-10-15 09:03:30来源: 电子工程专辑

布尔可满足性(Boolean satisfiability)的概念正在被用于确定软件代码中的“bug”,从而保证代码基本上不存在bug,满足编程者的愿望。

在2007年嵌入系统会议上,Coverity宣布了据称是第一种基于布尔可满足性(SAT)的源代码分析引擎。Coverity公司的SAT引擎利用了它的软件DNA图谱,自动、正确和精确地确定源代码中的缺陷。该软件DNA图谱精确地代表人们已写出来的任何软件。

Coverity在企业应用领域是领导厂商。它的静态分析软件客户包括财富500强上面57%的软件公司和50%的电脑外设公司。它的主要产品是Prevent Software Quality System (SQS),SQS通过在编译时解析源代码来使复杂软件中的缺陷和安全漏洞检测实现自动化。

目前的静态分析引擎依赖数据流分析和多个检验程序来确定软件缺陷。与此不同的是,SAT引擎基于布尔可满足性,将能支持多个解算程序确定软件缺陷。

这种新的软件代码分析方法,得益于Coverity正在申请专利的技术,该技术以精确到位(bit)的精度代表软件系统,每个相关软件运算都被翻译成布尔值真(true)与假(false)和布尔运算符(Not逻辑非)、and(逻辑与)、or(逻辑或)。这允许利用基于SAT的解算程序对源代码进行分析,这在商业电脑编程领域还是第一次。

300多家客户已经在依靠Coverity Prevent SQS来分析其应用程序中的每个路径。通过利用SAT,Prevent SQS不仅能够分析每个路径,而且能够分析这些路径之中每次计算中的每个值。Chelf表示,这样彻底的静态代码分析,实现了业内对关键性能和安全漏洞的最精确鉴定。

据Forrester Research的安全与风险管理部门的首席分析师Chenxi Wang,“可满足性”原理用于硬件检验已有一段时间,但以前从未用于软件检验。

Wang认为,还有创新空间,具体而言是在嵌入软件领域。“嵌入软件通常在复杂性和状态数量方面比普通应用软件受到的限制多一点,因此,SAT更可能在嵌入编程领域增强软件验证的水平。”

Coverity的Chelf表示,“静态分析方法一直成功地用于EDA产业。我们只是把电路设计工作中使用的同样的软件布尔原理用于软件代码领域。”

Coverity Prevent SQS的基础技术是20世纪90年代在斯坦福大学电脑系统实验室开发出来的,当时在此工作的Ben Chelf和同事把该技术用于商业应用。

关键字:引擎  图谱  编程  编译

编辑: 引用地址:http://www.eeworld.com.cn/news/embed/200710/16215.html
本网站转载的所有的文章、图片、音频视频文件等资料的版权归版权所有人所有,本站采用的非本站原创文章及图片等内容无法一一联系确认版权者。如果本网所选内容的文章作者及编辑认为其作品不宜公开自由传播,或不应无偿使用,请及时通过电子邮件或电话通知我们,以迅速采取适当措施,避免给双方造成不必要的经济损失。
论坛活动 E手掌握
微信扫一扫加关注
论坛活动 E手掌握
芯片资讯 锐利解读
微信扫一扫加关注
芯片资讯 锐利解读
推荐阅读
全部
引擎
图谱
编程
编译

小广播

独家专题更多

富士通铁电随机存储器FRAM主题展馆
富士通铁电随机存储器FRAM主题展馆
馆内包含了 纵览FRAM、独立FRAM存储器专区、FRAM内置LSI专区三大部分内容。 
走,跟Molex一起去看《中国电子消费品趋势》!
走,跟Molex一起去看《中国电子消费品趋势》!
 
带你走进LED王国——Microchip LED应用专题
带你走进LED王国——Microchip LED应用专题
 

About Us 关于我们 客户服务 联系方式 器件索引 网站地图 最新更新 手机版

站点相关: 数字电视 安防电子 医疗电子 物联网

北京市海淀区知春路23号集成电路设计园量子银座1305 电话:(010)82350740 邮编:100191

电子工程世界版权所有 京ICP证060456号 京ICP备10001474号 电信业务审批[2006]字第258号函 京公海网安备110108001534 Copyright © 2005-2016 EEWORLD.com.cn, Inc. All rights reserved