HSTM软件设计中特定执行路径检测算法及实现

发布时间：2020-04-19 23:07

【摘要】：软件系统在未来的城市建设中发挥着非常重要的作用,因此保证其功能正确性是进行软件开发的关键因素。层次状态迁移矩阵(Hierarchical State Transition Matrix,HSTM)是一种流行的软件设计语言,被广泛应用于嵌入式软件设计中。对于具有复杂层次结构及调用关系的HSTM设计,其执行路径通常难以跟踪和调试,如果HSTM设计中的特定变量的首次值变化到其后续引用的执行路径(称为更改-引用路径)能够自动的被输出,那么这些路径可以帮助HSTM设计者更好的跟踪变量的变化及使用情况,并分析潜在错误的成因,从而有利于开发出功能正确及稳定的软件。目前尚未有针对HSTM设计的更改-引用路径检测算法及工具实现。本文基于形式验证中的状态空间搜索技术,提出了针对HSTM软件设计中更改-引用路径的检测算法;针对状态空间探索中存在的状态空间爆炸问题(即状态数目过多导致探索无法在有限时间内利用有限计算资源完成),利用无状态显式搜索(Stateless Explicit State Exploration,SESE)以及限界上下文切换(Bounded Context Switch,BCS)技术来有效缓解状态空间爆炸问题;此外,在对更改-引用路径进行检测时,需要对HSTM设计进行死锁检查以及阈值检查,以避免输出错误的检测结果。算法的大致步骤如下:首先对HSTM设计进行解析,将其转换成一个状态迁移系统;其次将用户输入的更改-引用路径规约进行解析;然后利用显式状态空间搜索技术对HSTM对应的状态迁移系统进行路径检测,通过SESE技术记忆每个时间步的可达状态集,利用BCS技术限制到达当前状态集的进程间切换数;如果到达某个状态时检测到了更改-引用路径则输出到达该状态的详细转换路径,否则输出结果显示为无。本文将提出的更改-引用路径检测算法在课题组前期开发的Garakabu2形式化模型检测工具中进行了实现。除算法本身外,设计实现了更改-引用路径规约描述的解析功能,最短更改-引用路径的输出功能。实验结果表明,本文提出的算法能够对复杂HSTM软件设计中的更改-引用路径进行有效检测及输出,对设计者开发出正确的HSTM软件设计可以起到显著的帮助作用。
【学位授予单位】：大连理工大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP311.52

【参考文献】

相关期刊论文 前9条

1 魏欧;石玉峰;徐丙凤;黄志球;陈哲;;软件模型检测中的抽象模型研究综述[J];计算机研究与发展;2015年07期

2 金继伟;马菲菲;张健;;SMT求解技术简述[J];计算机科学与探索;2015年07期

3 侯刚;周宽久;勇嘉伟;任龙涛;王小龙;;模型检测中状态爆炸问题研究综述[J];计算机科学;2013年S1期

4 孙宏旭;邢薇;陶林;;基于有限状态机的模型转换方法的研究[J];计算机技术与发展;2012年02期

5 樊晓光;褚文奎;张凤鸣;;软件安全性研究综述[J];计算机科学;2011年05期

6 赵艳红;郭银章;白尚旺;;基于时间解耦的分布对象中间件异步通信消息转换机制研究[J];计算机应用与软件;2008年10期

7 袁志斌;;软件开发的形式化方法[J];电脑与电信;2008年07期

8 周修毅;赵建华;李宣东;郑国梁;;实时系统的模型检验中针对共享变量的优化技术[J];计算机科学;2005年07期

9 林惠民,张文辉;模型检测:理论、方法与应用[J];电子学报;2002年S1期

，

本文编号：2633838