没有合适的资源?快使用搜索试试~ 我知道了~
首页C2edl软件:SMV垃圾收集机制应用与bug分析实例
本文主要探讨了SMV(Session Markov Variables)垃圾收集机制在C语言编程环境下的应用,以及通过C2edl软件工具进行模型检查的方法。C2edl是一个将ANSI-C代码转换为RuleBase模型检查器输入语言EDL(Expressive Data Language)的工具。作者指出,C2edl采取了一种激进的抽象策略,以解决软件模型检查中的复杂性问题,这使得分析SMV的垃圾收集机制成为可能。 C2edl的优势在于它利用了现有的硬件设计模型检查技术,避免了专门为软件开发新工具所需的时间和资源投入。尽管C2edl的抽象可能会简化问题,但实际应用中,它构建的模型依然能够有效捕捉SMV的垃圾收集机制的细节。通过使用C2edl和RuleBase,研究者在RuleBase自身中发现了8个bug,这些bug都与相同的垃圾收集机制有关。 文章的结构清晰,首先回顾了相关工作,强调了模型检查在软件验证中的重要性和当前的研究趋势。随后,章节介绍了规则库的基本概念,接着详细解释了如何将程序转换为符号模型检验的形式以便于C2edl处理。第五节深入讨论了C2edl的具体功能和使用方法,而第六节则是核心部分,展示了在SMV垃圾收集机制上的具体应用实例和实验结果。 这篇论文提供了一种实用的方法,即利用C2edl工具对复杂的ANSI-C代码进行模型检查,以发现和分析SMV垃圾收集机制中的潜在问题。这对于理解和改进软件设计,尤其是在处理内存管理这类关键任务时,具有重要的实践价值。同时,它也揭示了模型检查作为一种现有工具的扩展应用,对于提升软件质量的潜力。
资源详情
资源推荐
![](https://csdnimg.cn/release/download_crawler_static/88730109/bg4.jpg)
艾斯
纳
4
3
预赛
本文中描述的工作是使用
RuleBase [6]
进行的。
RuleBase
最初基于
SMV
的一
个版本
[32]
。经过八年的发展
[4
,
8
,
3
,
9
,
7
,
5
,
6
,
21]
,原始
SMV
代码
只是整个代码的一小部分。然而,
SMV
的垃圾收集机制仍然存在。
RuleBase
的输入语言是
EDL
,它是
SMV
语言的一种方言。
RuleBase
使
用时态逻辑
Sugar [4]
作为其规范语言。
Sugar
结合了正则表达式和
CTL
的
语法加糖功能。本文所描述的工作只使用了一种
Sugar
公式,一个
Sugar
蕴涵。非正式地,这样的公式由两部分组成:
序列
和
必需条件
。一个序列
是一个计算路径的前缀,被描述为一个正则表达式。一个必要的条件是
一个糖公式,它需要在序列的每个最终状态中保持。 例如,下面的糖
公式:
(
1
)
f
true
[]
;
a
;b
[]
;
c
[+]
g
(
d
)
声明
d
需要保持在正则表达式
ab c+
描述的每个序列的
nal
状态。等效的
CTL
公式为:
(2)
:
EF
(
a
^
EX
E
[
b
U
E
[
c
U
(
c
^
:
d
)
]]
)
4
将程序表示为一组下一状态函数
将程序转换为一组适合模型检查的下一状态函数的过程类似于
[31
,
13]
。 我们以一个简单的例子来非正式地描述它,然后添加细节。考虑
图
1
中的
C
函数
getmax
()。我们用程序计数器(
pc
)的值来注释代码
如果我们将整数
a
和
max
限制在
0
到
3
的范围内,那么我们可以
int max
()
;
0
int max = 0;
1
多
夫
2
if
(
a
>
max
)
3
return a;
4
int maximum
()
;
5
g while
(
a
)
;
6
return
(
max
)
;
7 G
Fig. 1.
函数
getmax
()
按照变量的下一状态函数重写
getmax
(),如下所示 在图
2
中我们已经
将对
a=input
()的调用表示为对变量
a
的非确定性赋值。其他变量的下一
个状态函数是确定性的。为了简单起见,我们忽略了翻译
return
语句的
细节(下面有一个包含函数调用的例子)。通过轻微的语法更改和添加
状态变量声明,图
2
是一个完整的
SMV
或
EDL
程序,可以使用
SMV
或
RuleBase
进行模型检查
剩余18页未读,继续阅读
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![.pdf](https://img-home.csdnimg.cn/images/20210720083646.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 展开
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
最新资源
- Vue实现iOS原生Picker组件:详细解析与实现思路
- Arduino蓝牙小车:参数调试与功能控制
- 百度Java面试精华:200页精选资源涵盖核心知识点
- Swift使用CoreData填坑指南:CoreData在Swift 3.0的变化
- 微距离无线充电器创新设计及其实验探索
- MTK Android平台开发全攻略:44步详解流程
- RecyclerView全面解析:替代ListView的新选择
- Android开发:自动适配中英文键盘解决方案
- Android调用WebService接口教程
- Android开发:BitmapUtil图片处理全解析与实例
- Android多线程断点续传实现详解
- PCA算法在人脸识别会议签到系统中的应用
- EventBus 3.0:Android事件总线详解与实战应用
- Android FileUtil:全面解析文件操作实用技巧与实例
- RecyclerView添加头部和尾部实战教程
- Android实现微博滑动固定顶部栏实战与优化
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)