基于时间STM的软件形式化建模与验证方法

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.     

软件动态执行网络建模及其级联故障分析

随着人们对软件功能需求的不断增加,软件系统的结构和规模越来越复杂。如何对复杂软件系统的拓扑结构及其质量进行有效分析和评估是软件工程中亟待解决的难题。采用复杂网络理论对软件系统进行建模和求解,将软件源代码中的函数作为节点,函数之间的调用关系看作有向边,函数调用次数作为边的权重,提出了一种软件动态执行加权网络模型的构建方法。通过对TAR、GEDIT、EMACS这3个开源软件系统的建模及网络特征分析,发现软件系统动态执行的加权拓扑网络满足小世界效应和无标度特性,即符合复杂网络特性。基于此结论,进一步利用CML(耦合映像格子)网络故障传播模型对软件系统的级联效应进行了模拟,通过实验发现了影响软件级联故障的主要因子,这些因子为软件质量保证等研究提供了重要支持。     

基于时间Petri网的嵌入式系统中断建模与验证

嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。     

尼龙6切片连续干燥工艺浅析

对PA6切片间歇干燥、连续干燥两种干燥方式的优缺点进行了简单对比分析,介绍了连续干燥方式产生的背景、基本原理、工艺流程、重要工艺参数,分析了影响干燥效率的几个重要因素,并探讨了连续干燥的干燥、增黏功能,认为当前追求规模效益的切片生产厂家宜采用连续干燥这一先进、科学的干燥方式,以降低生产劳动成本,提高经济效益。