【摘 要】
:
软件系统在未来的城市建设中发挥着非常重要的作用,因此保证其功能正确性是进行软件开发的关键因素。层次状态迁移矩阵(Hierarchical State Transition Matrix,HSTM)是一种流
论文部分内容阅读
软件系统在未来的城市建设中发挥着非常重要的作用,因此保证其功能正确性是进行软件开发的关键因素。层次状态迁移矩阵(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软件设计可以起到显著的帮助作用。
其他文献
Letters from Burma是一部英语自传体文学。该书作者记述了昂山素季本人从1995年解除监禁后的相关经历和手记。在上世纪九十年代,昂山素季的非暴力不合作政治理念逐渐萌芽,而佛教思想对其政治理念有深远的影响。本报告选取本书第1到12章,内容包括Road to Thamanya,At Thamanya,The Peacock and the Dragon等章节,意图通过翻译理解佛学思想对原
真空烧结炉作为粉末冶金行业中的重要设备之一,需求量在近年来逐渐增加。在国际上,烧结炉的热效率水平达到了60%左右,而国内的烧结炉热效率水平还不到35%,以致于烧结炉设备的购置方面大多数依赖于进口,所以对高效低能耗的烧结炉设备的研究工作在国内具有较高的应用价值。在提高烧结炉能源利用效率的同时,还需要考虑炉膛内温度均匀性的问题,以确保工件质量。为了解决该问题,本文基于有限元数值模拟技术对烧结炉内的温度
数据挖掘是当前社会中正在蓬勃发展的非常重要的领域,而聚类分析又是数据挖掘中的一个热点问题,聚类分析作为统计学的一个分支,主要借助于统计学习方法、机器学习以及神经网
近年来,随着国际竞争愈发激烈,在经济、国防、军事等硬实力的竞争之外,文化软实力的重要性也日益凸显。长久以来,西方发达国家引领着世界文化发展的趋势与潮流,在此背景下,提升文化软实力成为我们建立文化自信,增强国际影响力的有力途径;随着国家文化旅游部的成立,文旅融合也上升为国家层面的战略思维,进一步推动了产业发展。因此,评价我国文化软实力水平、测度文旅融合程度,并研究两者之间的关系具有十分重要的意义。本
本文依托“河南省渑池县曹窑以西煤下铝青阳沟矿段详查”项目。研究区位于河南省渑池县张村镇西部桑树坪村及其附近,面积1.08km2,属于豫西陕县—渑池—新安铝土矿带的中矿带,
资本市场初期,A股市场壳属于非常稀缺的资源,很少出现公司被强制性退市的情况。与此同时,现有退市制度还未足够成熟,这也会导致企业找到制度漏洞以此逃避退市。直至2018年11月8日,A股市场中出现了第一支因市值低于面值而退市的股票,从此退市制度将迎接“一元退市”的到来。要衡量一个公司是否已经退市,可以通过净利润、营业收入、净资产和收盘价格等直观真实和准确地指标来进行一定的判断,这样才能更好地从一个客观
煤气泄漏是工业场所的重大安全隐患,当泄露发生时,如何快速的找到泄漏源,是一大技术难题。很多工厂在现场安装了自动煤气检测设备,当煤气浓度达到一定阈值即刻发出报警,但该方法没有办法精确定位泄漏点的位置。本文通过模拟工业场所的现场环境,设计了一种便携式设备和无人机共同查找泄漏点的算法,当巡检工作人员携带的便携式设备发出泄漏警报后,系统控制无人机到现场按照一定的路径搜索,以最快速度找到泄漏源。该方法能够为
环境问题,是全球工业快速发展的必然产物之一。上世纪80年代以来,世界范围内以重金属污染为首的环境水体污染事件频发,引起了科研专家、学者的高度关注。重金属在自然界中难被生化降解,一旦经食物链流进人体,极易引发肾脏、肝脏、生殖系统和脑组织等器官损伤。为此先后已有诸如离子交换、膜分离、化学沉淀、电化学和吸附等一批技术手段应用到水体重金属污染治理中,其中吸附法因原材料易得、吸附效率高和对原水重金属离子浓度
研究目的:本体感受性神经肌肉促进法(Proprioceptive Neurmuscular Facilitation,PNF)对提高柔韧性、协调性等的优势已在其他项目中有大量证明,但在羽毛球领域尚未应用研究,本研究将在FMS功能性动作筛查(Functional Movement Screen,FMS)基础上,进行PNF拉伸训练相结合,旨在探索羽毛球教学训练新方法,为羽毛球科学训练提供借鉴。研究方法
镁和镁合金具有良好的阻尼性能、较高的比强度和比弹性模量,然而存在易腐蚀、强度较低的问题。铝和铝合金通常比镁具有更好的成形性和抗腐蚀性能,通过累积叠轧工艺制备镁铝层