发新帖我要提问
返回列表
打印

Polyspace 使关键代码安全可靠

[复制链接]
5055|6
手机看帖
扫描二维码
随时随地手机跟帖
跳转到指定楼层
楼主
gaoyang9992006|  楼主 | 2018-8-15 21:24 | 只看该作者 |只看大图 回帖奖励 |倒序浏览 |阅读模式
space, 代码, Lab, 安全漏洞, 组件

Polyspace
®
  静态代码分析产品使用形式化方法来证明一切可能的控制流和数据流在缺乏关键的运行时错误。它们包括用于编码规则的检查程序，安全漏洞，代码指标以及数百种其他类型的错误。

https://ww2.mathworks.cn/products/polyspace.html

今天新发现的一个组件。今天我重装了MATLAB2018A发现的



使用特权

评论回复 赏

相关下载

相关帖子
沙发
gaoyang9992006|  楼主 | 2018-8-15 21:25 | 只看该作者

大家可以探索一下。

使用特权

评论回复 赏
板凳
gaoyang9992006|  楼主 | 2018-8-15 21:27 | 只看该作者
证明软件中不存在运行时错误
Polyspace Code Prover™ 作为一款可靠的静态分析工具，能够证明在C 和 C++ 源代码中不存在溢出、除零、数组访问越界以及其它运行时错误。整个分析过程无需执行程序、植入代码，或运行测试用例。Polyspace Code Prover 使用基于形式化方法的语义分析和抽象解释验证软件程序交互、控制和数据流的行为。你可以用于手写代码、生成代码或二者的混合代码。每项检查均在代码上着色表示是否无运行时错误、已证明有问题、不可达或有待进一步分析。
Polyspace Code Prover 亦能显示变量和函数返回值的范围信息，并可以证明变量是否超出指定范围限制。这些结果可以发布到看板上，以跟踪质量指标并确保符合软件质量目标。Polyspace Code Prover 还可以集成到编译生成系统中以执行自动验证。
通过IEC Certification Kit（适用于 IEC 61508 和 ISO 26262）和 DO Qualification Kit（适用于 DO-178）可以提供对行业标准的支持。此外，它还可以支持 Ada 语言。





使用特权

评论回复 赏
地板
gaoyang9992006|  楼主 | 2018-8-15 21:28 | 只看该作者

功能还是很强大的。

使用特权

评论回复 赏
5楼
gaoyang9992006|  楼主 | 2018-8-15 21:30 | 只看该作者


使用特权

评论回复 赏
6楼
gaoyang9992006|  楼主 | 2018-8-15 21:33 | 只看该作者

再说一次最新版的好处：你不用记绘图函数了

选择你要表现的数据点对应的图就行了。然后可以设置不同数据对应的坐标轴。

使用特权

评论回复 赏
7楼
lyfly_away| | 2020-8-20 10:26 | 只看该作者
请教下这种静态代码解析问题要怎么解决呢？ 就是bootloader跳转到app，调用了一个绝对地址跳转，要怎么写才不会违反规则？  谢谢！



使用特权

评论回复 赏
返回列表
发新帖 我要提问
高级模式
B Color Image Link Quote Code 收费 Smilies
您需要登录后才可以回帖 登录 | 注册

本版积分规则

gaoyang9992006 Image Image
认证：西安公路研究院南京院
简介：主要工作从事监控网络与通信网络设计，以及从事基于嵌入式的通信与控制设备研发。擅长单片机嵌入式系统物联网设备开发，音频功放电路开发。

1961

主题

15931

帖子

208

粉丝